Symbolic Computation

Question

 FSM:    where 

 Vin={a} V i n = { a } , Vout={o} , Vstate={p,q} , I = p ∨ q ,  R = next(p)|o&a&!q<->next(q)<->p

How can I compute the existential predecessors of p<->!q? And How the left associativity is distributed among relation R [ Is it the right way to give brackets " ((next(p)|(o&a&!q))<->(next(q))<->p)"  ? ] 

Answer 1

See slides 67-71 of chapter 4 (transition systems for the explanations of the symbolic predecessor and successor computations. Also, the teaching tool on  https://es.cs.uni-kl.de/tools/teaching/SymbolicStateTrans.html can help you to check your computations. For the above example, it computes

∃next(p).∃next(q).(next(p)|o&a&!q<->next(q)<->p)&(next(p)<->!next(q))
  = ∃next(q).!next(q)&(p<->next(q))|(p<->!q&a&o<->next(q))&next(q)
  = !p|(p<->!q&a&o)

Comments

Thank you, Professor. I solved it.