First shot at the framework (it does compile).

11 files changed, 390 insertions, 64 deletions

diff --git a/data/instructions/example_process.pl.kk b/data/instructions/example_process.pl.kk
new file mode 100644
index 0000000..c4f07b3
--- /dev/null
+++ b/data/instructions/example_process.pl.kk
@@ -0,0 +1,88 @@
+(add_element path p237_0)
+(is_path_of p237_0 237)
+(contains_node p237_0 262)
+(is_before p237_0 262 263)
+(contains_node p237_0 263)
+(add_element path p237_1)
+(is_path_of p237_1 262)
+(contains_node p237_1 263)
+(add_element path p237_2)
+(is_path_of p237_2 237)
+(contains_node p237_2 260)
+(is_before p237_2 260 261)
+(contains_node p237_2 261)
+(add_element path p237_3)
+(is_path_of p237_3 260)
+(contains_node p237_3 261)
+(add_element path p237_4)
+(is_path_of p237_4 237)
+(contains_node p237_4 258)
+(is_before p237_4 258 259)
+(contains_node p237_4 259)
+(add_element path p237_5)
+(is_path_of p237_5 258)
+(contains_node p237_5 259)
+(add_element path p237_6)
+(is_path_of p237_6 237)
+(contains_node p237_6 256)
+(is_before p237_6 256 257)
+(contains_node p237_6 257)
+(add_element path p237_7)
+(is_path_of p237_7 256)
+(contains_node p237_7 257)
+(add_element path p237_8)
+(is_path_of p237_8 237)
+(contains_node p237_8 254)
+(is_before p237_8 254 255)
+(contains_node p237_8 255)
+(add_element path p237_9)
+(is_path_of p237_9 254)
+(contains_node p237_9 255)
+(add_element path p237_10)
+(is_path_of p237_10 237)
+(contains_node p237_10 252)
+(is_before p237_10 252 253)
+(contains_node p237_10 253)
+(add_element path p237_11)
+(is_path_of p237_11 252)
+(contains_node p237_11 253)
+(add_element path p237_12)
+(is_path_of p237_12 237)
+(contains_node p237_12 250)
+(is_before p237_12 250 251)
+(contains_node p237_12 251)
+(add_element path p237_13)
+(is_path_of p237_13 250)
+(contains_node p237_13 251)
+(add_element path p237_14)
+(is_path_of p237_14 237)
+(contains_node p237_14 248)
+(is_before p237_14 248 249)
+(contains_node p237_14 249)
+(add_element path p237_15)
+(is_path_of p237_15 248)
+(contains_node p237_15 249)
+(add_element path p237_16)
+(is_path_of p237_16 237)
+(contains_node p237_16 246)
+(is_before p237_16 246 247)
+(contains_node p237_16 247)
+(add_element path p237_17)
+(is_path_of p237_17 246)
+(contains_node p237_17 247)
+(add_element path p237_18)
+(is_path_of p237_18 237)
+(contains_node p237_18 244)
+(is_before p237_18 244 245)
+(contains_node p237_18 245)
+(add_element path p237_19)
+(is_path_of p237_19 244)
+(contains_node p237_19 245)
+(add_element path p237_20)
+(is_path_of p237_20 237)
+(contains_node p237_20 239)
+(is_before p237_20 239 242)
+(contains_node p237_20 242)
+(add_element path p237_21)
+(is_path_of p237_21 239)
+(contains_node p237_21 242)
diff --git a/data/level/control_flow_level.data b/data/level/control_flow_level.lvl
index a7cc9c0..516f9ef 100644
--- a/data/level/control_flow_level.data
+++ b/data/level/control_flow_level.lvl
@@ -7,6 +7,11 @@
 (add_type node)
 (add_type node_depth)
 
+;; Redundancies
+(add_type process)
+(add_type string)
+(add_type waveform)
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/data/level/control_flow_level_kodkod.data b/data/level/control_flow_level_kodkod.lvl
index ed11735..949f69f 100644
--- a/data/level/control_flow_level_kodkod.data
+++ b/data/level/control_flow_level_kodkod.lvl
@@ -6,6 +6,9 @@
 
 (add_type path)
 
