add small result formulas

results/workflow2agents.ltl

+G ((n0 → X n1) ∧ (n1 → X (n3 ∨ n2)) ∧ (n2 → X n2) ∧ (n3 → X n1)) ∧ G (¬(n0 ∧ n1) ∧ ¬(n0 ∧ n2) ∧ ¬(n0 ∧ n3) ∧ ¬(n1 ∧ n2) ∧ ¬(n1 ∧ n3) ∧ ¬(n2 ∧ n3)) ∧ ((n0 ∧ X n1) → ((X Q_a_a ↔ (Q_a_a ∨ (O_a ∧ choice0_a_a))) ∧ (X Q_b_a ↔ (Q_b_a ∨ (O_a ∧ choice0_b_a))) ∧ (X Q_a_b ↔ (Q_a_b ∨ (O_b ∧ choice0_a_b))) ∧ (X Q_b_b ↔ (Q_b_b ∨ (O_b ∧ choice0_b_b))) ∧ ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b)))))) ∧ ((n1 ∧ X n3) → ((X S_a_a_a ↔ (S_a_a_a ∨ R_a_a)) ∧ (X S_b_a_a ↔ (S_b_a_a ∨ R_a_a)) ∧ (X S_a_b_a ↔ (S_a_b_a ∨ R_b_a)) ∧ (X S_b_b_a ↔ (S_b_b_a ∨ R_b_a)) ∧ (X S_a_a_b ↔ (S_a_a_b ∨ R_a_b)) ∧ (X S_b_a_b ↔ (S_b_a_b ∨ R_a_b)) ∧ (X S_a_b_b ↔ (S_a_b_b ∨ R_b_b)) ∧ (X S_b_b_b ↔ (S_b_b_b ∨ R_b_b)) ∧ ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b)))))) ∧ ((n1 ∧ X n2) → ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b)))))) ∧ ((n2 ∧ X n2) → ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b)))))) ∧ ((n3 ∧ X n1) → ((X R_a_a ↔ (R_a_a ∨ Q_a_a)) ∧ (X R_b_a ↔ (R_b_a ∨ Q_b_a)) ∧ (X R_a_b ↔ (R_a_b ∨ Q_a_b)) ∧ (X R_b_b ↔ (R_b_b ∨ Q_b_b)) ∧ ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b)))))) ∧ (n0 ∧ ¬n1 ∧ ¬n2 ∧ ¬n3 ∧ ¬Q_a_a ∧ ¬Q_b_a ∧ ¬Q_a_b ∧ ¬Q_b_b ∧ (¬R_a_a ∧ ¬R_b_a ∧ ¬R_a_b ∧ ¬R_b_b ∧ (¬S_a_a_a ∧ ¬S_b_a_a ∧ ¬S_a_b_a ∧ ¬S_b_b_a ∧ ¬S_a_a_b ∧ ¬S_b_a_b ∧ ¬S_a_b_b ∧ ¬S_b_b_b)))

results/workflow3agents.ltl

