| summaryrefslogtreecommitdiff |
diff options
| -rw-r--r-- | data/instructions/example_1.mod (renamed from data/instructions/example_1.sl) | 0 | ||||
| -rw-r--r-- | instr-to-kodkod/Makefile | 3 | ||||
| -rw-r--r-- | instr-to-kodkod/parser/PropertyParser.g4 | 22 | ||||
| -rw-r--r-- | instr-to-kodkod/src/Main.java | 11 | ||||
| -rw-r--r-- | instr-to-kodkod/src/VHDLPredicate.java | 2 | ||||
| -rw-r--r-- | instr-to-kodkod/src/VHDLType.java | 7 |
6 files changed, 41 insertions, 4 deletions
diff --git a/data/instructions/example_1.sl b/data/instructions/example_1.mod index 1adbd4b..1adbd4b 100644 --- a/data/instructions/example_1.sl +++ b/data/instructions/example_1.mod diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile index 0f51838..dd80198 100644 --- a/instr-to-kodkod/Makefile +++ b/instr-to-kodkod/Makefile @@ -19,6 +19,7 @@ REQUIRED_JARS = kodkod.jar org.sat4j.core.jar antlr-4.7-complete.jar ## Makefile Magic ############################################################## INPUT_FILES = $(MODEL_FILES) $(LEVEL_DIR) $(PROPERTY_FILE) SOURCES = $(wildcard src/*.java parser/*.java) +GRAMMARS = $(wildcard parser/*.g4) CLASSES = $(SOURCES:.java=.class) ## Makefile Rules ############################################################## @@ -39,5 +40,5 @@ run: parser/PropertyParser.java $(CLASSES) $(REQUIRED_JARS) echo "Attempting to download missing jar '$@'" $(DOWNLOADER) "$(JAR_SOURCE)/$@" -parser/PropertyParser.java: antlr-4.7-complete.jar +parser/PropertyParser.java: antlr-4.7-complete.jar $(GRAMMAR) $(MAKE) -C parser diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4 index 5e1ed11..0bcb6a9 100644 --- a/instr-to-kodkod/parser/PropertyParser.g4 +++ b/instr-to-kodkod/parser/PropertyParser.g4 @@ -132,7 +132,14 @@ sl_predicate { /* TODO */ - $result = null; + $result = + Expression.product + ( + ($id_list.list) + ).in + ( + Main.get_model().get_predicate_as_relation(($ID.text)) + ); } ; @@ -357,7 +364,18 @@ bl_predicate [Variable current_node] { /* TODO */ - $result = null; + $result = + current_node.product + ( + Expression.product + ( + ($id_list.list) + ) + ).in + ( + Main.get_model().get_predicate_as_relation(($ID.text)) + ); + } ; diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java index 0b1d2e4..0719679 100644 --- a/instr-to-kodkod/src/Main.java +++ b/instr-to-kodkod/src/Main.java @@ -31,6 +31,8 @@ public class Main { try { + System.out.println("Loading level file \"" + lvl + "\"..."); + VHDLLevel.add_to_model(MODEL, lvl); } catch (final Exception e) @@ -59,6 +61,13 @@ public class Main try { + System.out.println + ( + "Loading property file \"" + + PARAMETERS.get_property_file() + + "\"..." + ); + return pro.generate_formula(); } catch (final IOException e) @@ -81,6 +90,8 @@ public class Main { try { + System.out.println("Loading model file \"" + mod + "\"..."); + MODEL.parse_file(mod); } catch (final Exception e) diff --git a/instr-to-kodkod/src/VHDLPredicate.java b/instr-to-kodkod/src/VHDLPredicate.java index 210dd7e..3605e76 100644 --- a/instr-to-kodkod/src/VHDLPredicate.java +++ b/instr-to-kodkod/src/VHDLPredicate.java @@ -58,6 +58,8 @@ public class VHDLPredicate } is_used = true; + + System.out.println("Enabling predicate: " + name); } return as_relation; diff --git a/instr-to-kodkod/src/VHDLType.java b/instr-to-kodkod/src/VHDLType.java index 73cd9cf..58b0d1e 100644 --- a/instr-to-kodkod/src/VHDLType.java +++ b/instr-to-kodkod/src/VHDLType.java @@ -35,7 +35,12 @@ public class VHDLType public void flag_as_used () { - is_used = true; + if (!is_used) + { + System.out.println("Enabling type: " + name); + + is_used = true; + } } public boolean is_used () |