# Exercise Sheet 5 - Question 1.b

Compute the Kripke structure K={I,S,R,L}K={I′,S′,R′,L′}of the FSM: A={2Vin,2Vout,I,2Vstate,R}A={2Vin,2Vout,I,2Vstate,R}
where Vin={a}Vin={a}Vout={}Vout={}Vstate={p,q}Vstate={p,q}I=I=!p&!q,
R=R=a&p&next(p)&next(q)|a&q&!p&!next(p)&!next(q)|a&!p&!q&!next(q)&next(p),
and the following Kripke Structure and state transition diagram.  b) Construct a propositional logic formula that encodes the set of reachable states S'reach of Kripke Structure.

It says wrong in the tool. Could any one help me on this, where I did the mistake.?

Your kripke structure is correct but the set of reachable states is incomplete. You are missing two more states. the states {p,q} and {p,q,a} are also reachable states since they are the successors of a reachable state {p,a}.
by (1k points)
Thank You! I was having the idea that the states will be considered as reachable states only if its direct successors of initial state.
Your reachable states differ from the Kripke structure you drew. From state {a, p}, you can reach {p,q} and {p,q,a}.

by (25.6k points)
Got it, Thank You!