1 files changed, 80 insertions, 8 deletions
diff --git a/data/property/cnes/STD_04800.pro b/data/property/cnes/STD_04800.pro
index 5f9e817..ae8e4c9 100644
--- a/data/property/cnes/STD_04800.pro
+++ b/data/property/cnes/STD_04800.pro
@@ -6,10 +6,46 @@
       (exists ps_re process
          (CTL_verifies ps_re
             (EF
-               (and
-                  (is_read_structure "(??)")
-                  (is_read_element "0" "rising_edge")
-                  (is_read_element "1" wfm)
+               (or
+                  (and
+                     (is_read_structure "(??)")
+                     (is_read_element "0" "rising_edge")
+                     (is_read_element "1" wfm)
+                  )
+                  (and
+                     (is_read_structure "(?(??)(???))")
+                     (is_read_element "0" "and")
+                     (is_read_element "1" "event")
+                     (is_read_element "2" wfm)
+                     (is_read_element "3" "=")
+                     (or
+                        (and
+                           (is_read_element "4" wfm)
+                           (is_read_element "5" "'1'")
+                        )
+                        (and
+                           (is_read_element "4" "'1'")
+                           (is_read_element "5" wfm)
+                        )
+                     )
+                  )
+                  (and
+                     (is_read_structure "(?(???)(??))")
+                     (is_read_element "0" "and")
+                     (is_read_element "1" "=")
+                     (or
+                        (and
+                           (is_read_element "2" wfm)
+                           (is_read_element "3" "'1'")
+                        )
+                        (and
+                           (is_read_element "2" "'1'")
+                           (is_read_element "3" wfm)
+                        )
+                     )
+                     (is_read_element "4" "event")
+                     (is_read_element "5" wfm)
+                  )
                )
             )
          )
@@ -17,10 +53,46 @@
       (exists ps_fe process
          (CTL_verifies ps_fe
             (EF
-               (and
-                  (is_read_structure "(??)")
-                  (is_read_element "0" "falling_edge")
-                  (is_read_element "1" wfm)
+               (or
+                  (and
+                     (is_read_structure "(??)")
+                     (is_read_element "0" "falling_edge")
+                     (is_read_element "1" wfm)
+                  )
+                  (and
+                     (is_read_structure "(?(??)(???))")
+                     (is_read_element "0" "and")
+                     (is_read_element "1" "event")
+                     (is_read_element "2" wfm)
+                     (is_read_element "3" "=")
+                     (or
+                        (and
+                           (is_read_element "4" wfm)
+                           (is_read_element "5" "'0'")
+                        )
+                        (and
+                           (is_read_element "4" "'0'")
+                           (is_read_element "5" wfm)
+                        )
+                     )
+                  )
+                  (and
+                     (is_read_structure "(?(???)(??))")
+                     (is_read_element "0" "and")
+                     (is_read_element "1" "=")
+                     (or
+                        (and
+                           (is_read_element "2" wfm)
+                           (is_read_element "3" "'0'")
+                        )
+                        (and
+                           (is_read_element "2" "'0'")
+                           (is_read_element "3" wfm)
+                        )
+                     )
+                     (is_read_element "4" "event")
+                     (is_read_element "5" wfm)
+                  )
                )
             )
          )