| summaryrefslogtreecommitdiff |
diff options
| -rw-r--r-- | data/level/control_flow_level.lvl | 7 | ||||
| -rw-r--r-- | instr-to-kodkod/Makefile | 4 | ||||
| -rw-r--r-- | instr-to-kodkod/parser/PropertyParser.g4 | 147 | ||||
| -rw-r--r-- | instr-to-kodkod/src/Parameters.java | 12 |
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; |