MTL_Monitor/tests/washing_machine/properties/props.txt

6 lines
399 B
Plaintext

---------------------------------------------WASHING_MACHINE----------------------------------------------
(1) !(drain ^ dry) ---> satisfied by prog1_3
(2) START -> box [7,11] wash ---> satisfied by prog1, sometimes by prog3
(3) fill -> O (fill v soak ) ---> satisfied by prog1_3
(4) start -> Dia [4,6] soak ---> satisfied by prog1_3f
(5) start U [0,19] dry ---> should be satisfied only by prog3