4 lines
687 B
Plaintext
4 lines
687 B
Plaintext
|
[] <> (WD1_finished /\ WD2_finished /\ WD3_finished);
|
||
|
|
[] (((WD1_idle /\ -WD1_running /\ -WD1_finished) \/ (-WD1_idle /\ WD1_running /\ -WD1_finished) \/ (-WD1_idle /\ -WD1_running /\ WD1_finished)) /\ ((WD2_idle /\ -WD2_running /\ -WD2_finished) \/ (-WD2_idle /\ WD2_running /\ -WD2_finished) \/ (-WD2_idle /\ -WD2_running /\ WD2_finished)) /\ ((WD3_idle /\ -WD3_running /\ -WD3_finished) \/ (-WD3_idle /\ WD3_running /\ -WD3_finished) \/ (-WD3_idle /\ -WD3_running /\ WD3_finished)));
|
||
|
|
[] ((WD1_finished => [](-WD1_running /\ -WD1_idle /\ WD1_started)) /\ (WD2_finished => [](-WD2_running /\ -WD2_idle /\ WD2_started)) /\ (WD3_finished => [](-WD3_running /\ -WD3_idle /\ WD3_started)));
|