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
Hi,
Is my solution correct?
EDIT: Correct Solution as instructed by Professor and Martin.
I think that your solution is not correct. The formulas are both satisfied in the initial state of your structure. I quickly checked it with the model checker and got the following for S2:
The tool then computed
〖!(a & c <-> d & c)〗= {s1;s3;s4;s6}
〖A G !(a & c <-> d & c) | [] Z〗 = {s3;s6}
〖A X A F A G !(a & c <-> d & c)〗 = {s0;s1;s2;s3;s4;s5;s6}