data/property/impossible_processes.pro


1
2
3
4
5
6
7
8
9
10
11
12

(tag_existing
   (
      (ps process WHAT_ARE_YOU_DOING)
   )
   (forall sl1 waveform
      (CTL_verifies ps
         (not
            (EF (expr_writes sl1))
         )
      )
   )
)