First shot at the framework (it does compile).

3 files changed, 209 insertions, 54 deletions

diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java
index 41b8ef8..0b1d2e4 100644
--- a/instr-to-kodkod/src/Main.java
+++ b/instr-to-kodkod/src/Main.java
@@ -6,6 +6,9 @@ import kodkod.engine.config.*;
 import kodkod.engine.satlab.*;
 
 import kodkod.instance.*;
+
+import java.io.IOException;
+
 public class Main
 {
    private static Parameters PARAMETERS;
@@ -22,17 +25,80 @@ public class Main
       return VARIABLE_MANAGER;
    }
 
-   private static Formula get_formula (final VHDLModel model)
+   private static boolean load_levels ()
+   {
+      for (final String lvl: PARAMETERS.get_level_files())
+      {
+         try
+         {
+            VHDLLevel.add_to_model(MODEL, lvl);
+         }
+         catch (final Exception e)
+         {
+            System.err.println
+            (
+               "[E] Could not load level file \""
+               + lvl
+               + "\":"
+            );
+
+            e.printStackTrace();
+
+            return false;
+         }
+      }
+
+      return true;
+   }
+
+   private static Formula load_property ()
    {
-      final Variable w;
+      final VHDLProperty pro;
 
-      w = Variable.unary("w");
+      pro = new VHDLProperty(PARAMETERS.get_property_file());
 
-      return
-         w.join
+      try
+      {
+         return pro.generate_formula();
+      }
+      catch (final IOException e)
+      {
+         System.err.println
          (
-            model.get_predicate_as_relation("is_accessed_by")
-         ).no().forSome(w.oneOf(model.get_type_as_relation("waveform")));
+            "[E] Could not load property file \""
+            + PARAMETERS.get_property_file()
+            + "\":"
+         );
+         e.printStackTrace();
+
+         return null;
+      }
+   }
+
+   private static boolean load_models ()
+   {
+      for (final String mod: PARAMETERS.get_model_files())
+      {
+         try
+         {
+            MODEL.parse_file(mod);
+         }
+         catch (final Exception e)
+         {
+            System.err.println
+            (
+               "[E] Could not load instructions from file \""
+               + mod
+               + "\":"
+            );
+
+            e.printStackTrace();
+
+            return false;
+         }
+      }
+
+      return true;
    }
 
    public static void main (final String... args)
@@ -65,42 +131,26 @@ public class Main
       MODEL = new VHDLModel();
 
       /* 1/ Load Levels (Types + predicates) */
-      try
+      if (!load_levels())
       {
-         VHDLLevel.add_to_model
-         (
-            MODEL,
-            (
-               PARAMETERS.get_levels_directory()
-               + "/structural_level.data"
-            )
-         );
+         return;
       }
