Exam problem : 14.02.2018 8 (f) : *2018.02.14.vrs.solutions.pdf (uni-kl.de)
I just want to clarify about my understanding.
![](https://q2a.cs.uni-kl.de/?qa=blob&qa_blobid=16836012320538791720)
I came up with below solution which satisfies S2 and not S1 :
![](https://q2a.cs.uni-kl.de/?qa=blob&qa_blobid=2074020922312612465)
In S2, [a WB b] should hold because a is true in first place and hence as [a WB b] is true so the whole formula is true as c never holds.
In S1, a is true at first and as b and c never holds so in weak before [0 WB 0] results in true and hence both a and [b WB c] coexist hence it is not satisfied.
I also checked with tool :
G (a&!b&!c) -> (([[a WB b] WB c]) & !([a WB [b WB c]])) results Valid.
But I just wanted to know whether my understanding as described as above is correct or not.
Thanks in advance