agents

results/workflow1agent.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 O_a ↔ O_a) ∧ (X R_a_a ↔ R_a_a) ∧ (X S_a_a_a ↔ S_a_a_a))) ∧ ((n1 ∧ X n3) → ((X S_a_a_a ↔ (S_a_a_a ∨ (R_a_a ∧ choice1_a_a_a))) ∧ (X O_a ↔ O_a) ∧ (X Q_a_a ↔ Q_a_a) ∧ (X R_a_a ↔ R_a_a))) ∧ ((n1 ∧ X n2) → ((X O_a ↔ O_a) ∧ (X Q_a_a ↔ Q_a_a) ∧ (X R_a_a ↔ R_a_a) ∧ (X S_a_a_a ↔ S_a_a_a))) ∧ ((n2 ∧ X n2) → ((X O_a ↔ O_a) ∧ (X Q_a_a ↔ Q_a_a) ∧ (X R_a_a ↔ R_a_a) ∧ (X S_a_a_a ↔ S_a_a_a))) ∧ ((n3 ∧ X n1) → ((X R_a_a ↔ (R_a_a ∨ Q_a_a)) ∧ (X O_a ↔ O_a) ∧ (X Q_a_a ↔ Q_a_a) ∧ (X S_a_a_a ↔ S_a_a_a))) ∧ (n0 ∧ ¬n1 ∧ ¬n2 ∧ ¬n3 ∧ ¬Q_a_a ∧ ¬R_a_a ∧ ¬S_a_a_a)
+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)) ∧ 
+G (
+    ((n0 ∧ X n1) → 
+        ((X Q_a_a ↔ (Q_a_a ∨ (O_a ∧ choice0_a_a))) ∧ 
+        (X O_a ↔ O_a) ∧ 
+        (X R_a_a ↔ R_a_a) ∧ 
+        (X S_a_a_a ↔ S_a_a_a))) ∧ 
+    ((n1 ∧ X n3) → 
+        ((X S_a_a_a ↔ (S_a_a_a ∨ R_a_a)) ∧ 
+        (X O_a ↔ O_a) ∧ 
+        (X Q_a_a ↔ Q_a_a) ∧ 
+        (X R_a_a ↔ R_a_a))) ∧ 
+    ((n1 ∧ X n2) → 
+        ((X O_a ↔ O_a) ∧ 
+        (X Q_a_a ↔ Q_a_a) ∧ 
+        (X R_a_a ↔ R_a_a) ∧ 
+        (X S_a_a_a ↔ S_a_a_a))) ∧ 
+    ((n2 ∧ X n2) → 
+        ((X O_a ↔ O_a) ∧ 
+        (X Q_a_a ↔ Q_a_a) ∧ 
+        (X R_a_a ↔ R_a_a) ∧ 
+        (X S_a_a_a ↔ S_a_a_a))) ∧ 
+    ((n3 ∧ X n1) → 
+        ((X R_a_a ↔ (R_a_a ∨ Q_a_a)) ∧ 
+        (X O_a ↔ O_a) ∧ 
+        (X Q_a_a ↔ Q_a_a) ∧ 
+        (X S_a_a_a ↔ S_a_a_a)))) ∧ 
+
+n0 ∧ ¬n1 ∧ ¬n2 ∧ ¬n3 ∧ ¬Q_a_a ∧ ¬R_a_a ∧ ¬S_a_a_a

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)))
+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)) ∧ G (((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 ∧ choice1_a_a_a))) ∧ (X S_b_a_a ↔ (S_b_a_a ∨ (R_a_a ∧ choice1_b_a_a))) ∧ (X S_a_b_a ↔ (S_a_b_a ∨ (R_b_a ∧ choice1_a_b_a))) ∧ (X S_b_b_a ↔ (S_b_b_a ∨ (R_b_a ∧ choice1_b_b_a))) ∧ (X S_a_a_b ↔ (S_a_a_b ∨ (R_a_b ∧ choice1_a_a_b))) ∧ (X S_b_a_b ↔ (S_b_a_b ∨ (R_a_b ∧ choice1_b_a_b))) ∧ (X S_a_b_b ↔ (S_a_b_b ∨ (R_b_b ∧ choice1_a_b_b))) ∧ (X S_b_b_b ↔ (S_b_b_b ∨ (R_b_b ∧ choice1_b_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))

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

@@ -34,8 +34,9 @@ object Main extends App with LazyLogging {
   
   val res = Encoding.toFOLTL(w)
   
-  // agent list
-  val res2 = LTL.eliminateUniversals(res, List("a"))
+  // agent list to execute the workflow for (should not clash with variables in the workflow)
+  val agents:List[Var] = List("a","b","c")
+  val res2 = LTL.eliminateUniversals(res, agents)
   val res3 = LTL.eliminatePredicates(res2)
   logger.info(s"Complete formula: $res3")
 }
\ No newline at end of file