aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authornsensfel <SpamShield0@noot-noot.org>2017-10-31 16:22:43 +0100
committernsensfel <SpamShield0@noot-noot.org>2017-10-31 16:22:43 +0100
commit4c16982225c0951e02b23bcdb36d1a5a8c2b44de (patch)
treea6e9a341224502e6a8817f8f195f51fe391b1268
parent884b8a47fe7fc18e1c4427193cb86be53c24ff41 (diff)
downloadtabellion-master.zip
tabellion-master.tar.bz2
Disables the "inferred" feature by default.HEADmaster
-rw-r--r--Makefile11
-rw-r--r--no-prop-to-pred/Makefile42
2 files changed, 50 insertions, 3 deletions
diff --git a/Makefile b/Makefile
index a45b11d..44dd6f3 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,11 @@
## Makefile Parameters #########################################################
LEVELS_DIR ?= ${CURDIR}/data/level/
PROPERTIES_DIR ?= ${CURDIR}/data/property/
-PROPERTIES ?= $(basename $(notdir $(wildcard $(PROPERTIES_DIR)/*.pro)))
+#PROPERTIES ?= $(basename $(notdir $(wildcard $(PROPERTIES_DIR)/*.pro)))
+# Below is a list of properties that removes those requiring "inferred"
+# features. Comment the line above and uncomment the line below to use those.
+# Also, see the definition of PROP_TO_PRED further down.
+PROPERTIES ?= $(filter-out flip_flop CNE_01700 test, $(basename $(notdir $(wildcard $(PROPERTIES_DIR)/*.pro))))
AST_FILE ?= ${CURDIR}/data/ast/best_chronometer_ever.xml
TEMPLATE_DIR ?= ${CURDIR}/data/template/
TO_PRED_TEMPLATE_DIR ?= ${CURDIR}/data/to_pred_template/
@@ -21,8 +25,9 @@ AST_TO_INSTR ?= ast-to-instr
INST_CALC ?= instance-calculator
SOLVER ?= instr-to-kodkod
PRETTY_PRINTER ?= sol-pretty-printer
-PROP_TO_PRED ?= prop-to-pred
-
+#PROP_TO_PRED ?= prop-to-pred
+# Line above: use "inferred" feature, line below: do not use "inferred" feature.
+PROP_TO_PRED ?= no-prop-to-pred
export
################################################################################
diff --git a/no-prop-to-pred/Makefile b/no-prop-to-pred/Makefile
new file mode 100644
index 0000000..c5d2df4
--- /dev/null
+++ b/no-prop-to-pred/Makefile
@@ -0,0 +1,42 @@
+## Parameters ##################################################################
+TO_PRED_TEMPLATE_DIR ?=
+INFERRED_LEVEL_FILE ?=
+PROPERTIES_DIR ?=
+#### Where to find the properties to verify
+ALL_PROPERTY_FILES ?= $(wildcard $(PROPERTIES_DIR)/*.pro)
+
+################################################################################
+PRED_TO_INFER = \
+ $(addsuffix .pp,$(addprefix $(TO_PRED_TEMPLATE_DIR)/,$(notdir $(basename $(ALL_PROPERTY_FILES)))))
+ADDITIONAL_MAKEFILES = \
+ $(addsuffix .deps,$(addprefix $(DEPENDENCIES_DIR)/,$(basename $(notdir $(ALL_PROPERTY_FILES)))))
+
+export
+## Makefile Rules ##############################################################
+compile: $(PRED_TO_INFER) $(ADDITIONAL_MAKEFILES)
+
+model:
+
+solutions:
+
+clean:
+ rm -f $(TO_PRED_TEMPLATE_DIR)/*
+ rm -f $(INFERRED_LEVEL_FILE)
+
+clean_model:
+
+clean_solutions:
+ rm -f $(TO_PRED_TEMPLATE_DIR)/*
+ rm -f $(INFERRED_LEVEL_FILE)
+
+########
+$(TO_PRED_TEMPLATE_DIR)/%.pp: $(PROPERTIES_DIR)/%.pro
+ touch $@
+ $(MAKE) $(DEPENDENCIES_DIR)/$(patsubst %.pp,%,$(notdir $(basename $@))).deps
+
+$(DEPENDENCIES_DIR)/%.deps: $(PROPERTIES_DIR)/%.pro
+ printf "$(SOL_DIR)/$(notdir $(basename $@)).sol.ready: " > $@
+ for dep in `sed -n 's/^#require \"\(.*\)\"$$/\1/p' $<` ; do \
+ printf "$(SOL_DIR)/$$dep.sol " >> $@ ; \
+ done
+ printf "\n\t touch $(SOL_DIR)/$(notdir $(basename $@)).sol.ready\n\n" >> $@