Starting to link parser with the program.

But apparently I messed up some kodkod logic.

5 files changed, 208 insertions, 130 deletions

diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index 59bdeb4..2611f28 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -7,14 +7,14 @@ JAVA = java
 DOWNLOADER = wget
 
 ## Java Config #################################################################
-CLASSPATH = "kodkod.jar:./src/:org.sat4j.core.jar"
+CLASSPATH = "kodkod.jar:./src/:./parser/:org.sat4j.core.jar:antlr-4.7-complete.jar"
 
 ## Dependencies ################################################################
 JAR_SOURCE = https://noot-noot.org/onera_2017/jar/
 REQUIRED_JARS = kodkod.jar org.sat4j.core.jar antlr-4.7-complete.jar
 
 ## Makefile Magic ##############################################################
-SOURCES = $(wildcard src/*.java)
+SOURCES = $(wildcard src/*.java parser/*.java)
 CLASSES = $(SOURCES:.java=.class)
 
 ## Makefile Rules ##############################################################
diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4
index 5394570..d685790 100644
--- a/instr-to-kodkod/parser/PropertyParser.g4
+++ b/instr-to-kodkod/parser/PropertyParser.g4
@@ -18,7 +18,6 @@ options
 @members
 {
    /* of the class */
-
 }
 
 prog:
@@ -56,7 +55,7 @@ id_list
       (WS)+
       var=ID
       {
-         result.add(VARIABLE_SET.get_variable($var.text));
+         result.add(Main.get_variable_manager().get_variable($var.text));
       }
    )*
 
@@ -79,7 +78,7 @@ sl_predicate
 
    {
       /* TODO */
-      result = null;
+      $result = null;
    }
 ;
 
@@ -176,12 +175,12 @@ sl_exists_operator
       $result =
          ($f.result).forSome
          (
-            VARIABLE_SET.get_variable
+            Main.get_variable_manager().get_variable
             (
                ($var.text)
             ).in
             (
-               MODEL.get_type_as_relation(($type.text))
+               Main.get_model().get_type_as_relation(($type.text))
             )
          );
    }
@@ -201,12 +200,12 @@ sl_forall_operator
       $result =
          ($f.result).forAll
          (
-            VARIABLE_SET.get_variable
+            Main.get_variable_manager().get_variable
             (
                ($var.text)
             ).in
             (
-               MODEL.get_type_as_relation(($type.text))
+               Main.get_model().get_type_as_relation(($type.text))
             )
          );
    }
@@ -220,7 +219,7 @@ sl_ctl_verifies_operator
    {
       final Variable root_node;
 
-      root_node = VARIABLE_SET.generate_new_state_variable();
+      root_node = Main.get_variable_manager().generate_new_variable();
    }
 
    :
