datatype Node = A | end0 | B | C | D | startFlow14 | agateFlow40 | agateFlow29 | startFlow17 | startFlow22
datatype Msg = init | done
datatype Proc = GP2 | GS1

channel starts : Node
channel fin , aborts : { 0 }
channel finish , cancel , delayed , interrupted : Signal
channel Message44 , Message46 , Message47 , Message48 : Msg
channel Flow14 , Flow15 , Flow16 , Flow17 , Flow18 , cycle , Flow29 , Flow40 , Flow41 , Flow42 , Flow43 , Flow22 , Flow31 , Flow30

APool(A) = { fin.0, Flow14, Flow15, starts.A }
APool(end0) = { fin.0, Flow16 }
APool(B) = { fin.0, Flow17, Flow18, starts.B }
APool(C) = { fin.0, Flow15, Flow17, starts.C }
APool(D) = { fin.0, Flow18, Flow16, starts.D }
APool(startFlow14) = { fin.0, Flow14 }
IPool = { A, end0, B, C, D, startFlow14 }
AP2(end0) = { fin.0, Flow29 }
AP2(agateFlow40) = { fin.0, Flow17, Flow40, Flow41 }
AP2(agateFlow29) = { fin.0, Flow42, Flow43, Flow29 }
AP2(startFlow17) = { fin.0, Flow17 }
AP2(C) = { fin.0, Flow40, Flow42, Message44.init, Message46.done, starts.C }
AP2(D) = { fin.0, Flow41, Flow43, Message47.init, Message48.done, starts.D }
IP2 = { end0, agateFlow40, agateFlow29, startFlow17, C, D }
AS1(startFlow22) = { fin.0, Flow22 }
AS1(end0) = { fin.0, Flow31 }
AS1(A) = { fin.0, Flow22, Flow30, Message44.init, Message46.done, starts.A }
AS1(B) = { fin.0, Flow30, Flow31, Message47.init, Message48.done, starts.B }
IS1 = { startFlow22, end0, A, B }
Signal = { Flow22, Flow30, Flow31, Flow40, Flow29, Flow17, Flow42, Flow43, Flow15, Flow18, Flow16, Flow14 }
GA(GP2) = { Flow29, fin.0, Flow17, Flow40, Flow41, Flow42, Flow43, Message44.init, Message46.done, starts.C, Message47.init, Message48.done, starts.D }
GA(GS1) = { Flow22, Flow31, fin.0, Flow30, Message44.init, Message46.done, starts.A, Message47.init, Message48.done, starts.B }

