Exam problem : 14.02.2018 8 (f) : *2018.02.14.vrs.solutions.pdf (uni-kl.de)
I just want to clarify about my understanding.
I came up with below solution which satisfies S2 and not S1 :
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
