Starting to link parser with the program.

But apparently I messed up some kodkod logic.

3 files changed, 81 insertions, 2 deletions

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);
+   }
+}