Fixes combinational processes property.

1 files changed, 5 insertions, 11 deletions

diff --git a/data/property/combinational_processes.pro b/data/property/combinational_processes.pro
index b3f2633..b0f0d0c 100644
--- a/data/property/combinational_processes.pro
+++ b/data/property/combinational_processes.pro
@@ -5,28 +5,22 @@
    (forall sl1 waveform
       (and
          (implies
+            ;; If a signal is read,
             (exists target waveform
                (CTL_verifies ps
                   (EF
-                     (and
-                        (is_read_element _ sl1)
-                        (expr_writes target)
-                        (not
-                           (AX
-                              (AF
-                                 (expr_writes target)
-                              )
-                           )
-                        )
-                     )
+                     (is_read_element _ sl1)
                   )
                )
             )
+            ;; Then it must be in the sensitivity list.
             (is_in_sensitivity_list sl1 ps)
          )
          (CTL_verifies ps
             (implies
+               ;; If a signal is somehow assigned by this process,
                (EF (expr_writes sl1))
+               ;; Then it is assigned at every execution of the process.
                (AF (expr_writes sl1))
             )
          )