I have a question regarding the following example:
I tried to solve it in the same way shown in the lecture video (https://es.cs.uni-kl.de/teaching/vrs/videos/VRS-04-Transitionsystems-3.html 1:08:00):
However, this does not lead to the right answer (right answer is seen above).
I also used the Tool:
I quess that one could also rephrase my question into: "Why is there no transition from the state (p,a) to itself"?
IMO there should be one since p and p' would be satiesfied and therefore (next(p)|next(q)->a&!(o->q))&p would be true.