\begin{pattern}{par-share}
\begin{circusaction*}
  \circblockopen
    \circvar v : T \circspot\\
    \t1
    \circblockopen
      \circmu X \circspot ~ start \then \circwait 0 \upto Init_{TB} \circseq \lschexpract InitOp \rschexpract \circseq
      \\
      \circvar x_1, x_2, \dots, x_n : T \circspot
      \\
      \circblockopen
          (record~?~x \then (\circwait 0 \upto RC_{TB} \circseq x_1 := x)) \circseq
          \\
          (record~?~x \then (\circwait 0 \upto RC_{TB} \circseq x_2 := x)) \circseq
          \\
          \t1 \dots
          \\
          (record~?~x \then (\circwait 0 \upto RC_{TB} \circseq x_n := x))
        \circseq
        \\
        \circwait 0 \upto Merge_{TB} \circseq \lschexpract MergeOp(\lbag x_1, x_2, \dots, x_n \rbag) \rschexpract \circseq
        \\
        output~!~v \then \Skip \circseq sync \then X
      \circblockclose
    \circblockclose
  \circblockclose
  \also
  \t1 \refby
  \also
  \circblockopen
    \circblockopen
      \circvar v : T \circspot\\
      \t1
      \circmu X \circspot
      \circblockopen
        init \then (\circwait 0 \upto Init_{TB} \circseq InitOp) ~ ~ \extchoice
        \\
        record~?~x \then (\circwait 0 \upto RC_{TB} \circseq MergeOp(\lbag x \rbag)) ~ ~ \extchoice
        \\
        output~!~v \then \Skip
      \circblockclose
      \circseq X
    \circblockclose
    \also
    \t1 \lpar \emptyset | \lchanset init, record, output \rchanset | \emptyset \rpar
    \also
    \circblockopen
      \circmu X \circspot init \then start \then
      \circblockopen
        (record~?~\anyvar \then \Skip) ~ ~ \interleave
        \\
        (record~?~\anyvar \then \Skip) ~ ~ \interleave
        \\
        \t1 \dots
        \\
        (record~?~\anyvar \then \Skip)
      \circblockclose
      \circseq
      output~?~\anyvar \then \Skip \circseq sync \then X
    \circblockclose
  \circblockclose
  \circhide 
  \also
  \t1 \lchanset init \rchanset
  \also
  \provided \mbox{$InitOp$ and $MergeOp$ are data operations} \; \provand
  \also
  \wrt(InitOp) = \{v\} = \wrt(MergeOp) \; \provand \; MergeOp(b_1 \uplus b_2) = MergeOp(b_1) \circseq MergeOp(b_2)
\end{circusaction*}
\end{pattern}
