summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile4
-rw-r--r--data/property/cnes/CNE_00100.pro2
-rw-r--r--data/property/cnes/CNE_01800.pro2
-rw-r--r--data/property/cnes/STD_04800.pro16
-rw-r--r--instr-to-kodkod/Makefile2
5 files changed, 14 insertions, 12 deletions
diff --git a/Makefile b/Makefile
index 70bf737..cb755f3 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,8 @@
## Makefile Parameters #########################################################
LEVEL_FILES = $(wildcard ${CURDIR}/data/level/*.lvl)
-PROPERTY_FILES = $(wildcard ${CURDIR}/data/property/*.pro)
+PROPERTY_FILES = \
+ $(wildcard ${CURDIR}/data/property/*.pro) \
+ $(wildcard ${CURDIR}/data/property/cnes/*.pro)
AST_FILE = ${CURDIR}/data/ast/best_chronometer_ever.xml
TMP_DIR = /tmp/tabellion
diff --git a/data/property/cnes/CNE_00100.pro b/data/property/cnes/CNE_00100.pro
index 9cab7fc..221008b 100644
--- a/data/property/cnes/CNE_00100.pro
+++ b/data/property/cnes/CNE_00100.pro
@@ -14,7 +14,7 @@
(or
(and
(is_read_element "1" "'0'")
- (IS_READ_Element "2" wfm)
+ (is_read_element "2" wfm)
)
(and
(is_read_element "1" wfm)
diff --git a/data/property/cnes/CNE_01800.pro b/data/property/cnes/CNE_01800.pro
index 78e1094..6895f85 100644
--- a/data/property/cnes/CNE_01800.pro
+++ b/data/property/cnes/CNE_01800.pro
@@ -28,7 +28,7 @@
(is_read_structure "(??(??))")
(is_read_element "1" x_r1)
(is_read_element "2" "not")
- (is_read_element "3" x_)
+ (is_read_element "3" x)
)
)
(AX
diff --git a/data/property/cnes/STD_04800.pro b/data/property/cnes/STD_04800.pro
index 8f998e4..5f9e817 100644
--- a/data/property/cnes/STD_04800.pro
+++ b/data/property/cnes/STD_04800.pro
@@ -13,14 +13,14 @@
)
)
)
- (exists ps_fe process
- (CTL_verifies ps_fe
- (EF
- (and
- (is_read_structure "(??)")
- (is_read_element "0" "falling_edge")
- (is_read_element "1" wfm)
- )
+ )
+ (exists ps_fe process
+ (CTL_verifies ps_fe
+ (EF
+ (and
+ (is_read_structure "(??)")
+ (is_read_element "0" "falling_edge")
+ (is_read_element "1" wfm)
)
)
)
diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index dd94b48..60ad8da 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -93,7 +93,7 @@ CLASSES = $(SOURCES:.java=.class)
SOLUTION_FILES = $(addprefix $(SOL_DIR)/,$(notdir $(PROPERTY_FILES:.pro=.sol)))
MODEL_FILES = \
$(MODEL_DIR)/structural.mod \
- $(MODEL_DIR)/depth.mod \
+ $(MODEL_DIR)/depths.mod \
$(filter-out %structural.mod,$(wildcard $(MODEL_DIR)/cfg_*.mod))
PARSER_SOURCES = $(wildcard parser/*.g4)
PARSER_CLASSES = $(PARSER_SOURCES:.g4=.class)