Solves previous problem by changing path def.

Instead of the path "n1 -> n2 -> n3" being "n2 -> n3" a path starting
from n1, it's now "n1 -> n2 -> n3" (still starting from n1).

2 files changed, 188 insertions, 66 deletions

diff --git a/cfg-to-paths/src/Main.java b/cfg-to-paths/src/Main.java
index 481d53f..853983a 100644
--- a/cfg-to-paths/src/Main.java
+++ b/cfg-to-paths/src/Main.java
@@ -97,7 +97,7 @@ public class Main
       out.write("(add_element path " + id + ")\n");
       out.write("(is_path_of " + id + " " + tuple.get(0) + ")\n");
 
-      for (int i = 1; i < tuple_size; ++i)
+      for (int i = 0; i < tuple_size; ++i)
       {
          out.write("(contains_node " + id + " " + tuple.get(i) + ")\n");
 
diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4
index 2df87cb..4aeeffc 100644
--- a/instr-to-kodkod/parser/PropertyParser.g4
+++ b/instr-to-kodkod/parser/PropertyParser.g4
@@ -18,6 +18,7 @@ options
 @members
 {
    /* of the class */
+
 }
 
 prog:
@@ -429,7 +430,6 @@ bl_ex_operator [Variable current_state]
    }
 ;
 
-
 bl_ag_operator [Variable current_state]
    returns [Formula result]:
 
@@ -447,135 +447,257 @@ bl_ag_operator [Variable current_state]
    {
       /* TODO */
       $result =
-         Formula.replace /* That does not seem to exist. */
-         (
-            next_state,
-            current_state,
-            $bl_formula
-         ).and
+         $bl_formula.forAll
          (
-            $bl_formula.forAll
-            (
-               {n | <p, n> \in contains_node}
-            ).forAll
+            next_state.in
             (
-               {p | <p, current_node> \in is_path_of}
+               current_state.join
+               (
+                  MODEL.get_predicate_as_relation
+                  (
+                     "is_path_of"
+                  ).transpose() /* (is_path_of path node), we want the path. */
+               ).join
+               (
+                  MODEL.get_predicate_as_relation("contains_node")
+               ).
             )
          )
    }
 ;
 
-bl_eg_operator returns [Formula result]:
-   (WS)* EG_OPERATOR_KW bl_formula (WS)* R_PAREN
+bl_eg_operator [Variable current_state]
+   returns [Formula result]:
+
+   @init
+   {
+      final Variable next_state, chosen_path;
+
+      next_state = VARIABLE_SET.generate_new_state_variable();
+      chosen_path = VARIABLE_SET.generate_new_state_variable();
+   }
+
+   (WS)* EG_OPERATOR_KW
+      bl_formula[next_state]
+   (WS)* R_PAREN
+
    {
       /* TODO */
       $result =
-         $bl_formula.forSome
-         (
-            current_node
-         ).and
+         $bl_formula.forAll
          (
-            $bl_formula.forSome
+            next_state.in
             (
-               {n | <p, n> \in contains_node}
-            ).forAll
+               chosen_path.join
+               (
+                  MODEL.get_predicate_as_relation("contains_node")
+               ).
+            )
+         ).forSome
+         (
+            chosen_path.in
             (
-               {p | <p, current_node> \in is_path_of}
+               current_state.join
+               (
+                  MODEL.get_predicate_as_relation
+                  (
+                     "is_path_of"
+                  ).transpose() /* (is_path_of path node), we want the path. */
+               )
             )
          );
    }
 ;
 
-bl_af_operator returns [Formula result]:
-   (WS)* AF_OPERATOR_KW bl_formula (WS)* R_PAREN
+bl_af_operator [Variable current_state]
+   returns [Formula result]:
+
+   @init
+   {
+      final Variable next_state, chosen_path;
+
+      next_state = VARIABLE_SET.generate_new_state_variable();
+      chosen_path = VARIABLE_SET.generate_new_state_variable();
+   }
+
+   (WS)* AF_OPERATOR_KW
+      bl_formula[next_state]
+   (WS)* R_PAREN
+
    {
       /* TODO */
       $result =
          $bl_formula.forSome
          (
-            current_node
-         ).or
-         (
-            $bl_formula.forAll
+            next_state.in
             (
-               {n | <p, n> \in contains_node}
-            ).forSome
+               chosen_path.join
+               (
+                  MODEL.get_predicate_as_relation("contains_node")
+               ).
+            )
+         ).forAll
+         (
+            chosen_path.in
             (
-               {p | <p, current_node> \in is_path_of}
+               current_state.join
+               (
+                  MODEL.get_predicate_as_relation
+                  (
+                     "is_path_of"
+                  ).transpose() /* (is_path_of path node), we want the path. */
+               )
             )
          );
    }
 ;
 