@@ -237,11 +236,11 @@ sl_ctl_verifies_operator
          (
             root_node.oneOf
             (
-               MODEL.get_type_as_relation("node").in
+               Main.get_model().get_type_as_relation("node").in
                (
-                  VARIABLE_SET.get_variable(($ps.text)).join
+                  Main.get_variable_manager().get_variable(($ps.text)).join
                   (
-                     MODEL.get_predicate_as_relation("start_node")
+                     Main.get_model().get_predicate_as_relation("start_node")
                   )
                )
             )
@@ -297,7 +296,7 @@ sl_formula
 /******************************************************************************/
 /** Behavioral Level **********************************************************/
 /******************************************************************************/
-bl_predicate [Variable current_state]
+bl_predicate [Variable current_node]
    returns [Formula result]:
 
    (WS)* L_PAREN
@@ -307,11 +306,11 @@ bl_predicate [Variable current_state]
 
    {
       /* TODO */
-      result = null;
+      $result = null;
    }
 ;
 
-bl_formula_list [Variable current_state]
+bl_formula_list [Variable current_node]
    returns [List<Formula> list]
 
    @init
@@ -321,7 +320,7 @@ bl_formula_list [Variable current_state]
 
    :
    (
-      bl_formula[current_state]
+      bl_formula[current_node]
       {
          result.add(($bl_formula.result));
       }
@@ -333,12 +332,12 @@ bl_formula_list [Variable current_state]
 ;
 
 /**** First Order Expressions *************************************************/
-bl_and_operator [Variable current_state]
+bl_and_operator [Variable current_node]
    returns [Formula result]:
 
    (WS)* AND_OPERATOR_KW
-      bl_formula[current_state]
-      bl_formula_list[current_state]
+      bl_formula[current_node]
+      bl_formula_list[current_node]
    (WS)* R_PAREN
 
    {
@@ -347,12 +346,12 @@ bl_and_operator [Variable current_state]
    }
 ;
 
-bl_or_operator [Variable current_state]
+bl_or_operator [Variable current_node]
    returns [Formula result]:
 
    (WS)* OR_OPERATOR_KW
-      bl_formula[current_state]
-      bl_formula_list[current_state]
+      bl_formula[current_node]
+      bl_formula_list[current_node]
    (WS)* R_PAREN
 
    {
@@ -361,11 +360,11 @@ bl_or_operator [Variable current_state]
    }
 ;
 
-bl_not_operator [Variable current_state]
+bl_not_operator [Variable current_node]
    returns [Formula result]:
 
    (WS)* NOT_OPERATOR_KW
-      bl_formula[current_state]
+      bl_formula[current_node]
    (WS)* R_PAREN
 
    {
@@ -374,12 +373,12 @@ bl_not_operator [Variable current_state]
    }
 ;
 
-bl_implies_operator [Variable current_state]
+bl_implies_operator [Variable current_node]
    returns [Formula result]:
 
    (WS)* IMPLIES_OPERATOR_KW
-      a=bl_formula[current_state]
-      b=bl_formula[current_state]
+      a=bl_formula[current_node]
+      b=bl_formula[current_node]
    (WS)* R_PAREN
 
    {
@@ -389,19 +388,19 @@ bl_implies_operator [Variable current_state]
 ;
 
 /**** Computation Tree Logic Expressions **************************************/
-bl_ax_operator [Variable current_state]
+bl_ax_operator [Variable current_node]
    returns [Formula result]
 
    @init
    {
-      final Variable next_state;
+      final Variable next_node;
 
-      next_state = VARIABLE_SET.generate_new_state_variable();
+      next_node = Main.get_variable_manager().generate_new_variable();
    }
 
    :
    (WS)* AX_OPERATOR_KW
-      bl_formula[next_state]
+      bl_formula[next_node]
    (WS)* R_PAREN
 
    {
@@ -409,30 +408,30 @@ bl_ax_operator [Variable current_state]
       $result =
          ($bl_formula.result).forAll
          (
-            next_state.in
+            next_node.in
             (
-               current_state.join
+               current_node.join
                (
-                  MODEL.get_predicate_as_relation("node_connect")
+                  Main.get_model().get_predicate_as_relation("node_connect")
                )
-            );
+            )
          );
    }
 ;
 
-bl_ex_operator [Variable current_state]
+bl_ex_operator [Variable current_node]
    returns [Formula result]
 
    @init
    {
-      final Variable next_state;
+      final Variable next_node;
 
-      next_state = VARIABLE_SET.generate_new_state_variable();
+      next_node = Main.get_variable_manager().generate_new_variable();
    }
 
    :
    (WS)* EX_OPERATOR_KW
-      bl_formula[next_state]
+      bl_formula[next_node]
    (WS)* R_PAREN
 
    {
@@ -440,30 +439,30 @@ bl_ex_operator [Variable current_state]
       $result =
          ($bl_formula.result).forSome
          (
-            next_state.in
+            next_node.in
             (
-               current_state.join
+               current_node.join
                (
-                  MODEL.get_predicate_as_relation("node_connect")
+                  Main.get_model().get_predicate_as_relation("node_connect")
                )
-            );
+            )
          );
    }
 ;
 
-bl_ag_operator [Variable current_state]
+bl_ag_operator [Variable current_node]
    returns [Formula result]
 
    @init
    {
-      final Variable next_state;
+      final Variable next_node;
 
-      next_state = VARIABLE_SET.generate_new_state_variable();
+      next_node = Main.get_variable_manager().generate_new_variable();
    }
 
    :
    (WS)* AG_OPERATOR_KW
-      bl_formula[next_state]
+      bl_formula[next_node]
    (WS)* R_PAREN
 
    {
@@ -471,37 +470,37 @@ bl_ag_operator [Variable current_state]
       $result =
          ($bl_formula.result).forAll
          (
-            next_state.in
+            next_node.in
             (
-               current_state.join
+               current_node.join
                (
-                  MODEL.get_predicate_as_relation
+                  Main.get_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")
-               ).
+                  Main.get_model().get_predicate_as_relation("contains_node")
+               )
             )
-         )
+         );
    }
 ;
 