-      catch (final Exception e)
-      {
-         System.err.println("[E] Could not load structural level:");
-         e.printStackTrace();
 
+      /* 2/ Load Properties (will change 'is_used()' on predicates) */
+      /* FIXME? Currently only one property, due to the 'is_used' */
+      property = load_property();
+
+      if (property == null)
+      {
          return;
       }
 
-       /* 2/ Load Properties (will change 'is_used()' on predicates) */
-       property = get_formula(MODEL);
-       /* TODO */
-
-       /* 3/ Generate complementary model according to used predicates. */
-       /* TODO */
+      /* 3/ Generate complementary model according to used predicates. */
+      /* TODO */
 
       /* 4/ Load Model, but only for used predicates and types. */
-      try
-      {
-         MODEL.parse_file(PARAMETERS.get_model_file());
-      }
-      catch (final Exception e)
+      if (!load_models())
       {
-         System.err.println("[E] Could not load instructions:");
-         e.printStackTrace();
-
          return;
       }
 
diff --git a/instr-to-kodkod/src/Parameters.java b/instr-to-kodkod/src/Parameters.java
index 1face97..749f0fe 100644
--- a/instr-to-kodkod/src/Parameters.java
+++ b/instr-to-kodkod/src/Parameters.java
@@ -1,8 +1,13 @@
+import java.util.List;
+import java.util.ArrayList;
+
 public class Parameters
 {
-   private final String levels_dir;
-   private final String model_file;
+   private final List<String> level_files;
+   private final List<String> model_files;
+   private final String property_file;
    private final String var_prefix;
+
    private final boolean are_valid;
 
    public static void print_usage ()
@@ -11,45 +16,114 @@ public class Parameters
       (
          "Instr-to-kodkod\n"
          + "USAGE:\n"
-         + "\tjava Main <LEVELS_DIR> <INSTRUCTIONS> <VAR_PREFIX>\n"
+         + "\tjava Main <VAR_PREFIX> <FILES>+\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"
+         + "\t- <VAR_PREFIX>\tPrefix for anonymous variables (e.g. \"_anon_\").\n"
+         + "\t- <FILES>\tList of files to be loaded.\n"
          + "NOTES:\n"
-         + "\tThe properties to be verified still have to be hand coded in the"
-         + " source files (in Main.java)."
+         + "\t- One, single, property file MUST be in <FILES>.\n"
+         + "\t- Property files have a \".pro\" extension.\n"
+         + "\t- Model files have a \".mod\" extension.\n"
+         + "\t- Level files have a \".lvl\" extension.\n"
+         + "\t- The files may be given in any order."
       );
    }
 
    public Parameters (String... args)
    {
-      if (args.length != 3)
+      boolean has_pro_file, has_error;
+      String prop_file;
+
+      level_files = new ArrayList<String>();
+      model_files = new ArrayList<String>();
+
+      if (args.length < 2)
       {
          print_usage();
 
-         levels_dir = new String();
-         model_file = new String();
+         property_file = new String();
          var_prefix = new String();
+
          are_valid = false;
+
+         return;
+      }
+
+      has_pro_file = false;
+      has_error = false;
+
+      var_prefix = args[1];
+      prop_file = new String();
+
+      for (int i = 2; i < args.length; ++i)
+      {
+         if (args[i].endsWith(".lvl"))
+         {
+            level_files.add(args[i]);
+         }
+         else if (args[i].endsWith(".mod"))
+         {
+            model_files.add(args[i]);
+         }
+         else if (args[i].endsWith(".lvl"))
+         {
+            if (has_pro_file)
+            {
+               System.err.println
+               (
+                  "[E] Both files \""
+                  + prop_file
+                  + "\" and \"."
+                  + args[i]
+                  + "\" contain a property. Only one can be used at a time."
+               );
+
+               has_error = true;
+            }
+            else
+            {
+               has_pro_file = true;
+               prop_file = args[i];
+            }
+         }
+         else
+         {
+            System.err.println
+            (
+               "[E] Unknown file type \""
+               + args[i]
+               + "\"."
+            );
+
+            has_error = true;
+         }
       }
-      else
+
+      property_file = prop_file;
+
+      if (!has_pro_file)
       {
-         levels_dir = args[0];
-         model_file = args[1];
-         var_prefix = args[2];
-         are_valid = true;
+         System.err.println("[E] There was no property file.");
+
+         has_error = true;
       }
+
+      are_valid = has_error;
+   }
+
+   public List<String> get_level_files ()
+   {
+      return level_files;
    }
 
-   public String get_levels_directory ()
+   public List<String> get_model_files ()
    {
-      return levels_dir;
+      return model_files;
    }
 
-   public String get_model_file ()
+   public String get_property_file ()
    {
-      return model_file;
+      return property_file;
    }
 
    public String get_variables_prefix ()
diff --git a/instr-to-kodkod/src/VHDLProperty.java b/instr-to-kodkod/src/VHDLProperty.java
new file mode 100644
index 0000000..a91d25a
--- /dev/null
+++ b/instr-to-kodkod/src/VHDLProperty.java
@@ -0,0 +1,31 @@
+/* FIXME: Finer imports */
+import java.util.*;
+import java.io.*;
+
+import kodkod.ast.*;
+
+import org.antlr.v4.runtime.*;
+
+public class VHDLProperty
+{
+   private final String filename;
+
+   public VHDLProperty (final String filename)
+   {
+      this.filename = filename;
+   }
+
+   public Formula generate_formula ()
+   throws IOException
+   {
+      final PropertyLexer lexer;
+      final CommonTokenStream tokens;
+      final PropertyParser parser;
+
+      lexer = new PropertyLexer(CharStreams.fromFileName(filename));
+      tokens = new CommonTokenStream(lexer);
+      parser = new PropertyParser(tokens);
+
+      return parser.tag_existing().result;
+   }
+}