| 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 /data/property | |
| 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.
Diffstat (limited to 'data/property')
| -rw-r--r-- | data/property/cnes/CNE_01700.pro | 127 |
1 files changed, 66 insertions, 61 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 |