| summaryrefslogtreecommitdiff |
path: root/instr-to-kodkod
diff options
| author | Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org> | 2017-07-31 17:04:51 +0200 |
|---|---|---|
| committer | Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org> | 2017-07-31 17:04:51 +0200 |
| commit | bc8e275546e2e6fe6bcf19ce42c0fab07eecdf4c (patch) | |
| tree | c0fc19f8cb2a3b296f6fef3394ebee122fe5343c /instr-to-kodkod | |
| parent | 27fd5d8afef49ffeca83dd5714738bfaffe04505 (diff) | |
Fixes typo with functions, errors in grammar.
Looking for the groups matching CNE_01700 appears to take a really long
time. The formula is quite complex, yet unlikely to be one of the most
complex ones, so we'll have to see what can be done.
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; } |