Improves error reports for the property.

4 files changed, 152 insertions, 18 deletions

diff --git a/data/level/control_flow_level.lvl b/data/level/control_flow_level.lvl
index 4ae7837..9408409 100644
--- a/data/level/control_flow_level.lvl
+++ b/data/level/control_flow_level.lvl
@@ -20,6 +20,11 @@
 (add_predicate has_option node string)
 (add_predicate has_depth node node_depth)
 (add_predicate node_connect node node)
+
+;;; To be removed soon.
 (add_predicate expr_writes node waveform)
-(add_predicate expr_reads node waveform)
+
+(add_predicate is_read_structure node string)
+(add_predicate is_read_element node string waveform)
+(add_predicate is_read_element node string string)
 (add_predicate is_terminal node)
diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index efcfaa5..c25c95f 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -1,6 +1,7 @@
 ## Target(s) Configuration #####################################################
 #MODEL_FILES = $(wildcard ../data/instructions/*.mod)
 MODEL_FILES = ../ast-to-instr/structural.mod $(wildcard ../ast-to-instr/cfg_*.mod) $(wildcard ../cfg-to-paths/*.mod)
+MAP_FILES = $(wildcard ../ast-to-instr/*.map)
 LEVEL_DIR = $(wildcard ../data/level/*.lvl)
 #PROPERTY_FILE = ../data/property/unread_waveforms.pro
 #PROPERTY_FILE = ../data/property/impossible_processes.pro
@@ -20,7 +21,7 @@ JAR_SOURCE = https://noot-noot.org/onera_2017/jar/
 REQUIRED_JARS = kodkod.jar org.sat4j.core.jar antlr-4.7-complete.jar
 
 ## Makefile Magic ##############################################################
-INPUT_FILES = $(MODEL_FILES) $(LEVEL_DIR) $(PROPERTY_FILE)
+INPUT_FILES = $(MODEL_FILES) $(LEVEL_DIR) $(PROPERTY_FILE) $(MAP_FILES)
 SOURCES = $(wildcard src/*.java parser/*.java)
 GRAMMARS = $(wildcard parser/*.g4)
 CLASSES = $(SOURCES:.java=.class)
@@ -28,6 +29,7 @@ CLASSES = $(SOURCES:.java=.class)
 ## Makefile Rules ##############################################################
 
 all: parser/PropertyParser.java $(CLASSES)
+	$(MAKE) -C parser
 	$(MAKE) -C ../ast-to-instr
 	$(MAKE) -C ../cfg-to-paths
 
diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4
index b44fbe2..4542130 100644
--- a/instr-to-kodkod/parser/PropertyParser.g4
+++ b/instr-to-kodkod/parser/PropertyParser.g4
@@ -39,6 +39,26 @@ tag_existing
 
       for (final String[] tag_var: tags)
       {
+         final Relation type_as_relation;
+
+         type_as_relation = Main.get_model().get_type_as_relation(tag_var[1]);
+
+         if (type_as_relation == (Relation) null)
+         {
+            System.err.println
+            (
+               "[F] The property uses an unknown type: \""
+               + tag_var[1]
+               + "\" in its tag_existing (l."
+               + ($TAG_EXISTING_KW.getLine())
+               + " c."
+               + ($TAG_EXISTING_KW.getCharPositionInLine())
+               + ")."
+            );
+
+            System.exit(-1);
+         }
+
          $result =
             $result.forSome
             (
@@ -47,7 +67,7 @@ tag_existing
                   tag_var[0]
                ).oneOf
                (
-                  Main.get_model().get_type_as_relation(tag_var[1])
+                  type_as_relation
                )
             );
 
@@ -143,7 +163,29 @@ sl_predicate
    {
       final Expression predicate;
       final List<Variable> ids;
+      final Relation predicate_as_relation;
 
+      predicate_as_relation =
+         Main.get_model().get_predicate_as_relation
+         (
+            ($ID.text)
+         );
+
+      if (predicate_as_relation == (Relation) null)
+      {
+         System.err.println
+         (
+            "[F] The property uses an unknown predicate: \""
+            + ($ID.text)
+            + "\" at structural level. (l."
+            + ($ID.getLine())
+            + " c."
+            + ($ID.getCharPositionInLine())
+            + ")."
+         );
+
+         System.exit(-1);
+      }
 
       if (($id_list.has_joker))
       {
@@ -165,17 +207,14 @@ sl_predicate
          }
 
          predicate =
-            Main.get_model().get_predicate_as_relation
-            (
-               ($ID.text)
-            ).project
+            predicate_as_relation.project
             (
                (IntExpression[]) columns.toArray()
             );
       }
       else
       {
-         predicate = Main.get_model().get_predicate_as_relation(($ID.text));
+         predicate = predicate_as_relation;
          ids = ($id_list.list);
       }
 
@@ -280,6 +319,30 @@ sl_exists_operator
    (WS*) R_PAREN
 
    {
+      final Relation type_as_relation;
+
+      type_as_relation =
+         Main.get_model().get_type_as_relation
+         (
+            ($type.text)
+         );
+
+      if (type_as_relation == (Relation) null)
+      {
+         System.err.println
+         (
+            "[F] The property uses an unknown type: \""
+            + ($type.text)
+            + "\" in an \"exists\" at structural level (l."
+            + ($type.getLine())
+            + " c."
+            + ($type.getCharPositionInLine())
+            + ")."
+         );
+
+         System.exit(-1);
+      }
+
       $result =
          ($f.result).forSome
          (
@@ -288,7 +351,7 @@ sl_exists_operator
                ($var.text)
             ).oneOf
             (
-               Main.get_model().get_type_as_relation(($type.text))
+               type_as_relation
             )
          );
    }
@@ -304,6 +367,30 @@ sl_forall_operator
    (WS*) R_PAREN
 
    {
+      final Relation type_as_relation;
+
+      type_as_relation =
+         Main.get_model().get_type_as_relation
+         (
+            ($type.text)
+         );
+
+      if (type_as_relation == (Relation) null)
+      {
+         System.err.println
+         (
+            "[F] The property uses an unknown type: \""
+            + ($type.text)
+            + "\" in a \"forall\" at structural level (l."
+            + ($type.getLine())
+            + " c."
+            + ($type.getCharPositionInLine())
+            + ")."
+         );
+
+         System.exit(-1);
+      }
+
       $result =
          ($f.result).forAll
          (
@@ -312,7 +399,7 @@ sl_forall_operator
                ($var.text)
             ).oneOf
             (
-               Main.get_model().get_type_as_relation(($type.text))
+               type_as_relation
             )
          );
    }
@@ -344,7 +431,10 @@ sl_ctl_verifies_operator
             (
                Main.get_variable_manager().get_variable(($ps.text)).join
                (
-                  Main.get_model().get_predicate_as_relation("is_start_node").transpose()
+                  Main.get_model().get_predicate_as_relation
+                  (
+                     "is_start_node"
+                  ).transpose()
                )
             )
          );
@@ -410,7 +500,29 @@ bl_predicate [Variable current_node]
    {
       final Expression predicate;
       final List<Variable> ids;
+      final Relation predicate_as_relation;
+
+      predicate_as_relation =
+         Main.get_model().get_predicate_as_relation
+         (
+            ($ID.text)
+         );
 
+      if (predicate_as_relation == (Relation) null)
+      {
+         System.err.println
+         (
+            "[F] The property uses an unknown predicate: \""
+            + ($ID.text)
+            + "\" at behavioral level (l."
+            + ($ID.getLine())
+            + " c."
+            + ($ID.getCharPositionInLine())
+            + ")."
+         );
+
+         System.exit(-1);
+      }
 
       if (($id_list.has_joker))
       {
@@ -432,17 +544,14 @@ bl_predicate [Variable current_node]
          }
 
          predicate =
-            Main.get_model().get_predicate_as_relation
-            (
-               ($ID.text)
-            ).project
+            predicate_as_relation.project
             (
                (IntExpression[]) columns.toArray()
             );
       }
       else
       {
-         predicate = Main.get_model().get_predicate_as_relation(($ID.text));
+         predicate = predicate_as_relation;
          ids = ($id_list.list);
       }
 
@@ -811,7 +920,10 @@ bl_au_operator [Variable current_node]
             (
                current_node.join
                (
-                  Main.get_model().get_predicate_as_relation("is_path_of").transpose()
+                  Main.get_model().get_predicate_as_relation
+                  (
+                     "is_path_of"
+                  ).transpose()
                )
             )
          );
@@ -867,7 +979,10 @@ bl_eu_operator [Variable current_node]
             (
                current_node.join
                (
-                  Main.get_model().get_predicate_as_relation("is_path_of").transpose()
+                  Main.get_model().get_predicate_as_relation
+                  (
+                     "is_path_of"
+                  ).transpose()
                )
             )
          );
diff --git a/instr-to-kodkod/src/Parameters.java b/instr-to-kodkod/src/Parameters.java
index 81c9dba..c3fcd51 100644
--- a/instr-to-kodkod/src/Parameters.java
+++ b/instr-to-kodkod/src/Parameters.java
@@ -5,6 +5,7 @@ public class Parameters
 {
    private final List<String> level_files;
    private final List<String> model_files;
+   private final List<String> map_files;
    private final String property_file;
    private final String var_prefix;
 
@@ -25,6 +26,7 @@ public class Parameters
          + "\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- Map files have a \".map\" extension.\n"
          + "\t- The files may be given in any order."
       );
    }
@@ -36,6 +38,7 @@ public class Parameters
 
       level_files = new ArrayList<String>();
       model_files = new ArrayList<String>();
+      map_files = new ArrayList<String>();
 
       if (args.length < 2)
       {
@@ -65,6 +68,10 @@ public class Parameters
          {
             model_files.add(args[i]);
          }
+         else if (args[i].endsWith(".map"))
+         {
+            map_files.add(args[i]);
+         }
          else if (args[i].endsWith(".pro"))
          {
             if (has_pro_file)
@@ -121,6 +128,11 @@ public class Parameters
       return model_files;
    }
 
+   public List<String> get_map_files ()
+   {
+      return model_files;
+   }
+
    public String get_property_file ()
    {
       return property_file;