Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.3k answers

1.7k comments

556 users

0 votes

S1=[b SB [a WB c]]

S2=[b WB [a WB c]]

My solution is:

2 ; G (!b & !a &c) ; c & X (!c & a) & G (!b & !a)

I checked it with the tool and both formulas are valid but my solution is not accepted in the exercise system.

in * TF "Emb. Sys. and Rob." by (180 points)

1 Answer

0 votes
Case 2 means that !S1&S2 will be implied, but we have S1->S2, i.e., [b SB [a WB c]] -> [b WB [a WB c]] is valid. Hence, you should better go for case 1.

For case 1,  G (!b & !a &c) is good.

Your second formula is however equivalent to false: G(!b&!a) contradicts to X a.
by (170k points)
edited by
Case 2 was the case to go.

I came up with the simple solution:  2 ; G (!b & !a &c) ; G (!b & a &c)
Yes, you are right. Case 2 means !S1&S2 which can be satisfied since S2->S1 is not valid. Above, I wrote that S1->S2 is valid (which is true), but that means that we should go for case 2 as you did.
Imprint | Privacy Policy
...