aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-09-20 17:19:42 +0200
committerNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-09-20 17:19:42 +0200
commitbc3e8933e1005e93e4a97b9a207cb40db454a2a8 (patch)
treec6b6431a7ab6e1188faab80efb2d89712d4b48a6
parent71e7acf1ac104258a295a2662d6dc71f49ac77aa (diff)
downloadtabellion-bc3e8933e1005e93e4a97b9a207cb40db454a2a8.zip
tabellion-bc3e8933e1005e93e4a97b9a207cb40db454a2a8.tar.bz2
Solves the missing solutions bug. Starts PropDeps.
-rw-r--r--Makefile33
-rw-r--r--data/property/CNE_01100.pro35
-rw-r--r--instr-to-kodkod/Makefile11
-rw-r--r--instr-to-kodkod/parser/PropertyLexer.g44
-rw-r--r--instr-to-kodkod/src/Main.java11
-rw-r--r--instr-to-kodkod/src/VariableManager.java2
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;