| summaryrefslogtreecommitdiff |
path: root/instr-to-kodkod
diff options
Diffstat (limited to 'instr-to-kodkod')
| -rw-r--r-- | instr-to-kodkod/Makefile | 5 | ||||
| -rw-r--r-- | instr-to-kodkod/parser/PropertyLexer.g4 | 4 | ||||
| -rw-r--r-- | instr-to-kodkod/parser/PropertyParser.g4 | 7 | ||||
| -rw-r--r-- | instr-to-kodkod/src/Parameters.java | 2 |
4 files changed, 11 insertions, 7 deletions
diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile index bdc7324..5d81814 100644 --- a/instr-to-kodkod/Makefile +++ b/instr-to-kodkod/Makefile @@ -9,8 +9,7 @@ MAP_FILES = $(wildcard ../ast-to-instr/*.map) LEVEL_DIR = $(wildcard ../data/level/*.lvl) PROPERTIES = \ - ../data/property/combinational_processes.pro \ - ../data/property/likely_a_clock.pro + ../data/property/cnes/CNE_01700.pro ## Executables ################################################################# JAVAC = javac @@ -49,7 +48,7 @@ clean: echo "Solving \"$<\"..." $(MAKE) -C ../ast-to-instr $(MAKE) -C ../cfg-to-paths - $(JAVA) -cp $(CLASSPATH) Main $@ $< $(GLOBAL_INPUT_FILES) + $(JAVA) -cp $(CLASSPATH) Main $@ $< $(GLOBAL_INPUT_FILES) -v %.class: %.java $(REQUIRED_JARS) parser/PropertyParser.java $(JAVAC) -cp $(CLASSPATH) $< diff --git a/instr-to-kodkod/parser/PropertyLexer.g4 b/instr-to-kodkod/parser/PropertyLexer.g4 index ec01c88..f5b553e 100644 --- a/instr-to-kodkod/parser/PropertyLexer.g4 +++ b/instr-to-kodkod/parser/PropertyLexer.g4 @@ -4,8 +4,8 @@ fragment SEP: [ \t\r\n]+; L_PAREN : '('; R_PAREN : ')'; -L_BRAKT: ']'; -R_BRAKT: '['; +L_BRAKT: '['; +R_BRAKT: ']'; TAG_EXISTING_KW: '(tag_existing' SEP; diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4 index 3e5634f..e6cd164 100644 --- a/instr-to-kodkod/parser/PropertyParser.g4 +++ b/instr-to-kodkod/parser/PropertyParser.g4 @@ -323,7 +323,7 @@ regex_special_predicate [Variable current_node] (WS)* REGEX_SPECIAL_PREDICATE_KW id_or_string_or_fun[current_node] - STRING + (WS)+ STRING (WS)* R_PAREN { @@ -1303,6 +1303,11 @@ formula [Variable current_node] $result = ($predicate.result); } + | regex_special_predicate[current_node] + { + $result = ($regex_special_predicate.result); + } + | and_operator[current_node] { $result = ($and_operator.result); diff --git a/instr-to-kodkod/src/Parameters.java b/instr-to-kodkod/src/Parameters.java index 7c80474..c6383bd 100644 --- a/instr-to-kodkod/src/Parameters.java +++ b/instr-to-kodkod/src/Parameters.java @@ -140,7 +140,7 @@ public class Parameters prop_file = args[i]; } } - else if (output_file.equals("-v") || output_file.equals("--verbose")) + else if (args[i].equals("-v") || args[i].equals("--verbose")) { should_be_verbose = true; } |