-bl_ef_operator returns [Formula result]:
-   (WS)* EF_OPERATOR_KW bl_formula (WS)* R_PAREN
+bl_ef_operator [Variable current_state]
+   returns [Formula result]:
+
+   @init
+   {
+      final Variable next_state, chosen_path;
+
+      next_state = VARIABLE_SET.generate_new_state_variable();
+      chosen_path = VARIABLE_SET.generate_new_state_variable();
+   }
+
+   (WS)* EF_OPERATOR_KW
+      bl_formula[next_state]
+   (WS)* R_PAREN
+
    {
       /* TODO */
       $result =
          $bl_formula.forSome
          (
-            current_node
-         ).or
-         (
-            $bl_formula.forSome
+            next_state.in
             (
-               {n | <p, n> \in contains_node}
-            ).forSome
+               chosen_path.join
+               (
+                  MODEL.get_predicate_as_relation("contains_node")
+               ).
+            )
+         ).forSome
+         (
+            chosen_path.in
             (
-               {p | <p, current_node> \in is_path_of}
+               current_state.join
+               (
+                  MODEL.get_predicate_as_relation
+                  (
+                     "is_path_of"
+                  ).transpose() /* (is_path_of path node), we want the path. */
+               )
             )
          );
    }
 ;
 
-bl_au_operator returns [Formula result]: (WS)* AU_OPERATOR_KW f1=bl_formula f2=bl_formula (WS)* R_PAREN
+bl_au_operator [Variable current_state]
+   returns [Formula result]:
+
+   @init
+   {
+      final Variable f1_state, f2_state, chosen_path;
+
+      f1_state = VARIABLE_SET.generate_new_state_variable();
+      f2_state = VARIABLE_SET.generate_new_state_variable();
+      chosen_path = VARIABLE_SET.generate_new_state_variable();
+   }
+
+   (WS)* AU_OPERATOR_KW
+      f1=bl_formula[f1_state]
+      f2=bl_formula[f2_state]
+   (WS)* R_PAREN
+
    {
       /* TODO */
       $result =
-         $f1.forSome
+         $f1.forAll
          (
-            current_node
-         ).and
-         (
-            $f2.and
+            f1_state.in
             (
-               $f1.forAll
+               f2_state.join
                (
-                  {t | <p, t, n> \in is_before}
+                  chosen_path.join
+                  (
+                     MODEL.get_predicate_as_relation("is_before")
+                  ).transpose()
                )
-            ).forSome
+            );
+         ).forSome
+         (
+            f2_state.in
             (
-               {n | <p, n> \in contains_node}
-            ).forAll
+               chosen_path.join
+               (
+                  MODEL.get_predicate_as_relation("contains_node")
+               )
+            )
+         ).forAll
+         (
+            chosen_path.in
             (
-               {p | <p, current_node> \in is_path_of}
+               current_state.join
+               (
+                  MODEL.get_predicate_as_relation("is_path_of").transpose()
+               )
             )
          );
    }
 ;
 
-bl_eu_operator returns [Formula result]:
-   (WS)* EU_OPERATOR_KW f1=bl_formula f2=bl_formula (WS)* R_PAREN
+bl_eu_operator [Variable current_state]
+   returns [Formula result]:
+
+   @init
+   {
+      final Variable f1_state, f2_state, chosen_path;
+
+      f1_state = VARIABLE_SET.generate_new_state_variable();
+      f2_state = VARIABLE_SET.generate_new_state_variable();
+      chosen_path = VARIABLE_SET.generate_new_state_variable();
+   }
+
+   (WS)* EU_OPERATOR_KW
+      f1=bl_formula[f1_state]
+      f2=bl_formula[f2_state]
+   (WS)* R_PAREN
+
    {
       /* TODO */
       $result =
-         $f1.forSome
-         (
-            current_node
-         ).and
+         $f1.forAll
          (
-            $f2.and
+            f1_state.in
             (
-               $f1.forAll
+               f2_state.join
                (
-                  {t | <p, t, n> \in is_before}
+                  chosen_path.join
+                  (
+                     MODEL.get_predicate_as_relation("is_before")
+                  ).transpose()
                )
-            ).forSome
+            );
+         ).forSome
+         (
+            f2_state.in
             (
-               {n | <p, n> \in contains_node}
-            ).forSome
+               chosen_path.join
+               (
+                  MODEL.get_predicate_as_relation("contains_node")
+               )
+            )
+         ).forSome
+         (
+            chosen_path.in
             (
-               {p | <p, current_node> \in is_path_of}
+               current_state.join
+               (
+                  MODEL.get_predicate_as_relation("is_path_of").transpose()
+               )
             )
          );
    }