sheet 4 problem:3

Question

for above problem i got

dead state : (!p&a&!q) | (p&!q&a) | (!p&a&q) | (p&a&q)

initial state:  (!q&!p&!a) | (q&!p&!a) | (p&!a&q)

reachable:  (!p&!a&!q) | (!p&q&!a) | (p&!a&q) | (p&a&q) which are correct in tool 

 but after deleting unreachable node and dead node i have below structure its showing  wrong in tool,i am not getting which part i did wrong:

vars p,q;

init 0,1,2;

labels 0; 1:q,p; 2:q;

transitions 0->1; 1->1; 2->1;

Comments

Your screenshot is not good; we cannot see the initial states, but it seems that the initial states are !(p&!q) according to the diagram shown. Also, please don't give sheet X, problem Y as a title for a question since that does not allow the system to associate it with related question. Note that those not knowing the current sheet, cannot help you, and those in later years will also not find the question and answer useful.

Answer 1

Your task is to produce the Kripke structure, right? Then you probably forgot to add variable a to vars. The Kripke structure is a structure over p, q, a where a is false in every state. That's a subtle difference to a Kripke structure that makes no statements on a.

Answer 2

If I am right, we speak about the following Kripke structure which then shows that not all of your computations are correct: 

After removing the deadend states from the transitions, the following states remain: 

So, it seems that you are right up to here. Please use https://es.cs.uni-kl.de/tools/teaching/SymbolicStateTrans.html to double check. Have a look at Martin's hint to correct your input to the submission tool. 

Comments

It seems that Martin found the problem in your submission.

---

yes .thank you