-bl_eg_operator [Variable current_state]
+bl_eg_operator [Variable current_node]
    returns [Formula result]
 
    @init
    {
-      final Variable next_state, chosen_path;
+      final Variable next_node, chosen_path;
 
-      next_state = VARIABLE_SET.generate_new_state_variable();
-      chosen_path = VARIABLE_SET.generate_new_state_variable();
+      next_node = Main.get_variable_manager().generate_new_variable();
+      chosen_path = Main.get_variable_manager().generate_new_variable();
    }
 
    :
    (WS)* EG_OPERATOR_KW
-      bl_formula[next_state]
+      bl_formula[next_node]
    (WS)* R_PAREN
 
    {
@@ -509,20 +508,20 @@ bl_eg_operator [Variable current_state]
       $result =
          ($bl_formula.result).forAll
          (
-            next_state.in
+            next_node.in
             (
                chosen_path.join
                (
-                  MODEL.get_predicate_as_relation("contains_node")
-               ).
+                  Main.get_model().get_predicate_as_relation("contains_node")
+               )
             )
          ).forSome
          (
             chosen_path.in
             (
-               current_state.join
+               current_node.join
                (
-                  MODEL.get_predicate_as_relation
+                  Main.get_model().get_predicate_as_relation
                   (
                      "is_path_of"
                   ).transpose() /* (is_path_of path node), we want the path. */
@@ -532,20 +531,20 @@ bl_eg_operator [Variable current_state]
    }
 ;
 
-bl_af_operator [Variable current_state]
+bl_af_operator [Variable current_node]
    returns [Formula result]
 
    @init
    {
-      final Variable next_state, chosen_path;
+      final Variable next_node, chosen_path;
 
-      next_state = VARIABLE_SET.generate_new_state_variable();
-      chosen_path = VARIABLE_SET.generate_new_state_variable();
+      next_node = Main.get_variable_manager().generate_new_variable();
+      chosen_path = Main.get_variable_manager().generate_new_variable();
    }
 
    :
    (WS)* AF_OPERATOR_KW
-      bl_formula[next_state]
+      bl_formula[next_node]
    (WS)* R_PAREN
 
    {
@@ -553,20 +552,20 @@ bl_af_operator [Variable current_state]
       $result =
          ($bl_formula.result).forSome
          (
-            next_state.in
+            next_node.in
             (
                chosen_path.join
                (
-                  MODEL.get_predicate_as_relation("contains_node")
-               ).
+                  Main.get_model().get_predicate_as_relation("contains_node")
+               )
             )
          ).forAll
          (
             chosen_path.in
             (
-               current_state.join
+               current_node.join
                (
-                  MODEL.get_predicate_as_relation
+                  Main.get_model().get_predicate_as_relation
                   (
                      "is_path_of"
                   ).transpose() /* (is_path_of path node), we want the path. */
@@ -576,20 +575,20 @@ bl_af_operator [Variable current_state]
    }
 ;
 
-bl_ef_operator [Variable current_state]
+bl_ef_operator [Variable current_node]
    returns [Formula result]
 
    @init
    {
-      final Variable next_state, chosen_path;
+      final Variable next_node, chosen_path;
 
-      next_state = VARIABLE_SET.generate_new_state_variable();
-      chosen_path = VARIABLE_SET.generate_new_state_variable();
+      next_node = Main.get_variable_manager().generate_new_variable();
+      chosen_path = Main.get_variable_manager().generate_new_variable();
    }
 
    :
    (WS)* EF_OPERATOR_KW
-      bl_formula[next_state]
+      bl_formula[next_node]
    (WS)* R_PAREN
 
    {
@@ -597,20 +596,20 @@ bl_ef_operator [Variable current_state]
       $result =
          ($bl_formula.result).forSome
          (
-            next_state.in
+            next_node.in
             (
                chosen_path.join
                (
-                  MODEL.get_predicate_as_relation("contains_node")
-               ).
+                  Main.get_model().get_predicate_as_relation("contains_node")
+               )
             )
          ).forSome
          (
             chosen_path.in
             (
-               current_state.join
+               current_node.join
                (
-                  MODEL.get_predicate_as_relation
+                  Main.get_model().get_predicate_as_relation
                   (
                      "is_path_of"
                   ).transpose() /* (is_path_of path node), we want the path. */
@@ -620,22 +619,22 @@ bl_ef_operator [Variable current_state]
    }
 ;
 
-bl_au_operator [Variable current_state]
+bl_au_operator [Variable current_node]
    returns [Formula result]
 
    @init
    {
-      final Variable f1_state, f2_state, chosen_path;
+      final Variable f1_node, f2_node, 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();
+      f1_node = Main.get_variable_manager().generate_new_variable();
+      f2_node = Main.get_variable_manager().generate_new_variable();
+      chosen_path = Main.get_variable_manager().generate_new_variable();
    }
 
    :
    (WS)* AU_OPERATOR_KW
-      f1=bl_formula[f1_state]
-      f2=bl_formula[f2_state]
+      f1=bl_formula[f1_node]
+      f2=bl_formula[f2_node]
    (WS)* R_PAREN
 
    {
@@ -643,57 +642,57 @@ bl_au_operator [Variable current_state]
       $result =
          ($f1.result).forAll
          (
-            f1_state.in
+            f1_node.in
             (
-               f2_state.join
+               f2_node.join
                (
                   chosen_path.join
                   (
-                     MODEL.get_predicate_as_relation("is_before")
+                     Main.get_model().get_predicate_as_relation("is_before")
                   ).transpose()
                )
-            );
+            )
          ).and
          (
             ($f2.result)
          ).forSome
          (
-            f2_state.in
+            f2_node.in
             (
                chosen_path.join
                (
-                  MODEL.get_predicate_as_relation("contains_node")
+                  Main.get_model().get_predicate_as_relation("contains_node")
                )
             )
          ).forAll
          (
             chosen_path.in
             (
-               current_state.join
+               current_node.join
                (
-                  MODEL.get_predicate_as_relation("is_path_of").transpose()
+                  Main.get_model().get_predicate_as_relation("is_path_of").transpose()
                )
             )
          );
    }
 ;
 
-bl_eu_operator [Variable current_state]
+bl_eu_operator [Variable current_node]
    returns [Formula result]
 
    @init
    {
-      final Variable f1_state, f2_state, chosen_path;
+      final Variable f1_node, f2_node, 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();
+      f1_node = Main.get_variable_manager().generate_new_variable();
+      f2_node = Main.get_variable_manager().generate_new_variable();
+      chosen_path = Main.get_variable_manager().generate_new_variable();
    }
 
    :
    (WS)* EU_OPERATOR_KW
-      f1=bl_formula[f1_state]
-      f2=bl_formula[f2_state]
+      f1=bl_formula[f1_node]
+      f2=bl_formula[f2_node]
    (WS)* R_PAREN
 
    {
@@ -701,34 +700,34 @@ bl_eu_operator [Variable current_state]
       $result =
          ($f1.result).forAll
          (
-            f1_state.in
+            f1_node.in
             (
-               f2_state.join
+               f2_node.join
                (
                   chosen_path.join
                   (
-                     MODEL.get_predicate_as_relation("is_before")
+                     Main.get_model().get_predicate_as_relation("is_before")
                   ).transpose()
                )
-            );
+            )
          ).and(
             ($f2.result)
          ).forSome
          (
-            f2_state.in
+            f2_node.in
             (
                chosen_path.join
                (
-                  MODEL.get_predicate_as_relation("contains_node")
+                  Main.get_model().get_predicate_as_relation("contains_node")
                )
             )
          ).forSome
          (
             chosen_path.in
             (
-               current_state.join
+               current_node.join
                (
-                  MODEL.get_predicate_as_relation("is_path_of").transpose()
+                  Main.get_model().get_predicate_as_relation("is_path_of").transpose()
                )
             )
          );
@@ -736,58 +735,58 @@ bl_eu_operator [Variable current_state]
 ;
 
 /**** Formula Definition ******************************************************/
-bl_formula [Variable current_state]
+bl_formula [Variable current_node]
    returns [Formula result]:
 
-   bl_predicate[current_state]
+   bl_predicate[current_node]
    {
       $result = ($bl_predicate.result);
    }
-   | bl_and_operator[current_state]
+   | bl_and_operator[current_node]
    {
       $result = ($bl_and_operator.result);
    }
-   | bl_or_operator[current_state]
+   | bl_or_operator[current_node]
    {
       $result = ($bl_or_operator.result);
    }
-   | bl_not_operator[current_state]
+   | bl_not_operator[current_node]
    {
       $result = ($bl_not_operator.result);
    }
-   | bl_implies_operator[current_state]
+   | bl_implies_operator[current_node]
    {
       $result = ($bl_implies_operator.result);
    }
-   | bl_ax_operator[current_state]
+   | bl_ax_operator[current_node]
    {
       $result = ($bl_ax_operator.result);
    }
-   | bl_ex_operator[current_state]
+   | bl_ex_operator[current_node]
    {
       $result = ($bl_ex_operator.result);
    }
-   | bl_ag_operator[current_state]
+   | bl_ag_operator[current_node]
    {
       $result = ($bl_ag_operator.result);
    }
-   | bl_eg_operator[current_state]
+   | bl_eg_operator[current_node]
    {
       $result = ($bl_eg_operator.result);
    }
-   | bl_af_operator[current_state]
+   | bl_af_operator[current_node]
    {
       $result = ($bl_af_operator.result);
    }
-   | bl_ef_operator[current_state]
+   | bl_ef_operator[current_node]
    {
       $result = ($bl_ef_operator.result);
    }
-   | bl_au_operator[current_state]
+   | bl_au_operator[current_node]
    {
       $result = ($bl_au_operator.result);
    }
-   | bl_eu_operator[current_state]
+   | bl_eu_operator[current_node]
    {
       $result = ($bl_eu_operator.result);
    }
diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java
index ba9ebaa..41b8ef8 100644
--- a/instr-to-kodkod/src/Main.java
+++ b/instr-to-kodkod/src/Main.java
@@ -10,6 +10,17 @@ public class Main
 {
    private static Parameters PARAMETERS;
    private static VHDLModel MODEL;
+   private static VariableManager VARIABLE_MANAGER;
+
+   public static VHDLModel get_model ()
+   {
+      return MODEL;
+   }
+
+   public static VariableManager get_variable_manager ()
+   {
+      return VARIABLE_MANAGER;
+   }
 
    private static Formula get_formula (final VHDLModel model)
    {
@@ -49,6 +60,8 @@ public class Main
          return;
       }
 
+      VARIABLE_MANAGER = new VariableManager(PARAMETERS.get_variables_prefix());
+
       MODEL = new VHDLModel();
 
       /* 1/ Load Levels (Types + predicates) */
diff --git a/instr-to-kodkod/src/Parameters.java b/instr-to-kodkod/src/Parameters.java
index e9dc648..1face97 100644
--- a/instr-to-kodkod/src/Parameters.java
+++ b/instr-to-kodkod/src/Parameters.java
@@ -2,6 +2,7 @@ public class Parameters
 {
    private final String levels_dir;
    private final String model_file;
+   private final String var_prefix;
    private final boolean are_valid;
 
    public static void print_usage ()
@@ -10,10 +11,11 @@ public class Parameters
       (
          "Instr-to-kodkod\n"
          + "USAGE:\n"
-         + "\tjava Main <LEVELS_DIR> <INSTRUCTIONS>\n"
+         + "\tjava Main <LEVELS_DIR> <INSTRUCTIONS> <VAR_PREFIX>\n"
          + "PARAMETERS:\n"
          + "\t<LEVELS_DIR>\tDirectory containing the level definitions.\n"
          + "\t<INSTRUCTIONS>\tInstruction file describing the model.\n"
+         + "\t<VAR_PREFIX>\tPrefix for anonymous variables (e.g. \"_anon_\").\n"
          + "NOTES:\n"
          + "\tThe properties to be verified still have to be hand coded in the"
          + " source files (in Main.java)."
@@ -22,18 +24,20 @@ public class Parameters
 
    public Parameters (String... args)
    {
-      if (args.length != 2)
+      if (args.length != 3)
       {
          print_usage();
 
          levels_dir = new String();
          model_file = new String();
+         var_prefix = new String();
          are_valid = false;
       }
       else
       {
          levels_dir = args[0];
          model_file = args[1];
+         var_prefix = args[2];
          are_valid = true;
       }
    }
@@ -48,6 +52,11 @@ public class Parameters
       return model_file;
    }
 
+   public String get_variables_prefix ()
+   {
+      return var_prefix;
+   }
+
    public boolean are_valid ()
    {
       return are_valid;
diff --git a/instr-to-kodkod/src/VariableManager.java b/instr-to-kodkod/src/VariableManager.java
new file mode 100644
index 0000000..381a774
--- /dev/null
+++ b/instr-to-kodkod/src/VariableManager.java
@@ -0,0 +1,57 @@
+/* FIXME: finer imports. */
+import java.util.*;
+
+import kodkod.ast.*;
+
+public class VariableManager
+{
+   private final Map<String, Variable> from_string;
+   private final Map<String, String> tags;
+   private final String var_prefix;
+   private int next_id;
+
+   public VariableManager (final String var_prefix)
+   {
+      from_string = new HashMap<String, Variable>();
+      tags = new HashMap<String, String>();
+
+      this.var_prefix = var_prefix;
+   }
+
+   private String generate_new_id ()
+   {
+      final String result;
+
+      result = var_prefix + next_id;
+
+      next_id += 1;
+
+      return result;
+   }
+
+   public Variable get_variable (final String name)
+   {
+      Variable result;
+
+      result = from_string.get(name);
+
+      if (result == null)
+      {
+         result = Variable.unary(name);
+
+         from_string.put(name, result);
+      }
+
+      return result;
+   }
+
+   public Variable generate_new_variable ()
+   {
+      return get_variable(generate_new_id());
+   }
+
+   public void tag_variable (final String name, final String tag)
+   {
+      tags.put(name, tag);
+   }
+}