Also in struggle with Sheet4/Ex2

Question

And again, I am now in struggle with exercise 2.

Comments

Could you please explain what Sheet4/Ex2 is about? Remember the questions and answers should also be useful for students in another semester later on. It would also help others to give you an answer.

---

Oh sorry, we have a given FSM with given propositional formula for the initial states as well as one for the transition. The question for the first part of the exercise, which i am no struggling at, is to derive from this FSM the state transition diagram. For this we shall maintain the given labels (seen in picture) as well as the inputs {a}, {} and outputs {o},{}

Answer 1

Here is the cruel way to solve it: We compute a full DNF for the transition relation

    (next(q)  ∧  ¬(q->p)  ∧  (a ∨ o ∨ next(p)))

which is

    ¬p ∧ q ∧ ¬a ∧ ¬o ∧  next(p) ∧ next(q) ∨ 
    ¬p ∧ q ∧ ¬a ∧  o ∧  next(p) ∧ next(q) ∨ 
    ¬p ∧ q ∧  a ∧ ¬o ∧  next(p) ∧ next(q) ∨ 
    ¬p ∧ q ∧  a ∧  o ∧  next(p) ∧ next(q) ∨ 
    ¬p ∧ q ∧ ¬a ∧  o ∧ ¬next(p) ∧ next(q) ∨ 
    ¬p ∧ q ∧  a ∧ ¬o ∧ ¬next(p) ∧ next(q) ∨ 
    ¬p ∧ q ∧  a ∧  o ∧ ¬next(p) ∧ next(q)

Hence, you should have seven transitions in the explicit representation of the transitions. They all start in state {q} and either go to state {q} or to state {p,q}.

Comments

Thank you very much, so my thoughts in my comment after @Martin's response was right. So an additional thank you for Martin as well.

Answer 2

You've forgotten some transitions. For each line, you wrote only one transition. Just that a line doesn't mention a variable doesn't mean it needs to be false. Hence, every line should become four transitions.

The initial states however are completely correct.

Comments

In this part of the exercise, I just need to have the state transition diagram. So according to this, should this be now:
(2, {a}, {o}, 2);
(2, {a}, {}, 2);
(2, {}, {o}, 2);  --- here the transition (2, {}, {}, 2); is not added because in the first to clausel there is at least one input/output to be true.

(2, {a}, {o}, 3);
(2, {a}, {}, 3);
(2, {}, {o}, 3);
(2, {}, {}, 3);