| summaryrefslogtreecommitdiff | 
diff options
| author | Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org> | 2017-07-31 17:04:51 +0200 | 
|---|---|---|
| committer | Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org> | 2017-07-31 17:04:51 +0200 | 
| commit | bc8e275546e2e6fe6bcf19ce42c0fab07eecdf4c (patch) | |
| tree | c0fc19f8cb2a3b296f6fef3394ebee122fe5343c /data/property/cnes/CNE_00100.pro | |
| parent | 27fd5d8afef49ffeca83dd5714738bfaffe04505 (diff) | |
Fixes typo with functions, errors in grammar.
Looking for the groups matching CNE_01700 appears to take a really long
time. The formula is quite complex, yet unlikely to be one of the most
complex ones, so we'll have to see what can be done.
Diffstat (limited to 'data/property/cnes/CNE_00100.pro')
| -rw-r--r-- | data/property/cnes/CNE_00100.pro | 52 | 
1 files changed, 52 insertions, 0 deletions
| diff --git a/data/property/cnes/CNE_00100.pro b/data/property/cnes/CNE_00100.pro new file mode 100644 index 0000000..c5d0319 --- /dev/null +++ b/data/property/cnes/CNE_00100.pro @@ -0,0 +1,52 @@ +(tag_existing +   ( +      (wfm waveform CNE_00100_HAS_BAD_NAME) +   ) +   (and +      (not (string_matches [identifier wfm] ".*_n")) +      (exists p1 process +         (CTL_verifies p1 +            (EF +               (and +                  (kind "if") +                  (is_read_structure "(???)") +                  (is_read_element "0" "=") +                  (or +                     (and +                        (is_read_element "1" "'0'") +                        (is_read_element "2" wfm) +                     ) +                     (and +                        (is_read_element "1" wfm) +                        (is_read_element "2" "'0'") +                     ) +                  ) +               ) +            ) +         ) +      ) +      (not +         (exists p2 process  +            (CTL_verifies p2 +               (EF +                  (and +                     (kind "if") +                     (is_read_structure "(???)") +                     (is_read_element "0" "=") +                     (or +                        (and +                           (is_read_element "1" "'0'") +                           (is_read_element "2" wfm) +                        ) +                        (and +                           (is_read_element "1" wfm) +                           (is_read_element "2" "'0'") +                        ) +                     ) +                  ) +               ) +            ) +         ) +      ) +   ) +) | 


