Solves the missing solutions bug. Starts PropDeps.

6 files changed, 66 insertions, 30 deletions

diff --git a/Makefile b/Makefile
index 983e476..e60aa8d 100644
--- a/Makefile
+++ b/Makefile
@@ -1,25 +1,38 @@
 ## Makefile Parameters #########################################################
 LEVEL_FILES ?= $(wildcard ${CURDIR}/data/level/*.lvl)
-PROPERTY_FILES ?= $(wildcard ${CURDIR}/data/property/*.pro)
+ALL_PROPERTY_FILES ?= $(wildcard ${CURDIR}/data/property/*.pro)
+#PROPERTY_FILES ?= $(wildcard ${CURDIR}/data/property/*.pro)
+PROPERTY_FILES ?= $(wildcard ${CURDIR}/data/property/test.pro)
 AST_FILE ?= ${CURDIR}/data/ast/best_chronometer_ever.xml
 TEMPLATE_DIR ?= ${CURDIR}/data/template/
 #AST_FILE = ${CURDIR}/data/ast/pong.xml
 NICE_MESSAGE ?=
 
 TMP_DIR ?= /tmp/tabellion
+DEPENDENCIES_DIR ?= $(TMP_DIR)/deps
 MODEL_DIR ?= $(TMP_DIR)/mod
 MODEL_INSTANCES_DIR ?= $(MODEL_DIR)/instance
+MODEL_INFERRED_DIR ?= $(MODEL_DIR)/inferred
 SOL_DIR ?= $(TMP_DIR)/sol
 
 ## Sub-programs ################################################################
-AST_TO_INSTR = ast-to-instr
-INST_CALC = instance-calculator
-SOLVER = instr-to-kodkod
-PRETTY_PRINTER = sol-pretty-printer
+AST_TO_INSTR ?= ast-to-instr
+INST_CALC ?= instance-calculator
+SOLVER ?= instr-to-kodkod
+PRETTY_PRINTER ?= sol-pretty-printer
 
 export
 
-all: $(TMP_DIR) $(MODEL_DIR) $(SOL_DIR)
+################################################################################
+ALL_DIRS = \
+	$(TMP_DIR) \
+	$(DEPENDENCIES_DIR) \
+	$(MODEL_DIR) \
+	$(MODEL_INSTANCES_DIR) \
+	$(MODEL_INFERED_DIR) \
+	$(SOL_DIR)
+
+all: $(ALL_DIRS)
 	$(MAKE) compile
 	$(MAKE) model
 	$(MAKE) solutions
@@ -60,11 +73,5 @@ clean_solutions:
 	$(MAKE) -C $(SOLVER) clean_solutions
 	$(MAKE) -C $(PRETTY_PRINTER) clean_solutions
 
-$(TMP_DIR):
-	mkdir -p $@
-
-$(MODEL_DIR):
-	mkdir -p $@
-
-$(SOL_DIR):
+$(ALL_DIRS):
 	mkdir -p $@
diff --git a/data/property/CNE_01100.pro b/data/property/CNE_01100.pro
index ad94747..6ed2cff 100644
--- a/data/property/CNE_01100.pro
+++ b/data/property/CNE_01100.pro
@@ -2,19 +2,28 @@
    (
       (pt port CNE_01100_BAD_NAME)
    )
-   (not
-      (or
-         (and
-            (string_matches [identifier pt] "^i_.*")
-            (has_mode pt "in")
-         )
-         (and
-            (string_matches [identifier pt] "^o_.*")
-            (has_mode pt "out")
-         )
-         (and
-            (string_matches [identifier pt] "^b_.*")
-            (has_mode pt "inout")
+   (exists pt2 port
+      (and
+;; Goes into infinity:
+;;       (has_mode pt2 _)
+;;       (has_mode pt2 "in")
+;; Fixes all:
+         (eq pt2 pt)
+         (not
+            (or
+               (and
+                  (string_matches [identifier pt] "^i_.*")
+                  (has_mode pt "in")
+               )
+               (and
+                  (string_matches [identifier pt] "^o_.*")
+                  (has_mode pt "out")
+               )
+               (and
+                  (string_matches [identifier pt] "^b_.*")
+                  (has_mode pt "inout")
+               )
+            )
          )
       )
    )
diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index b708c16..322205f 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -91,6 +91,8 @@ ANTLR_JAR = ${CURDIR}/antlr-4.7-complete.jar
 SOURCES = $(wildcard src/*.java)
 CLASSES = $(SOURCES:.java=.class)
 SOLUTION_FILES = $(addprefix $(SOL_DIR)/,$(notdir $(PROPERTY_FILES:.pro=.sol)))
+DEPENDENCY_FILES = \
+	$(addprefix $(DEPENDENCIES_DIR)/,$(notdir $(PROPERTY_FILES:.pro=.deps)))
 MODEL_FILES = \
 	$(MODEL_DIR)/structural.mod \
 	$(MODEL_DIR)/depths.mod \
@@ -115,12 +117,14 @@ clean:
 	$(MAKE) -C cfg-to-paths clean
 	rm -f $(CLASSES)
 	rm -f $(SOL_DIR)/*.sol
+	rm -f $(DEPENDENCY_FILES)
 
 clean_model:
 	$(MAKE) -C cfg-to-paths clean_model
 
 clean_solutions:
 	rm -f $(SOL_DIR)/*.sol
+	rm -f $(DEPENDENCY_FILES)
 
 ########
 cfg-generator:
@@ -129,7 +133,8 @@ cfg-generator:
 $(PARSER_CLASSES): antlr-4.7-complete.jar kodkod.jar $(PARSER_SOURCES)
 	$(MAKE) -C parser
 
-$(SOL_DIR)/%.sol: $(PROPERTY_FILES) $(MODEL_FILES) $(LEVEL_FILES)
+$(SOL_DIR)/%.sol: \
+	$(DEPENDENCIES_DIR)/%.deps $(PROPERTY_FILES) $(MODEL_FILES) $(LEVEL_FILES)
 	touch $@
 	$(JAVA) -cp $(CLASSPATH) Main $@ -v \
 		$(filter %$(basename $(notdir $@)).pro,$(PROPERTY_FILES)) \
@@ -137,6 +142,10 @@ $(SOL_DIR)/%.sol: $(PROPERTY_FILES) $(MODEL_FILES) $(LEVEL_FILES)
 		$(MODEL_FILES) \
 		$(wildcard $(PATH_MODEL_DIR)/*.mod)
 
+$(DEPENDENCY_FILES): $(PROPERTY_FILES)
+	sed -n 's/^#require \"\(.*\)\"$$/\1/p' \
+		$(filter %$(basename $(notdir $@)).pro,$(PROPERTY_FILES)) > $@
+
 src/%.class: src/%.java $(PARSER_CLASSES) $(REQUIRED_JARS)
 	$(JAVAC) -cp $(CLASSPATH) $<
 
diff --git a/instr-to-kodkod/parser/PropertyLexer.g4 b/instr-to-kodkod/parser/PropertyLexer.g4
index 3b6011d..e100efb 100644
--- a/instr-to-kodkod/parser/PropertyLexer.g4
+++ b/instr-to-kodkod/parser/PropertyLexer.g4
@@ -37,7 +37,7 @@ DEPTH_NO_CHANGE_OPERATOR_KW: ('(NDCB' | '(does_not_change_depth_before') SEP;
 
 WS: SEP;
 
-ID: [a-zA-Z0-9_]+;
+ID: [a-zA-Z0-9_~]+;
 STRING: '"' ~('\r' | '\n' | '"')* '"';
 
-COMMENT: ';;' .*? '\n' -> channel(HIDDEN);
+COMMENT: (';;'|'#require') .*? '\n' -> channel(HIDDEN);
diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java
index 11a357a..be5cb21 100644
--- a/instr-to-kodkod/src/Main.java
+++ b/instr-to-kodkod/src/Main.java
@@ -355,10 +355,21 @@ public class Main
 
       solver = new Solver();
       solver.options().setSkolemDepth(-1);
+      solver.options().setSymmetryBreaking(0);
       solver.options().setSolver(SATFactory.DefaultSAT4J);
 
       if (PARAMETERS.be_verbose())
       {
+         System.out.println(bounds);
+         System.out.println
+         (
+            "Final formula:"
+            +
+            property.and
+            (
+               VARIABLE_MANAGER.generate_tagged_variable_constraints()
+            ).toString()
+         );
          solver.options().setReporter(new ConsoleReporter());
       }
 
diff --git a/instr-to-kodkod/src/VariableManager.java b/instr-to-kodkod/src/VariableManager.java
index 249b183..fee499e 100644
--- a/instr-to-kodkod/src/VariableManager.java
+++ b/instr-to-kodkod/src/VariableManager.java
@@ -144,7 +144,7 @@ public class VariableManager
 
       for (final TaggedVariable tg: tagged_variables.values())
       {
-         result = result.and(tg.as_relation.one());
+           result = result.and(tg.as_relation.one());
       }
 
       return result;