+;; Redundancies
+(add_type node)
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/data/level/structural_level.data b/data/level/structural_level.lvl
index 75c4ac9..75c4ac9 100644
--- a/data/level/structural_level.data
+++ b/data/level/structural_level.lvl
diff --git a/data/property/unread_waveforms.pro b/data/property/unread_waveforms.pro
new file mode 100644
index 0000000..b53862b
--- /dev/null
+++ b/data/property/unread_waveforms.pro
@@ -0,0 +1,10 @@
+(tag_existing
+   (
+      (wf waveform UNREAD_WAVEFORM)
+   )
+   (not
+      (exists ps process
+         (is_accessed_by wf ps)
+      )
+   )
+)
diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index 2611f28..073fe58 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -19,12 +19,13 @@ CLASSES = $(SOURCES:.java=.class)
 
 ## Makefile Rules ##############################################################
 
-all: $(CLASSES)
+all: parser/PropertyParser.java $(CLASSES)
 
 clean:
 	rm -f $(CLASSES)
+	$(MAKE) -C parser clean
 
-run: $(CLASSES) $(REQUIRED_JARS)
+run: parser/PropertyParser.java $(CLASSES) $(REQUIRED_JARS)
 	$(JAVA) -cp $(CLASSPATH) Main $(LEVEL_DIR) $(MODEL_FILE)
 
 %.class: %.java $(REQUIRED_JARS)
@@ -34,3 +35,5 @@ run: $(CLASSES) $(REQUIRED_JARS)
 	echo "Attempting to download missing jar '$@'"
 	$(DOWNLOADER) "$(JAR_SOURCE)/$@"
 
+parser/PropertyParser.java: antlr-4.7-complete.jar
+	$(MAKE) -C parser
diff --git a/instr-to-kodkod/parser/Makefile b/instr-to-kodkod/parser/Makefile
new file mode 100644
index 0000000..8f36479
--- /dev/null
+++ b/instr-to-kodkod/parser/Makefile
@@ -0,0 +1,8 @@
+PropertyParser.java: PropertyLexer.g4  PropertyParser.g4
+	java -jar ../antlr-4.7-complete.jar PropertyLexer.g4 PropertyParser.g4
+
+clean:
+	rm -f *.java *.class *.tokens
+
+#test_run:
+#	java -cp ".:../antlr-4.7-complete.jar" org.antlr.v4.gui.TestRig Property prog -gui
diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4
index 63939d7..5e1ed11 100644
--- a/instr-to-kodkod/parser/PropertyParser.g4
+++ b/instr-to-kodkod/parser/PropertyParser.g4
@@ -20,26 +20,80 @@ options
    /* of the class */
 }
 
-prog:
-   tag_existing
-;
+tag_existing
+   returns [Formula result]:
 
-tag_existing:
    (WS)* TAG_EXISTING_KW
       L_PAREN
-         (tag_item)+
+         tag_list
       R_PAREN
    (WS)* sl_formula
    (WS)* R_PAREN
+
+   {
+      final List<String[]> tags;
+
+      $result = ($sl_formula.result);
+
+      tags = ($tag_list.list);
+
+      for (final String[] tag_var: tags)
+      {
+         $result =
+            $result.forSome
+            (
+               Main.get_variable_manager().get_variable
+               (
+                  tag_var[0]
+               ).oneOf
+               (
+                  Main.get_model().get_type_as_relation(tag_var[1])
+               )
+            );
+
+         Main.get_variable_manager().tag_variable(tag_var[0], tag_var[2]);
+      }
+   }
 ;
 
-tag_item:
+tag_list
+   returns [List<String[]> list]
+
+   @init
+   {
+      final List<String[]> result = new ArrayList<String[]>();
+   }
+
+   :
+   (
+      tag_item
+      {
+         result.add(($tag_item.result));
+      }
+   )+
+
+   {
+      $list = result;
+   }
+;
+
+tag_item
+   returns [String[] result]:
+
    (WS)* L_PAREN
    (WS)* var=ID
    (WS)+ type=ID
    (WS)+ tag=ID
    (WS)* R_PAREN
    (WS)*
+
+   {
+      $result = new String[3];
+
+      $result[0] = ($var.text);
+      $result[1] = ($type.text);
+      $result[2] = ($tag.text);
+   }
 ;
 
 id_list
@@ -53,9 +107,9 @@ id_list
    :
    (
       (WS)+
-      var=ID
+      ID
       {
-         result.add(Main.get_variable_manager().get_variable($var.text));
+         result.add(Main.get_variable_manager().get_variable(($ID.text)));
       }
    )*
 
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;
+   }
+}