6 lines
399 B
Plaintext
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
|