PPool(A) = ( ( ( Flow14 -> ( SKIP ) ) ; ( ( SKIP ) ; ( ( starts.A -> ( SKIP ) ) ; ( ( ( SKIP ) ; ( ( SKIP ) ; ( SKIP ) ) ) ; ( Flow15 -> ( SKIP ) ) ) ) ) ) ; ( PPool(A) ) ) [] ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
PPool(B) = ( ( ( Flow17 -> ( SKIP ) ) ; ( ( SKIP ) ; ( ( starts.B -> ( SKIP ) ) ; ( ( ( SKIP ) ; ( ( SKIP ) ; ( SKIP ) ) ) ; ( Flow18 -> ( SKIP ) ) ) ) ) ) ; ( PPool(B) ) ) [] ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
PPool(C) = ( ( ( Flow15 -> ( SKIP ) ) ; ( ( SKIP ) ; ( ( starts.C -> ( SKIP ) ) ; ( ( ( SKIP ) ; ( ( SKIP ) ; ( SKIP ) ) ) ; ( Flow17 -> ( SKIP ) ) ) ) ) ) ; ( PPool(C) ) ) [] ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
PPool(D) = ( ( ( Flow18 -> ( SKIP ) ) ; ( ( SKIP ) ; ( ( starts.D -> ( SKIP ) ) ; ( ( ( SKIP ) ; ( ( SKIP ) ; ( SKIP ) ) ) ; ( Flow16 -> ( SKIP ) ) ) ) ) ) ; ( PPool(D) ) ) [] ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
PPool(startFlow14) = ( Flow14 -> ( SKIP ) ) ; ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
PPool(end0) = ( Flow16 -> ( SKIP ) ) ; ( fin.0 -> ( SKIP ) )
WPool = || iPool:IPool @ [ APool(iPool) ] ( PPool(iPool) )
PCPool = ( [] i:{ fin.0 } @ ( i -> ( SKIP ) ) ) [] ( [] i:{ Flow14, Flow15, starts.A, Flow16, Flow17, Flow18, starts.B, starts.C, starts.D } @ ( i -> ( PCPool ) ) )
LPool = ( WPool ) [| { fin.0, Flow14, Flow15, starts.A, Flow16, Flow17, Flow18, starts.B, starts.C, starts.D } |] ( PCPool )
DFPool = ( |~| i:{ Flow14, Flow15, starts.A, Flow16, Flow17, Flow18, starts.B, starts.C, starts.D } @ ( i -> ( DFPool ) ) ) |~| ( |~| i:{ fin.0 } @ ( i -> ( SKIP ) ) )
UPool = ( LPool ) \ ( { Flow14, Flow15, Flow16, Flow17, Flow18 } )
CPool1 = ( Flow14 -> ( ( ( ( ( ( ( ( starts.A -> ( Flow15 -> ( SKIP ) ) ) ; ( finish.Flow15 -> ( SKIP ) ) ) /\ ( cancel.Flow15 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow18, finish.Flow18, cancel.Flow18, delayed.Flow17, finish.Flow17, cancel.Flow17, delayed.Flow16, finish.Flow16, cancel.Flow16 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow15, finish.Flow15, cancel.Flow15, delayed.Flow18, finish.Flow18, cancel.Flow18, delayed.Flow17, finish.Flow17, cancel.Flow17, delayed.Flow16, finish.Flow16, cancel.Flow16 }) ) ) [| { delayed.Flow15, finish.Flow15, cancel.Flow15, delayed.Flow18, finish.Flow18, cancel.Flow18, delayed.Flow17, finish.Flow17, cancel.Flow17, delayed.Flow16, finish.Flow16, cancel.Flow16 } |] ( finish.Flow15 -> ( ( ( ( ( ( ( ( starts.C -> ( Flow17 -> ( SKIP ) ) ) ; ( finish.Flow17 -> ( SKIP ) ) ) /\ ( cancel.Flow17 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow15, finish.Flow15, cancel.Flow15, delayed.Flow18, finish.Flow18, cancel.Flow18, delayed.Flow16, finish.Flow16, cancel.Flow16 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow15, finish.Flow15, cancel.Flow15, delayed.Flow18, finish.Flow18, cancel.Flow18, delayed.Flow17, finish.Flow17, cancel.Flow17, delayed.Flow16, finish.Flow16, cancel.Flow16 }) ) ) [| { delayed.Flow15, finish.Flow15, cancel.Flow15, delayed.Flow18, finish.Flow18, cancel.Flow18, delayed.Flow17, finish.Flow17, cancel.Flow17, delayed.Flow16, finish.Flow16, cancel.Flow16 } |] ( finish.Flow17 -> ( ( ( ( ( ( ( ( starts.B -> ( Flow18 -> ( SKIP ) ) ) ; ( finish.Flow18 -> ( SKIP ) ) ) /\ ( cancel.Flow18 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow15, finish.Flow15, cancel.Flow15, delayed.Flow17, finish.Flow17, cancel.Flow17, delayed.Flow16, finish.Flow16, cancel.Flow16 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow15, finish.Flow15, cancel.Flow15, delayed.Flow18, finish.Flow18, cancel.Flow18, delayed.Flow17, finish.Flow17, cancel.Flow17, delayed.Flow16, finish.Flow16, cancel.Flow16 }) ) ) [| { delayed.Flow15, finish.Flow15, cancel.Flow15, delayed.Flow18, finish.Flow18, cancel.Flow18, delayed.Flow17, finish.Flow17, cancel.Flow17, delayed.Flow16, finish.Flow16, cancel.Flow16 } |] ( finish.Flow18 -> ( ( ( ( ( ( ( ( starts.D -> ( Flow16 -> ( SKIP ) ) ) ; ( finish.Flow16 -> ( SKIP ) ) ) /\ ( cancel.Flow16 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow15, finish.Flow15, cancel.Flow15, delayed.Flow18, finish.Flow18, cancel.Flow18, delayed.Flow17, finish.Flow17, cancel.Flow17 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow15, finish.Flow15, cancel.Flow15, delayed.Flow18, finish.Flow18, cancel.Flow18, delayed.Flow17, finish.Flow17, cancel.Flow17, delayed.Flow16, finish.Flow16, cancel.Flow16 }) ) ) [| { delayed.Flow15, finish.Flow15, cancel.Flow15, delayed.Flow18, finish.Flow18, cancel.Flow18, delayed.Flow17, finish.Flow17, cancel.Flow17, delayed.Flow16, finish.Flow16, cancel.Flow16 } |] ( finish.Flow16 -> ( SKIP ) ) ) ) ) ) ) ) ) ) /\ ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
CPool = ( CPool1 ) \ ( { delayed.Flow15, finish.Flow15, cancel.Flow15, delayed.Flow18, finish.Flow18, cancel.Flow18, delayed.Flow17, finish.Flow17, cancel.Flow17, delayed.Flow16, finish.Flow16, cancel.Flow16 } )
TPool1 = ( LPool ) [| { Flow14, Flow15, starts.A, Flow16, fin.0, Flow17, Flow18, starts.B, starts.C, starts.D } |] ( CPool )
TPool = ( TPool1 ) \ ( { Flow14, Flow15, Flow16, Flow17, Flow18 } )
PP2(agateFlow40) = ( ( ( Flow17 -> ( SKIP ) ) ; ( ( Flow40 -> ( SKIP ) ) ||| ( Flow41 -> ( SKIP ) ) ) ) ; ( PP2(agateFlow40) ) ) [] ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
PP2(agateFlow29) = ( ( ( ( Flow42 -> ( SKIP ) ) ||| ( Flow43 -> ( SKIP ) ) ) ; ( Flow29 -> ( SKIP ) ) ) ; ( PP2(agateFlow29) ) ) [] ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
PP2(startFlow17) = ( Flow17 -> ( SKIP ) ) ; ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
PP2(C) = ( ( ( Flow40 -> ( SKIP ) ) ; ( ( Message44.init -> ( SKIP ) ) ; ( ( starts.C -> ( SKIP ) ) ; ( ( ( SKIP ) ; ( ( Message46.done -> ( SKIP ) ) ; ( SKIP ) ) ) ; ( Flow42 -> ( SKIP ) ) ) ) ) ) ; ( PP2(C) ) ) [] ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
PP2(D) = ( ( ( Flow41 -> ( SKIP ) ) ; ( ( Message47.init -> ( SKIP ) ) ; ( ( starts.D -> ( SKIP ) ) ; ( ( ( SKIP ) ; ( ( Message48.done -> ( SKIP ) ) ; ( SKIP ) ) ) ; ( Flow43 -> ( SKIP ) ) ) ) ) ) ; ( PP2(D) ) ) [] ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
PP2(end0) = ( Flow29 -> ( SKIP ) ) ; ( fin.0 -> ( SKIP ) )
WP2 = || iP2:IP2 @ [ AP2(iP2) ] ( PP2(iP2) )
PCP2 = ( [] i:{ fin.0 } @ ( i -> ( SKIP ) ) ) [] ( [] i:{ Flow29, Flow17, Flow40, Flow41, Flow42, Flow43, Message44.init, Message46.done, starts.C, Message47.init, Message48.done, starts.D } @ ( i -> ( PCP2 ) ) )
LP2 = ( WP2 ) [| { fin.0, Flow29, Flow17, Flow40, Flow41, Flow42, Flow43, Message44.init, Message46.done, starts.C, Message47.init, Message48.done, starts.D } |] ( PCP2 )
DFP2 = ( |~| i:{ Flow29, Flow17, Flow40, Flow41, Flow42, Flow43, Message44.init, Message46.done, starts.C, Message47.init, Message48.done, starts.D } @ ( i -> ( DFP2 ) ) ) |~| ( |~| i:{ fin.0 } @ ( i -> ( SKIP ) ) )
UP2 = ( LP2 ) \ ( { Flow29, Flow17, Flow40, Flow41, Flow42, Flow43 } )
CP21 = ( Flow17 -> ( ( Flow40 -> ( Flow41 -> ( ( ( ( ( ( ( ( ( starts.C -> ( Flow42 -> ( SKIP ) ) ) ; ( finish.Flow42 -> ( SKIP ) ) ) |~| ( delayed.Flow42 -> ( SKIP ) ) ) /\ ( cancel.Flow42 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow43, finish.Flow43, cancel.Flow43 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 }) ) ) [| { delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 } |] ( ( delayed.Flow42 -> ( ( ( ( ( ( ( ( ( ( starts.D -> ( Flow43 -> ( SKIP ) ) ) ; ( finish.Flow43 -> ( SKIP ) ) ) |~| ( delayed.Flow43 -> ( SKIP ) ) ) /\ ( cancel.Flow43 -> ( SKIP ) ) ) ||| ( ( ( starts.C -> ( Flow42 -> ( SKIP ) ) ) ; ( finish.Flow42 -> ( SKIP ) ) ) /\ ( cancel.Flow42 -> ( SKIP ) ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({  }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 }) ) ) [| { delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 } |] ( ( delayed.Flow43 -> ( finish.Flow42 -> ( ( ( ( ( ( ( ( ( starts.D -> ( Flow43 -> ( SKIP ) ) ) ; ( finish.Flow43 -> ( SKIP ) ) ) |~| ( delayed.Flow43 -> ( SKIP ) ) ) /\ ( cancel.Flow43 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 }) ) ) [| { delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 } |] ( ( delayed.Flow43 -> ( ( ( ( ( ( ( ( starts.D -> ( Flow43 -> ( SKIP ) ) ) ; ( finish.Flow43 -> ( SKIP ) ) ) /\ ( cancel.Flow43 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 }) ) ) [| { delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 } |] ( finish.Flow43 -> ( Flow29 -> ( SKIP ) ) ) ) ) [] ( finish.Flow43 -> ( Flow29 -> ( SKIP ) ) ) ) ) ) ) [] ( ( finish.Flow43 -> ( finish.Flow42 -> ( Flow29 -> ( SKIP ) ) ) ) [] ( finish.Flow42 -> ( ( delayed.Flow43 -> ( ( ( ( ( ( ( ( ( starts.D -> ( Flow43 -> ( SKIP ) ) ) ; ( finish.Flow43 -> ( SKIP ) ) ) |~| ( delayed.Flow43 -> ( SKIP ) ) ) /\ ( cancel.Flow43 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 }) ) ) [| { delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 } |] ( ( delayed.Flow43 -> ( ( ( ( ( ( ( ( starts.D -> ( Flow43 -> ( SKIP ) ) ) ; ( finish.Flow43 -> ( SKIP ) ) ) /\ ( cancel.Flow43 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 }) ) ) [| { delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 } |] ( finish.Flow43 -> ( Flow29 -> ( SKIP ) ) ) ) ) [] ( finish.Flow43 -> ( Flow29 -> ( SKIP ) ) ) ) ) ) [] ( finish.Flow43 -> ( Flow29 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow42 -> ( ( ( ( ( ( ( ( ( starts.D -> ( Flow43 -> ( SKIP ) ) ) ; ( finish.Flow43 -> ( SKIP ) ) ) |~| ( delayed.Flow43 -> ( SKIP ) ) ) /\ ( cancel.Flow43 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 }) ) ) [| { delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 } |] ( ( delayed.Flow43 -> ( ( ( ( ( ( ( ( starts.D -> ( Flow43 -> ( SKIP ) ) ) ; ( finish.Flow43 -> ( SKIP ) ) ) /\ ( cancel.Flow43 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 }) ) ) [| { delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 } |] ( finish.Flow43 -> ( Flow29 -> ( SKIP ) ) ) ) ) [] ( finish.Flow43 -> ( Flow29 -> ( SKIP ) ) ) ) ) ) ) ) ) ) [] ( Flow41 -> ( Flow40 -> ( ( ( ( ( ( ( ( ( starts.C -> ( Flow42 -> ( SKIP ) ) ) ; ( finish.Flow42 -> ( SKIP ) ) ) |~| ( delayed.Flow42 -> ( SKIP ) ) ) /\ ( cancel.Flow42 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow43, finish.Flow43, cancel.Flow43 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 }) ) ) [| { delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 } |] ( ( delayed.Flow42 -> ( ( ( ( ( ( ( ( ( ( starts.D -> ( Flow43 -> ( SKIP ) ) ) ; ( finish.Flow43 -> ( SKIP ) ) ) |~| ( delayed.Flow43 -> ( SKIP ) ) ) /\ ( cancel.Flow43 -> ( SKIP ) ) ) ||| ( ( ( starts.C -> ( Flow42 -> ( SKIP ) ) ) ; ( finish.Flow42 -> ( SKIP ) ) ) /\ ( cancel.Flow42 -> ( SKIP ) ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({  }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 }) ) ) [| { delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 } |] ( ( delayed.Flow43 -> ( finish.Flow42 -> ( ( ( ( ( ( ( ( ( starts.D -> ( Flow43 -> ( SKIP ) ) ) ; ( finish.Flow43 -> ( SKIP ) ) ) |~| ( delayed.Flow43 -> ( SKIP ) ) ) /\ ( cancel.Flow43 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 }) ) ) [| { delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 } |] ( ( delayed.Flow43 -> ( ( ( ( ( ( ( ( starts.D -> ( Flow43 -> ( SKIP ) ) ) ; ( finish.Flow43 -> ( SKIP ) ) ) /\ ( cancel.Flow43 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 }) ) ) [| { delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 } |] ( finish.Flow43 -> ( Flow29 -> ( SKIP ) ) ) ) ) [] ( finish.Flow43 -> ( Flow29 -> ( SKIP ) ) ) ) ) ) ) [] ( ( finish.Flow43 -> ( finish.Flow42 -> ( Flow29 -> ( SKIP ) ) ) ) [] ( finish.Flow42 -> ( ( delayed.Flow43 -> ( ( ( ( ( ( ( ( ( starts.D -> ( Flow43 -> ( SKIP ) ) ) ; ( finish.Flow43 -> ( SKIP ) ) ) |~| ( delayed.Flow43 -> ( SKIP ) ) ) /\ ( cancel.Flow43 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 }) ) ) [| { delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 } |] ( ( delayed.Flow43 -> ( ( ( ( ( ( ( ( starts.D -> ( Flow43 -> ( SKIP ) ) ) ; ( finish.Flow43 -> ( SKIP ) ) ) /\ ( cancel.Flow43 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 }) ) ) [| { delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 } |] ( finish.Flow43 -> ( Flow29 -> ( SKIP ) ) ) ) ) [] ( finish.Flow43 -> ( Flow29 -> ( SKIP ) ) ) ) ) ) [] ( finish.Flow43 -> ( Flow29 -> ( SKIP ) ) ) ) ) ) ) ) ) [] ( finish.Flow42 -> ( ( ( ( ( ( ( ( ( starts.D -> ( Flow43 -> ( SKIP ) ) ) ; ( finish.Flow43 -> ( SKIP ) ) ) |~| ( delayed.Flow43 -> ( SKIP ) ) ) /\ ( cancel.Flow43 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 }) ) ) [| { delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 } |] ( ( delayed.Flow43 -> ( ( ( ( ( ( ( ( starts.D -> ( Flow43 -> ( SKIP ) ) ) ; ( finish.Flow43 -> ( SKIP ) ) ) /\ ( cancel.Flow43 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 }) ) ) [| { delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 } |] ( finish.Flow43 -> ( Flow29 -> ( SKIP ) ) ) ) ) [] ( finish.Flow43 -> ( Flow29 -> ( SKIP ) ) ) ) ) ) ) ) ) ) ) ) /\ ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
CP2 = ( CP21 ) \ ( { delayed.Flow42, finish.Flow42, cancel.Flow42, delayed.Flow43, finish.Flow43, cancel.Flow43 } )
TP21 = ( LP2 ) [| { Flow29, fin.0, Flow17, Flow40, Flow41, Flow42, Flow43, starts.C, starts.D } |] ( CP2 )
TP2 = ( TP21 ) \ ( { Flow29, Flow17, Flow40, Flow41, Flow42, Flow43 } )
PS1(startFlow22) = ( Flow22 -> ( SKIP ) ) ; ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
PS1(A) = ( ( ( Flow22 -> ( SKIP ) ) ; ( ( SKIP ) ; ( ( starts.A -> ( SKIP ) ) ; ( ( ( Message44.init -> ( SKIP ) ) ; ( ( SKIP ) ; ( Message46.done -> ( SKIP ) ) ) ) ; ( Flow30 -> ( SKIP ) ) ) ) ) ) ; ( PS1(A) ) ) [] ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
PS1(B) = ( ( ( Flow30 -> ( SKIP ) ) ; ( ( SKIP ) ; ( ( starts.B -> ( SKIP ) ) ; ( ( ( Message47.init -> ( SKIP ) ) ; ( ( SKIP ) ; ( Message48.done -> ( SKIP ) ) ) ) ; ( Flow31 -> ( SKIP ) ) ) ) ) ) ; ( PS1(B) ) ) [] ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
PS1(end0) = ( Flow31 -> ( SKIP ) ) ; ( fin.0 -> ( SKIP ) )
WS1 = || iS1:IS1 @ [ AS1(iS1) ] ( PS1(iS1) )
PCS1 = ( [] i:{ fin.0 } @ ( i -> ( SKIP ) ) ) [] ( [] i:{ Flow22, Flow31, Flow30, Message44.init, Message46.done, starts.A, Message47.init, Message48.done, starts.B } @ ( i -> ( PCS1 ) ) )
LS1 = ( WS1 ) [| { fin.0, Flow22, Flow31, Flow30, Message44.init, Message46.done, starts.A, Message47.init, Message48.done, starts.B } |] ( PCS1 )
DFS1 = ( |~| i:{ Flow22, Flow31, Flow30, Message44.init, Message46.done, starts.A, Message47.init, Message48.done, starts.B } @ ( i -> ( DFS1 ) ) ) |~| ( |~| i:{ fin.0 } @ ( i -> ( SKIP ) ) )
US1 = ( LS1 ) \ ( { Flow22, Flow31, Flow30 } )
CS11 = ( Flow22 -> ( ( ( ( ( ( ( ( ( starts.A -> ( Flow30 -> ( SKIP ) ) ) ; ( finish.Flow30 -> ( SKIP ) ) ) |~| ( delayed.Flow30 -> ( SKIP ) ) ) /\ ( cancel.Flow30 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow31, finish.Flow31, cancel.Flow31 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow30, finish.Flow30, cancel.Flow30, delayed.Flow31, finish.Flow31, cancel.Flow31 }) ) ) [| { delayed.Flow30, finish.Flow30, cancel.Flow30, delayed.Flow31, finish.Flow31, cancel.Flow31 } |] ( ( delayed.Flow30 -> ( ( ( ( ( ( ( ( starts.A -> ( Flow30 -> ( SKIP ) ) ) ; ( finish.Flow30 -> ( SKIP ) ) ) /\ ( cancel.Flow30 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow31, finish.Flow31, cancel.Flow31 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow30, finish.Flow30, cancel.Flow30, delayed.Flow31, finish.Flow31, cancel.Flow31 }) ) ) [| { delayed.Flow30, finish.Flow30, cancel.Flow30, delayed.Flow31, finish.Flow31, cancel.Flow31 } |] ( finish.Flow30 -> ( ( ( ( ( ( ( ( ( starts.B -> ( Flow31 -> ( SKIP ) ) ) ; ( finish.Flow31 -> ( SKIP ) ) ) |~| ( delayed.Flow31 -> ( SKIP ) ) ) /\ ( cancel.Flow31 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow30, finish.Flow30, cancel.Flow30 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow30, finish.Flow30, cancel.Flow30, delayed.Flow31, finish.Flow31, cancel.Flow31 }) ) ) [| { delayed.Flow30, finish.Flow30, cancel.Flow30, delayed.Flow31, finish.Flow31, cancel.Flow31 } |] ( ( delayed.Flow31 -> ( ( ( ( ( ( ( ( starts.B -> ( Flow31 -> ( SKIP ) ) ) ; ( finish.Flow31 -> ( SKIP ) ) ) /\ ( cancel.Flow31 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow30, finish.Flow30, cancel.Flow30 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow30, finish.Flow30, cancel.Flow30, delayed.Flow31, finish.Flow31, cancel.Flow31 }) ) ) [| { delayed.Flow30, finish.Flow30, cancel.Flow30, delayed.Flow31, finish.Flow31, cancel.Flow31 } |] ( finish.Flow31 -> ( SKIP ) ) ) ) [] ( finish.Flow31 -> ( SKIP ) ) ) ) ) ) ) [] ( finish.Flow30 -> ( ( ( ( ( ( ( ( ( starts.B -> ( Flow31 -> ( SKIP ) ) ) ; ( finish.Flow31 -> ( SKIP ) ) ) |~| ( delayed.Flow31 -> ( SKIP ) ) ) /\ ( cancel.Flow31 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow30, finish.Flow30, cancel.Flow30 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow30, finish.Flow30, cancel.Flow30, delayed.Flow31, finish.Flow31, cancel.Flow31 }) ) ) [| { delayed.Flow30, finish.Flow30, cancel.Flow30, delayed.Flow31, finish.Flow31, cancel.Flow31 } |] ( ( delayed.Flow31 -> ( ( ( ( ( ( ( ( starts.B -> ( Flow31 -> ( SKIP ) ) ) ; ( finish.Flow31 -> ( SKIP ) ) ) /\ ( cancel.Flow31 -> ( SKIP ) ) ) ; ( cycle -> ( SKIP ) ) ) [| { cycle } |] ( ( run({ delayed.Flow30, finish.Flow30, cancel.Flow30 }) ) /\ ( cycle -> ( SKIP ) ) ) ) \ ( { cycle } ) ) ; ( run({ delayed.Flow30, finish.Flow30, cancel.Flow30, delayed.Flow31, finish.Flow31, cancel.Flow31 }) ) ) [| { delayed.Flow30, finish.Flow30, cancel.Flow30, delayed.Flow31, finish.Flow31, cancel.Flow31 } |] ( finish.Flow31 -> ( SKIP ) ) ) ) [] ( finish.Flow31 -> ( SKIP ) ) ) ) ) ) ) ) /\ ( [] i:{ 0 } @ ( fin.i -> ( SKIP ) ) )
CS1 = ( CS11 ) \ ( { delayed.Flow30, finish.Flow30, cancel.Flow30, delayed.Flow31, finish.Flow31, cancel.Flow31 } )
run(S) = [] i:S @ ( i -> ( run(S) ) )
TS11 = ( LS1 ) [| { Flow22, Flow31, fin.0, Flow30, starts.A, starts.B } |] ( CS1 )
TS1 = ( TS11 ) \ ( { Flow22, Flow31, Flow30 } )
DF = ( |~| i:{ Flow29, Flow17, Flow40, Flow41, Flow42, Flow43, Message44.init, Message46.done, starts.C, Message47.init, Message48.done, starts.D, Flow22, Flow31, Flow30, starts.A, starts.B } @ ( i -> ( DF ) ) ) |~| ( |~| i:{ fin.0, fin.0 } @ ( i -> ( SKIP ) ) )
UGP(GP2) = UP2
UGP(GS1) = US1
UC = ( || i:{ GP2, GS1 } @ [ GA(i) ] ( UGP(i) ) ) \ ( { Message44.init, Message46.done, Message47.init, Message48.done, Message44.init, Message46.done, Message47.init, Message48.done } )
TGP(GP2) = TP2
TGP(GS1) = TS1
TC = ( || i:{ GP2, GS1 } @ [ GA(i) ] ( TGP(i) ) ) \ ( { Message44.init, Message46.done, Message47.init, Message48.done, Message44.init, Message46.done, Message47.init, Message48.done } )

assert DFPool [F= UPool
assert DFPool [F= TPool
assert DFP2 [F= ( UP2 ) \ ( { Message44.init, Message46.done, Message47.init, Message48.done } )
assert DFP2 [F= ( TP2 ) \ ( { Message44.init, Message46.done, Message47.init, Message48.done } )
assert DFS1 [F= ( US1 ) \ ( { Message44.init, Message46.done, Message47.init, Message48.done } )
assert DFS1 [F= ( TS1 ) \ ( { Message44.init, Message46.done, Message47.init, Message48.done } )
assert DF [F= UC
assert DF [F= TC
assert TPool [F= TC
assert TPool [F= UC