aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-09-25 12:48:44 +0200
committerNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-09-25 12:48:44 +0200
commit4669bdf7046c03200a28de4188075bee69571eb8 (patch)
tree97ff430a177d257be7e11d1392f3894d27de2f63
parent0fc661ebabdf55b8e0d26c4f85f0547c106b6549 (diff)
downloadtabellion-4669bdf7046c03200a28de4188075bee69571eb8.zip
tabellion-4669bdf7046c03200a28de4188075bee69571eb8.tar.bz2
Updates Tests, fixes 2 properties & inferred/*.mod
-rw-r--r--Makefile6
-rw-r--r--data/property/CNE_01100.pro35
-rw-r--r--data/property/CNE_01700.pro161
-rw-r--r--data/property/simple_flip_flop.pro5
-rw-r--r--data/test/Makefile7
-rw-r--r--instr-to-kodkod/Makefile4
-rw-r--r--sol-pretty-printer/Makefile2
7 files changed, 37 insertions, 183 deletions
diff --git a/Makefile b/Makefile
index 1f72ef0..e8242d7 100644
--- a/Makefile
+++ b/Makefile
@@ -42,21 +42,21 @@ all: $(ALL_DIRS)
$(MAKE) model
$(MAKE) solutions
-compile:
+compile: $(ALL_DIRS)
$(MAKE) -C $(AST_TO_INSTR) compile
$(MAKE) -C $(INST_CALC) compile
$(MAKE) -C $(SOLVER) compile
$(MAKE) -C $(PRETTY_PRINTER) compile
$(MAKE) -C $(PROP_TO_PRED) compile
-model:
+model: $(ALL_DIRS)
$(MAKE) -C $(AST_TO_INSTR) model
$(MAKE) -C $(INST_CALC) model
$(MAKE) -C $(SOLVER) model
$(MAKE) -C $(PRETTY_PRINTER) model
$(MAKE) -C $(PROP_TO_PRED) model
-solutions: $(TMP_DIR) $(MODEL_DIR) $(SOL_DIR)
+solutions: $(ALL_DIRS)
$(MAKE) -C $(AST_TO_INSTR) solutions
$(MAKE) -C $(INST_CALC) solutions
$(MAKE) -C $(SOLVER) solutions
diff --git a/data/property/CNE_01100.pro b/data/property/CNE_01100.pro
index 6ed2cff..ad94747 100644
--- a/data/property/CNE_01100.pro
+++ b/data/property/CNE_01100.pro
@@ -2,28 +2,19 @@
(
(pt port CNE_01100_BAD_NAME)
)
- (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")
- )
- )
+ (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/data/property/CNE_01700.pro b/data/property/CNE_01700.pro
index 7452a3c..2327afc 100644
--- a/data/property/CNE_01700.pro
+++ b/data/property/CNE_01700.pro
@@ -1,9 +1,11 @@
+#require "flip_flop"
+
(tag_existing
(
(x_re waveform CNE_01700_HAS_BAD_NAME)
)
(and
- (not (string_matches [identifier [is_waveform_of x_re]] ".*_re"))
+ (not (string_matches [identifier [is_waveform_of x_re]] ".*_re$"))
;; 'x' is the signal 'x_re' detects the rising edge of.
(exists x waveform
(and
@@ -58,159 +60,16 @@
(is_accessed_by x_r1 ps1)
(is_accessed_by x ps1)
(is_explicit_process ps1)
-;; 'clk1' is the clock controlling that flipflop
-(exists clk1 waveform
- (and
- (is_in_sensitivity_list clk1 ps1)
- (not (eq clk1 x_re))
- (not (eq clk1 x))
- (not (eq clk1 x_r1))
- (or
-;; 'ps1' could be a simple flipflop
-(CTL_verifies ps1
- (AF
- (and
- (kind "if")
- (or
- (and
- (is_read_structure "(??)")
- (or
- (is_read_element "0" "falling_edge")
- (is_read_element "0" "rising_edge")
- )
- (is_read_element "1" clk1)
- )
- (and
- (is_read_structure "(?(??)(???))")
- (is_read_element "0" "and")
- (is_read_element "1" "event")
- (is_read_element "2" clk1)
- (is_read_element "3" "=")
- (or
- (is_read_element "4" clk1)
- (is_read_element "5" clk1)
- )
- )
- (and
- (is_read_structure "(?(???)(??))")
- (is_read_element "0" "and")
- (is_read_element "1" "=")
- (or
- (is_read_element "2" clk1)
- (is_read_element "3" clk1)
- )
- (is_read_element "4" "event")
- (is_read_element "5" clk1)
- )
- )
- (EX
+ (_flip_flop x_r1 _ ps1)
+ (CTL_verifies ps1
+ (EF
(and
- (has_option "cond_was_true")
- (does_not_reach_parent_before
- (and
- (expr_writes x_r1)
- (is_read_structure "?")
- (is_read_element "0" x)
- (AX
- (not
- (EF
- (expr_writes x_r1)
- )
- )
- )
- )
- )
+ (expr_writes x_r1)
+ (is_read_structure "?")
+ (is_read_element "0" x)
)
)
)
)
)
-;; 'ps1' could be a flipflop with reset
-;; 'rst1' is that reset signal
-(exists rst1 waveform
- (and
- (is_in_sensitivity_list rst1 ps1)
- (not (eq rst1 x_re))
- (not (eq rst1 x))
- (not (eq rst1 x_r1))
- (not (eq rst1 clk1))
-(CTL_verifies ps1
- (AF
- (and
- (kind "if")
- (is_read_structure "(???)")
- (is_read_element "0" "=")
- (is_read_element _ rst1)
- (EX
- (and
- (not (has_option "cond_was_true"))
- (kind "if")
- (or
- (and
- (is_read_structure "(??)")
- (or
- (is_read_element "0" "falling_edge")
- (is_read_element "0" "rising_edge")
- )
- (is_read_element "1" clk1)
- )
- (and
- (is_read_structure "(?(??)(???))")
- (is_read_element "0" "and")
- (is_read_element "1" "event")
- (is_read_element "2" clk1)
- (is_read_element "3" "=")
- (or
- (is_read_element "4" clk1)
- (is_read_element "5" clk1)
- )
- )
- (and
- (is_read_structure "(?(???)(??))")
- (is_read_element "0" "and")
- (is_read_element "1" "=")
- (or
- (is_read_element "2" clk1)
- (is_read_element "3" clk1)
- )
- (is_read_element "4" "event")
- (is_read_element "5" clk1)
- )
- )
- (EX
- (and
- (has_option "cond_was_true")
- (does_not_reach_parent_before
- (and
- (expr_writes x_r1)
- (is_read_structure "?")
- (is_read_element "0" x)
- (AX
- (not
- (EF
- (expr_writes x_r1)
- )
- )
- )
- )
- )
- )
- )
- )
- )
- )
- )
-)
-)
-)
-)
-)
-)
-)
-)
-)
-)
-)
-)
-)
-)
+))))))
diff --git a/data/property/simple_flip_flop.pro b/data/property/simple_flip_flop.pro
index b054c7f..09ef98b 100644
--- a/data/property/simple_flip_flop.pro
+++ b/data/property/simple_flip_flop.pro
@@ -9,7 +9,8 @@
(is_explicit_process ps)
(is_in_sensitivity_list clk ps)
(CTL_verifies ps
- (AF
+ (AU
+ (not (expr_writes reg))
(and
(kind "if")
(or
@@ -46,7 +47,7 @@
)
(EX
(and
- (has_option "COND_WAS_TRUE")
+ (has_option "cond_was_true")
(does_not_reach_parent_before
(and
(expr_writes reg)
diff --git a/data/test/Makefile b/data/test/Makefile
index 37769db..07f6a88 100644
--- a/data/test/Makefile
+++ b/data/test/Makefile
@@ -2,7 +2,7 @@ TABELLION_MAIN ?= ${CURDIR}/../../
AST_CREATOR = ghdl --file-to-xml
#TEST_DIRS ?= $(addprefix ${CURDIR}/,$(wildcard */))
TEST_DIRS ?= $(patsubst %/,%,$(wildcard */))
-PROPERTY_DIR ?= ${CURDIR}/../property
+PROPERTIES_DIR ?= ${CURDIR}/../property
# TODO: Start using those variables...
SOLUTION_DIR ?= /tmp/tabellion/sol/
ORACLE_CREATOR_SCRIPT = ${CURDIR}/oracle_creator.py
@@ -44,6 +44,7 @@ clean:
rm -f $(VLD_FILES)
rm -f $(IVLD_FILES)
rm -f $(SOL_FILES)
+ rm -f $(addprefix .ready,$(SOL_FILES))
rm -rf /tmp/tabellion_{,in}valid
$(AST_FILES): %.xml : %.vhd
@@ -62,7 +63,7 @@ $(VLD_FILES): %/valid.result: %/valid.ocl %/valid.xml
$(MAKE) -C $(TABELLION_MAIN) \
TMP_DIR=/tmp/tabellion_valid \
AST_FILE=${PWD}/$(dir $@)/valid.xml \
- PROPERTY_FILES=$(PROPERTY_DIR)/$(patsubst %/,%,$(dir $@)).pro \
+ PROPERTIES=$(patsubst %/,%,$(dir $@)) \
TEMPLATE_DIR=${PWD}/$(dir $@)/ \
NICE_MESSAGE=/tmp/tabellion_valid/result
cat /tmp/tabellion_valid/result | sed '/^\s*$$/d' | sort > /tmp/tabellion_valid/result_clean
@@ -78,7 +79,7 @@ $(IVLD_FILES): %/invalid.result: %/invalid.ocl %/invalid.xml
$(MAKE) -C $(TABELLION_MAIN) \
TMP_DIR=/tmp/tabellion_invalid \
AST_FILE=${PWD}/$(dir $@)/invalid.xml \
- PROPERTY_FILES=$(PROPERTY_DIR)/$(patsubst %/,%,$(dir $@)).pro \
+ PROPERTIES=$(patsubst %/,%,$(dir $@)) \
TEMPLATE_DIR=${PWD}/$(dir $@)/ \
NICE_MESSAGE=/tmp/tabellion_invalid/result
cat /tmp/tabellion_invalid/result | sed '/^\s*$$/d' | sort > $@
diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index 0523a46..cac9ffe 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -108,6 +108,7 @@ clean:
$(MAKE) -C cfg-to-paths clean
rm -f $(CLASSES)
rm -f $(SOL_DIR)/*.sol
+ rm -f $(SOL_DIR)/*.sol.ready
rm -f $(DEPENDENCY_FILES)
rm -f $(wildcard $(MODEL_INFERRED_DIR)/*.mod)
@@ -117,6 +118,7 @@ clean_model:
clean_solutions:
rm -f $(SOL_DIR)/*.sol
+ rm -f $(SOL_DIR)/*.sol.ready
rm -f $(DEPENDENCY_FILES)
########
@@ -136,7 +138,7 @@ $(SOLUTION_FILES): $(SOL_DIR)/%.sol: $(PROPERTIES_DIR)/%.pro \
$< \
$(LEVEL_FILES) \
$(MODEL_FILES) \
- $(MODEL_INFERRED_DIR)/*.mod \
+ `ls $(MODEL_INFERRED_DIR)/*.mod 2>/dev/null`\
$(wildcard $(PATH_MODEL_DIR)/*.mod)
echo "" >> $@
$(MAKE) -C .. \
diff --git a/sol-pretty-printer/Makefile b/sol-pretty-printer/Makefile
index f5c6e7a..262078b 100644
--- a/sol-pretty-printer/Makefile
+++ b/sol-pretty-printer/Makefile
@@ -48,7 +48,7 @@ CLASSES = $(SOURCES:.java=.class)
SOLUTION_FILES = $(wildcard $(SOL_DIR)/*.sol)
PROPERTY_PP_FILES = $(wildcard $(TEMPLATE_DIR)/*.pp)
SOLUTION_PP_PAIRS = \
- $(foreach sf,$(SOLUTION_FILES),$(sf) $(filter %$(basename $(notdir $(sf))).pp,$(PROPERTY_PP_FILES)))
+ $(foreach sf,$(SOLUTION_FILES),$(sf) $(TEMPLATE_DIR)/$(basename $(notdir $(sf))).pp)
## Makefile Rules ##############################################################
compile: $(CLASSES)