| summaryrefslogtreecommitdiff |
diff options
| author | Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org> | 2017-08-01 10:04:25 +0200 |
|---|---|---|
| committer | Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org> | 2017-08-01 10:04:25 +0200 |
| commit | 798dea30c7832f8c6364d1734423c6a6fda1ce57 (patch) | |
| tree | 908b316421d31c87d0c6f4603af8b6d464ab613e | |
| parent | bc8e275546e2e6fe6bcf19ce42c0fab07eecdf4c (diff) | |
Fixes regex predicate + optimizes CNE_01700.
The combination of those two changes makes the solving much faster, but
since BCE does not have anything that would be matched, it may also
simply be incorrect.
| -rw-r--r-- | data/property/cnes/CNE_01700.pro | 127 | ||||
| -rw-r--r-- | instr-to-kodkod/parser/PropertyParser.g4 | 4 |
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) |