+G ((n0 → X n1) ∧ (n1 → X (n3 ∨ n2)) ∧ (n2 → X n2) ∧ (n3 → X n1)) ∧ G (¬(n0 ∧ n1) ∧ ¬(n0 ∧ n2) ∧ ¬(n0 ∧ n3) ∧ ¬(n1 ∧ n2) ∧ ¬(n1 ∧ n3) ∧ ¬(n2 ∧ n3)) ∧ ((n0 ∧ X n1) → ((X Q_a_a ↔ (Q_a_a ∨ (O_a ∧ choice0_a_a))) ∧ (X Q_b_a ↔ (Q_b_a ∨ (O_a ∧ choice0_b_a))) ∧ (X Q_c_a ↔ (Q_c_a ∨ (O_a ∧ choice0_c_a))) ∧ (X Q_a_b ↔ (Q_a_b ∨ (O_b ∧ choice0_a_b))) ∧ (X Q_b_b ↔ (Q_b_b ∨ (O_b ∧ choice0_b_b))) ∧ (X Q_c_b ↔ (Q_c_b ∨ (O_b ∧ choice0_c_b))) ∧ (X Q_a_c ↔ (Q_a_c ∨ (O_c ∧ choice0_a_c))) ∧ (X Q_b_c ↔ (Q_b_c ∨ (O_c ∧ choice0_b_c))) ∧ (X Q_c_c ↔ (Q_c_c ∨ (O_c ∧ choice0_c_c))) ∧ ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ (X O_c ↔ O_c) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_c_a ↔ R_c_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b) ∧ (X R_c_b ↔ R_c_b) ∧ (X R_a_c ↔ R_a_c) ∧ (X R_b_c ↔ R_b_c) ∧ (X R_c_c ↔ R_c_c) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_c_a_a ↔ S_c_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_c_b_a ↔ S_c_b_a) ∧ (X S_a_c_a ↔ S_a_c_a) ∧ (X S_b_c_a ↔ S_b_c_a) ∧ (X S_c_c_a ↔ S_c_c_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_c_a_b ↔ S_c_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b) ∧ (X S_c_b_b ↔ S_c_b_b) ∧ (X S_a_c_b ↔ S_a_c_b) ∧ (X S_b_c_b ↔ S_b_c_b) ∧ (X S_c_c_b ↔ S_c_c_b) ∧ (X S_a_a_c ↔ S_a_a_c) ∧ (X S_b_a_c ↔ S_b_a_c) ∧ (X S_c_a_c ↔ S_c_a_c) ∧ (X S_a_b_c ↔ S_a_b_c) ∧ (X S_b_b_c ↔ S_b_b_c) ∧ (X S_c_b_c ↔ S_c_b_c) ∧ (X S_a_c_c ↔ S_a_c_c) ∧ (X S_b_c_c ↔ S_b_c_c) ∧ (X S_c_c_c ↔ S_c_c_c)))))) ∧ ((n1 ∧ X n3) → ((X S_a_a_a ↔ (S_a_a_a ∨ R_a_a)) ∧ (X S_b_a_a ↔ (S_b_a_a ∨ R_a_a)) ∧ (X S_c_a_a ↔ (S_c_a_a ∨ R_a_a)) ∧ (X S_a_b_a ↔ (S_a_b_a ∨ R_b_a)) ∧ (X S_b_b_a ↔ (S_b_b_a ∨ R_b_a)) ∧ (X S_c_b_a ↔ (S_c_b_a ∨ R_b_a)) ∧ (X S_a_c_a ↔ (S_a_c_a ∨ R_c_a)) ∧ (X S_b_c_a ↔ (S_b_c_a ∨ R_c_a)) ∧ (X S_c_c_a ↔ (S_c_c_a ∨ R_c_a)) ∧ (X S_a_a_b ↔ (S_a_a_b ∨ R_a_b)) ∧ (X S_b_a_b ↔ (S_b_a_b ∨ R_a_b)) ∧ (X S_c_a_b ↔ (S_c_a_b ∨ R_a_b)) ∧ (X S_a_b_b ↔ (S_a_b_b ∨ R_b_b)) ∧ (X S_b_b_b ↔ (S_b_b_b ∨ R_b_b)) ∧ (X S_c_b_b ↔ (S_c_b_b ∨ R_b_b)) ∧ (X S_a_c_b ↔ (S_a_c_b ∨ R_c_b)) ∧ (X S_b_c_b ↔ (S_b_c_b ∨ R_c_b)) ∧ (X S_c_c_b ↔ (S_c_c_b ∨ R_c_b)) ∧ (X S_a_a_c ↔ (S_a_a_c ∨ R_a_c)) ∧ (X S_b_a_c ↔ (S_b_a_c ∨ R_a_c)) ∧ (X S_c_a_c ↔ (S_c_a_c ∨ R_a_c)) ∧ (X S_a_b_c ↔ (S_a_b_c ∨ R_b_c)) ∧ (X S_b_b_c ↔ (S_b_b_c ∨ R_b_c)) ∧ (X S_c_b_c ↔ (S_c_b_c ∨ R_b_c)) ∧ (X S_a_c_c ↔ (S_a_c_c ∨ R_c_c)) ∧ (X S_b_c_c ↔ (S_b_c_c ∨ R_c_c)) ∧ (X S_c_c_c ↔ (S_c_c_c ∨ R_c_c)) ∧ ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ (X O_c ↔ O_c) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_c_a ↔ Q_c_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ (X Q_c_b ↔ Q_c_b) ∧ (X Q_a_c ↔ Q_a_c) ∧ (X Q_b_c ↔ Q_b_c) ∧ (X Q_c_c ↔ Q_c_c) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_c_a ↔ R_c_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b) ∧ (X R_c_b ↔ R_c_b) ∧ (X R_a_c ↔ R_a_c) ∧ (X R_b_c ↔ R_b_c) ∧ (X R_c_c ↔ R_c_c)))))) ∧ ((n1 ∧ X n2) → ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ (X O_c ↔ O_c) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_c_a ↔ Q_c_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ (X Q_c_b ↔ Q_c_b) ∧ (X Q_a_c ↔ Q_a_c) ∧ (X Q_b_c ↔ Q_b_c) ∧ (X Q_c_c ↔ Q_c_c) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_c_a ↔ R_c_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b) ∧ (X R_c_b ↔ R_c_b) ∧ (X R_a_c ↔ R_a_c) ∧ (X R_b_c ↔ R_b_c) ∧ (X R_c_c ↔ R_c_c) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_c_a_a ↔ S_c_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_c_b_a ↔ S_c_b_a) ∧ (X S_a_c_a ↔ S_a_c_a) ∧ (X S_b_c_a ↔ S_b_c_a) ∧ (X S_c_c_a ↔ S_c_c_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_c_a_b ↔ S_c_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b) ∧ (X S_c_b_b ↔ S_c_b_b) ∧ (X S_a_c_b ↔ S_a_c_b) ∧ (X S_b_c_b ↔ S_b_c_b) ∧ (X S_c_c_b ↔ S_c_c_b) ∧ (X S_a_a_c ↔ S_a_a_c) ∧ (X S_b_a_c ↔ S_b_a_c) ∧ (X S_c_a_c ↔ S_c_a_c) ∧ (X S_a_b_c ↔ S_a_b_c) ∧ (X S_b_b_c ↔ S_b_b_c) ∧ (X S_c_b_c ↔ S_c_b_c) ∧ (X S_a_c_c ↔ S_a_c_c) ∧ (X S_b_c_c ↔ S_b_c_c) ∧ (X S_c_c_c ↔ S_c_c_c)))))) ∧ ((n2 ∧ X n2) → ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ (X O_c ↔ O_c) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_c_a ↔ Q_c_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ (X Q_c_b ↔ Q_c_b) ∧ (X Q_a_c ↔ Q_a_c) ∧ (X Q_b_c ↔ Q_b_c) ∧ (X Q_c_c ↔ Q_c_c) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_c_a ↔ R_c_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b) ∧ (X R_c_b ↔ R_c_b) ∧ (X R_a_c ↔ R_a_c) ∧ (X R_b_c ↔ R_b_c) ∧ (X R_c_c ↔ R_c_c) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_c_a_a ↔ S_c_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_c_b_a ↔ S_c_b_a) ∧ (X S_a_c_a ↔ S_a_c_a) ∧ (X S_b_c_a ↔ S_b_c_a) ∧ (X S_c_c_a ↔ S_c_c_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_c_a_b ↔ S_c_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b) ∧ (X S_c_b_b ↔ S_c_b_b) ∧ (X S_a_c_b ↔ S_a_c_b) ∧ (X S_b_c_b ↔ S_b_c_b) ∧ (X S_c_c_b ↔ S_c_c_b) ∧ (X S_a_a_c ↔ S_a_a_c) ∧ (X S_b_a_c ↔ S_b_a_c) ∧ (X S_c_a_c ↔ S_c_a_c) ∧ (X S_a_b_c ↔ S_a_b_c) ∧ (X S_b_b_c ↔ S_b_b_c) ∧ (X S_c_b_c ↔ S_c_b_c) ∧ (X S_a_c_c ↔ S_a_c_c) ∧ (X S_b_c_c ↔ S_b_c_c) ∧ (X S_c_c_c ↔ S_c_c_c)))))) ∧ ((n3 ∧ X n1) → ((X R_a_a ↔ (R_a_a ∨ Q_a_a)) ∧ (X R_b_a ↔ (R_b_a ∨ Q_b_a)) ∧ (X R_c_a ↔ (R_c_a ∨ Q_c_a)) ∧ (X R_a_b ↔ (R_a_b ∨ Q_a_b)) ∧ (X R_b_b ↔ (R_b_b ∨ Q_b_b)) ∧ (X R_c_b ↔ (R_c_b ∨ Q_c_b)) ∧ (X R_a_c ↔ (R_a_c ∨ Q_a_c)) ∧ (X R_b_c ↔ (R_b_c ∨ Q_b_c)) ∧ (X R_c_c ↔ (R_c_c ∨ Q_c_c)) ∧ ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ (X O_c ↔ O_c) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_c_a ↔ Q_c_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ (X Q_c_b ↔ Q_c_b) ∧ (X Q_a_c ↔ Q_a_c) ∧ (X Q_b_c ↔ Q_b_c) ∧ (X Q_c_c ↔ Q_c_c) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_c_a_a ↔ S_c_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_c_b_a ↔ S_c_b_a) ∧ (X S_a_c_a ↔ S_a_c_a) ∧ (X S_b_c_a ↔ S_b_c_a) ∧ (X S_c_c_a ↔ S_c_c_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_c_a_b ↔ S_c_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b) ∧ (X S_c_b_b ↔ S_c_b_b) ∧ (X S_a_c_b ↔ S_a_c_b) ∧ (X S_b_c_b ↔ S_b_c_b) ∧ (X S_c_c_b ↔ S_c_c_b) ∧ (X S_a_a_c ↔ S_a_a_c) ∧ (X S_b_a_c ↔ S_b_a_c) ∧ (X S_c_a_c ↔ S_c_a_c) ∧ (X S_a_b_c ↔ S_a_b_c) ∧ (X S_b_b_c ↔ S_b_b_c) ∧ (X S_c_b_c ↔ S_c_b_c) ∧ (X S_a_c_c ↔ S_a_c_c) ∧ (X S_b_c_c ↔ S_b_c_c) ∧ (X S_c_c_c ↔ S_c_c_c)))))) ∧ (n0 ∧ ¬n1 ∧ ¬n2 ∧ ¬n3 ∧ ¬Q_a_a ∧ ¬Q_b_a ∧ ¬Q_c_a ∧ ¬Q_a_b ∧ ¬Q_b_b ∧ ¬Q_c_b ∧ ¬Q_a_c ∧ ¬Q_b_c ∧ ¬Q_c_c ∧ (¬R_a_a ∧ ¬R_b_a ∧ ¬R_c_a ∧ ¬R_a_b ∧ ¬R_b_b ∧ ¬R_c_b ∧ ¬R_a_c ∧ ¬R_b_c ∧ ¬R_c_c ∧ (¬S_a_a_a ∧ ¬S_b_a_a ∧ ¬S_c_a_a ∧ ¬S_a_b_a ∧ ¬S_b_b_a ∧ ¬S_c_b_a ∧ ¬S_a_c_a ∧ ¬S_b_c_a ∧ ¬S_c_c_a ∧ ¬S_a_a_b ∧ ¬S_b_a_b ∧ ¬S_c_a_b ∧ ¬S_a_b_b ∧ ¬S_b_b_b ∧ ¬S_c_b_b ∧ ¬S_a_c_b ∧ ¬S_b_c_b ∧ ¬S_c_c_b ∧ ¬S_a_a_c ∧ ¬S_b_a_c ∧ ¬S_c_a_c ∧ ¬S_a_b_c ∧ ¬S_b_b_c ∧ ¬S_c_b_c ∧ ¬S_a_c_c ∧ ¬S_b_c_c ∧ ¬S_c_c_c)))
+G ((n0 → X n1) ∧ (n1 → X (n3 ∨ n2)) ∧ (n2 → X n2) ∧ (n3 → X n1)) ∧ G (¬(n0 ∧ n1) ∧ ¬(n0 ∧ n2) ∧ ¬(n0 ∧ n3) ∧ ¬(n1 ∧ n2) ∧ ¬(n1 ∧ n3) ∧ ¬(n2 ∧ n3)) ∧ ((n0 ∧ X n1) → ((X Q_a_a ↔ (Q_a_a ∨ (O_a ∧ choice0_a_a))) ∧ (X Q_b_a ↔ (Q_b_a ∨ (O_a ∧ choice0_b_a))) ∧ (X Q_c_a ↔ (Q_c_a ∨ (O_a ∧ choice0_c_a))) ∧ (X Q_a_b ↔ (Q_a_b ∨ (O_b ∧ choice0_a_b))) ∧ (X Q_b_b ↔ (Q_b_b ∨ (O_b ∧ choice0_b_b))) ∧ (X Q_c_b ↔ (Q_c_b ∨ (O_b ∧ choice0_c_b))) ∧ (X Q_a_c ↔ (Q_a_c ∨ (O_c ∧ choice0_a_c))) ∧ (X Q_b_c ↔ (Q_b_c ∨ (O_c ∧ choice0_b_c))) ∧ (X Q_c_c ↔ (Q_c_c ∨ (O_c ∧ choice0_c_c))) ∧ ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ (X O_c ↔ O_c) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_c_a ↔ R_c_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b) ∧ (X R_c_b ↔ R_c_b) ∧ (X R_a_c ↔ R_a_c) ∧ (X R_b_c ↔ R_b_c) ∧ (X R_c_c ↔ R_c_c) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_c_a_a ↔ S_c_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_c_b_a ↔ S_c_b_a) ∧ (X S_a_c_a ↔ S_a_c_a) ∧ (X S_b_c_a ↔ S_b_c_a) ∧ (X S_c_c_a ↔ S_c_c_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_c_a_b ↔ S_c_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b) ∧ (X S_c_b_b ↔ S_c_b_b) ∧ (X S_a_c_b ↔ S_a_c_b) ∧ (X S_b_c_b ↔ S_b_c_b) ∧ (X S_c_c_b ↔ S_c_c_b) ∧ (X S_a_a_c ↔ S_a_a_c) ∧ (X S_b_a_c ↔ S_b_a_c) ∧ (X S_c_a_c ↔ S_c_a_c) ∧ (X S_a_b_c ↔ S_a_b_c) ∧ (X S_b_b_c ↔ S_b_b_c) ∧ (X S_c_b_c ↔ S_c_b_c) ∧ (X S_a_c_c ↔ S_a_c_c) ∧ (X S_b_c_c ↔ S_b_c_c) ∧ (X S_c_c_c ↔ S_c_c_c)))))) ∧ ((n1 ∧ X n3) → ((X S_a_a_a ↔ (S_a_a_a ∨ R_a_a)) ∧ (X S_b_a_a ↔ (S_b_a_a ∨ R_a_a)) ∧ (X S_c_a_a ↔ (S_c_a_a ∨ R_a_a)) ∧ (X S_a_b_a ↔ (S_a_b_a ∨ R_b_a)) ∧ (X S_b_b_a ↔ (S_b_b_a ∨ R_b_a)) ∧ (X S_c_b_a ↔ (S_c_b_a ∨ R_b_a)) ∧ (X S_a_c_a ↔ (S_a_c_a ∨ R_c_a)) ∧ (X S_b_c_a ↔ (S_b_c_a ∨ R_c_a)) ∧ (X S_c_c_a ↔ (S_c_c_a ∨ R_c_a)) ∧ (X S_a_a_b ↔ (S_a_a_b ∨ R_a_b)) ∧ (X S_b_a_b ↔ (S_b_a_b ∨ R_a_b)) ∧ (X S_c_a_b ↔ (S_c_a_b ∨ R_a_b)) ∧ (X S_a_b_b ↔ (S_a_b_b ∨ R_b_b)) ∧ (X S_b_b_b ↔ (S_b_b_b ∨ R_b_b)) ∧ (X S_c_b_b ↔ (S_c_b_b ∨ R_b_b)) ∧ (X S_a_c_b ↔ (S_a_c_b ∨ R_c_b)) ∧ (X S_b_c_b ↔ (S_b_c_b ∨ R_c_b)) ∧ (X S_c_c_b ↔ (S_c_c_b ∨ R_c_b)) ∧ (X S_a_a_c ↔ (S_a_a_c ∨ R_a_c)) ∧ (X S_b_a_c ↔ (S_b_a_c ∨ R_a_c)) ∧ (X S_c_a_c ↔ (S_c_a_c ∨ R_a_c)) ∧ (X S_a_b_c ↔ (S_a_b_c ∨ R_b_c)) ∧ (X S_b_b_c ↔ (S_b_b_c ∨ R_b_c)) ∧ (X S_c_b_c ↔ (S_c_b_c ∨ R_b_c)) ∧ (X S_a_c_c ↔ (S_a_c_c ∨ R_c_c)) ∧ (X S_b_c_c ↔ (S_b_c_c ∨ R_c_c)) ∧ (X S_c_c_c ↔ (S_c_c_c ∨ R_c_c)) ∧ ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ (X O_c ↔ O_c) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_c_a ↔ Q_c_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ (X Q_c_b ↔ Q_c_b) ∧ (X Q_a_c ↔ Q_a_c) ∧ (X Q_b_c ↔ Q_b_c) ∧ (X Q_c_c ↔ Q_c_c) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_c_a ↔ R_c_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b) ∧ (X R_c_b ↔ R_c_b) ∧ (X R_a_c ↔ R_a_c) ∧ (X R_b_c ↔ R_b_c) ∧ (X R_c_c ↔ R_c_c)))))) ∧ ((n1 ∧ X n2) → ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ (X O_c ↔ O_c) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_c_a ↔ Q_c_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ (X Q_c_b ↔ Q_c_b) ∧ (X Q_a_c ↔ Q_a_c) ∧ (X Q_b_c ↔ Q_b_c) ∧ (X Q_c_c ↔ Q_c_c) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_c_a ↔ R_c_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b) ∧ (X R_c_b ↔ R_c_b) ∧ (X R_a_c ↔ R_a_c) ∧ (X R_b_c ↔ R_b_c) ∧ (X R_c_c ↔ R_c_c) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_c_a_a ↔ S_c_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_c_b_a ↔ S_c_b_a) ∧ (X S_a_c_a ↔ S_a_c_a) ∧ (X S_b_c_a ↔ S_b_c_a) ∧ (X S_c_c_a ↔ S_c_c_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_c_a_b ↔ S_c_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b) ∧ (X S_c_b_b ↔ S_c_b_b) ∧ (X S_a_c_b ↔ S_a_c_b) ∧ (X S_b_c_b ↔ S_b_c_b) ∧ (X S_c_c_b ↔ S_c_c_b) ∧ (X S_a_a_c ↔ S_a_a_c) ∧ (X S_b_a_c ↔ S_b_a_c) ∧ (X S_c_a_c ↔ S_c_a_c) ∧ (X S_a_b_c ↔ S_a_b_c) ∧ (X S_b_b_c ↔ S_b_b_c) ∧ (X S_c_b_c ↔ S_c_b_c) ∧ (X S_a_c_c ↔ S_a_c_c) ∧ (X S_b_c_c ↔ S_b_c_c) ∧ (X S_c_c_c ↔ S_c_c_c)))))) ∧ ((n2 ∧ X n2) → ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ (X O_c ↔ O_c) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_c_a ↔ Q_c_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ (X Q_c_b ↔ Q_c_b) ∧ (X Q_a_c ↔ Q_a_c) ∧ (X Q_b_c ↔ Q_b_c) ∧ (X Q_c_c ↔ Q_c_c) ∧ ((X R_a_a ↔ R_a_a) ∧ (X R_b_a ↔ R_b_a) ∧ (X R_c_a ↔ R_c_a) ∧ (X R_a_b ↔ R_a_b) ∧ (X R_b_b ↔ R_b_b) ∧ (X R_c_b ↔ R_c_b) ∧ (X R_a_c ↔ R_a_c) ∧ (X R_b_c ↔ R_b_c) ∧ (X R_c_c ↔ R_c_c) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_c_a_a ↔ S_c_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_c_b_a ↔ S_c_b_a) ∧ (X S_a_c_a ↔ S_a_c_a) ∧ (X S_b_c_a ↔ S_b_c_a) ∧ (X S_c_c_a ↔ S_c_c_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_c_a_b ↔ S_c_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b) ∧ (X S_c_b_b ↔ S_c_b_b) ∧ (X S_a_c_b ↔ S_a_c_b) ∧ (X S_b_c_b ↔ S_b_c_b) ∧ (X S_c_c_b ↔ S_c_c_b) ∧ (X S_a_a_c ↔ S_a_a_c) ∧ (X S_b_a_c ↔ S_b_a_c) ∧ (X S_c_a_c ↔ S_c_a_c) ∧ (X S_a_b_c ↔ S_a_b_c) ∧ (X S_b_b_c ↔ S_b_b_c) ∧ (X S_c_b_c ↔ S_c_b_c) ∧ (X S_a_c_c ↔ S_a_c_c) ∧ (X S_b_c_c ↔ S_b_c_c) ∧ (X S_c_c_c ↔ S_c_c_c)))))) ∧ ((n3 ∧ X n1) → ((X R_a_a ↔ (R_a_a ∨ Q_a_a)) ∧ (X R_b_a ↔ (R_b_a ∨ Q_b_a)) ∧ (X R_c_a ↔ (R_c_a ∨ Q_c_a)) ∧ (X R_a_b ↔ (R_a_b ∨ Q_a_b)) ∧ (X R_b_b ↔ (R_b_b ∨ Q_b_b)) ∧ (X R_c_b ↔ (R_c_b ∨ Q_c_b)) ∧ (X R_a_c ↔ (R_a_c ∨ Q_a_c)) ∧ (X R_b_c ↔ (R_b_c ∨ Q_b_c)) ∧ (X R_c_c ↔ (R_c_c ∨ Q_c_c)) ∧ ((X O_a ↔ O_a) ∧ (X O_b ↔ O_b) ∧ (X O_c ↔ O_c) ∧ ((X Q_a_a ↔ Q_a_a) ∧ (X Q_b_a ↔ Q_b_a) ∧ (X Q_c_a ↔ Q_c_a) ∧ (X Q_a_b ↔ Q_a_b) ∧ (X Q_b_b ↔ Q_b_b) ∧ (X Q_c_b ↔ Q_c_b) ∧ (X Q_a_c ↔ Q_a_c) ∧ (X Q_b_c ↔ Q_b_c) ∧ (X Q_c_c ↔ Q_c_c) ∧ ((X S_a_a_a ↔ S_a_a_a) ∧ (X S_b_a_a ↔ S_b_a_a) ∧ (X S_c_a_a ↔ S_c_a_a) ∧ (X S_a_b_a ↔ S_a_b_a) ∧ (X S_b_b_a ↔ S_b_b_a) ∧ (X S_c_b_a ↔ S_c_b_a) ∧ (X S_a_c_a ↔ S_a_c_a) ∧ (X S_b_c_a ↔ S_b_c_a) ∧ (X S_c_c_a ↔ S_c_c_a) ∧ (X S_a_a_b ↔ S_a_a_b) ∧ (X S_b_a_b ↔ S_b_a_b) ∧ (X S_c_a_b ↔ S_c_a_b) ∧ (X S_a_b_b ↔ S_a_b_b) ∧ (X S_b_b_b ↔ S_b_b_b) ∧ (X S_c_b_b ↔ S_c_b_b) ∧ (X S_a_c_b ↔ S_a_c_b) ∧ (X S_b_c_b ↔ S_b_c_b) ∧ (X S_c_c_b ↔ S_c_c_b) ∧ (X S_a_a_c ↔ S_a_a_c) ∧ (X S_b_a_c ↔ S_b_a_c) ∧ (X S_c_a_c ↔ S_c_a_c) ∧ (X S_a_b_c ↔ S_a_b_c) ∧ (X S_b_b_c ↔ S_b_b_c) ∧ (X S_c_b_c ↔ S_c_b_c) ∧ (X S_a_c_c ↔ S_a_c_c) ∧ (X S_b_c_c ↔ S_b_c_c) ∧ (X S_c_c_c ↔ S_c_c_c)))))) ∧ (n0 ∧ ¬n1 ∧ ¬n2 ∧ ¬n3 ∧ ¬Q_a_a ∧ ¬Q_b_a ∧ ¬Q_c_a ∧ ¬Q_a_b ∧ ¬Q_b_b ∧ ¬Q_c_b ∧ ¬Q_a_c ∧ ¬Q_b_c ∧ ¬Q_c_c ∧ (¬R_a_a ∧ ¬R_b_a ∧ ¬R_c_a ∧ ¬R_a_b ∧ ¬R_b_b ∧ ¬R_c_b ∧ ¬R_a_c ∧ ¬R_b_c ∧ ¬R_c_c ∧ (¬S_a_a_a ∧ ¬S_b_a_a ∧ ¬S_c_a_a ∧ ¬S_a_b_a ∧ ¬S_b_b_a ∧ ¬S_c_b_a ∧ ¬S_a_c_a ∧ ¬S_b_c_a ∧ ¬S_c_c_a ∧ ¬S_a_a_b ∧ ¬S_b_a_b ∧ ¬S_c_a_b ∧ ¬S_a_b_b ∧ ¬S_b_b_b ∧ ¬S_c_b_b ∧ ¬S_a_c_b ∧ ¬S_b_c_b ∧ ¬S_c_c_b ∧ ¬S_a_a_c ∧ ¬S_b_a_c ∧ ¬S_c_a_c ∧ ¬S_a_b_c ∧ ¬S_b_b_c ∧ ¬S_c_b_c ∧ ¬S_a_c_c ∧ ¬S_b_c_c ∧ ¬S_c_c_c)))

src/main/scala/de/tum/workflows/Main.scala

@@ -21,7 +21,7 @@ object Main extends App with LazyLogging {
           Add(Fun("O","s"),"Q", List("x","s"))
       ),
       Loop(List(
-          ForallBlock(List("x","y","s"),
+          ForallMayBlock(List("x","y","s"),
               Add(Fun("R", List("y","s")), "S", List("x","y","s"))
           ),
           ForallBlock(List("x","s"),

src/main/scala/de/tum/workflows/WorkflowEncoding.scala

@@ -128,7 +128,7 @@ object Encoding extends LazyLogging {
       val terms = res.map(_._1) ++ staying
       Implies(And(nodeVar(e.from), Next(nodeVar(e.to))), BinOp.makeL(And.apply, terms))
     }
-    BinOp.makeL(And.apply, impls)
+    Globally(BinOp.makeL(And.apply, impls))
   }
   
   def encodeInitial(sig: Signature, g: Graph[Int, LDiEdge]) = {