summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--data/property/cnes/CNE_01700.pro127
-rw-r--r--instr-to-kodkod/parser/PropertyParser.g44
2 files changed, 68 insertions, 63 deletions
diff --git a/data/property/cnes/CNE_01700.pro b/data/property/cnes/CNE_01700.pro
index 6b77fa1..a0cb792 100644
--- a/data/property/cnes/CNE_01700.pro
+++ b/data/property/cnes/CNE_01700.pro
@@ -7,34 +7,38 @@
(exists x waveform
(exists x_r1 waveform
(and
- (exists clk1 waveform
- (exists ps1 process
- (and
- (is_explicit_process ps1)
- (is_in_sensitivity_list clk1 ps1)
- (or
- (CTL_verifies ps1
- (AF
- (and
- (kind "if")
- (is_read_structure "(??)")
- (or
- (is_read_element "0" "falling_edge")
- (is_read_element "0" "rising_edge")
- )
- (is_read_element "1" 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)
+ (exists ps1 process
+ (and
+ (is_accessed_by x_r1 ps1)
+ (is_accessed_by x ps1)
+ (is_explicit_process ps1)
+ (exists clk1 waveform
+ (and
+ (is_in_sensitivity_list clk1 ps1)
+ (or
+ (CTL_verifies ps1
+ (AF
+ (and
+ (kind "if")
+ (is_read_structure "(??)")
+ (or
+ (is_read_element "0" "falling_edge")
+ (is_read_element "0" "rising_edge")
+ )
+ (is_read_element "1" 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)
+ )
)
)
)
@@ -44,39 +48,39 @@
)
)
)
- )
- (exists rst1 waveform
- (and
- (is_in_sensitivity_list rst1 ps1)
- (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")
- (is_read_structure "(??)")
- (or
- (is_read_element "0" "falling_edge")
- (is_read_element "0" "rising_edge")
- )
- (is_read_element "1" 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)
+ (exists rst1 waveform
+ (and
+ (is_in_sensitivity_list rst1 ps1)
+ (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")
+ (is_read_structure "(??)")
+ (or
+ (is_read_element "0" "falling_edge")
+ (is_read_element "0" "rising_edge")
+ )
+ (is_read_element "1" 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)
+ )
)
)
)
@@ -99,6 +103,7 @@
(and
(is_in_sensitivity_list x_r1 ps2)
(is_in_sensitivity_list x ps2)
+ (is_accessed_by x_re ps2)
(CTL_verifies ps2
(AF
(and
diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4
index e6cd164..021f02c 100644
--- a/instr-to-kodkod/parser/PropertyParser.g4
+++ b/instr-to-kodkod/parser/PropertyParser.g4
@@ -340,8 +340,8 @@ regex_special_predicate [Variable current_node]
(
Main.get_model().get_predicate_as_relation
(
- "is_start_node"
- ).transpose()
+ "string_matches"
+ )
);
}
catch (final Exception e)