I am having issues computing the transitions from a given FSM relation formula

Question

for a given question i have the transition relation given as follows : R=(o|a->!(p->q))&next(q)&next(p). and an initial state !(p->q)

I have computed the DNF and i got this: (¬O ∧ ¬A ∧ p' ∧ q') ∨ (P ∧ ¬Q ∧ p' ∧ q')

I computed all possible transitions with the given DNF and i arrived at this:

init 1;

transitions (0,{},{},3);(1,{},{},3); (2,{},{},3); (3,{},{},3);(1,{a},{},3);(1,{},{o},3);(1,{a},{o},3);(1,{},{},3);

My transitions correspond with the diagram i generated with the tool, but the excercise tool keeps on rejecting the answer.

Comments

Please don't use question 2 exercise sheet 4 as a title for a question since that does not allow the system to associate it well with related question. Note also that those not knowing the current sheet, cannot help you, and those in later years will also not benefit from the question and answer. Better tell us what the problem is and use that also in the title.

---

Have you thought about removing unreachable states?

---

i just tried removing unreachable states and i am left with
init 1;
transitions (3,{},{},3);(1,{a},{},3);(1,{},{o},3);(1,{a},{o},3);(1,{},{},3);
but the answer is still rejected

---

With which message does the exercise tool reject your answer? Did you notice that you listed transition (1,{},{},3) twice?

---

the message from the excercise tool is "Your solution was not correct (0%)
Submission is not equivalent to solution." After i removed the unreachable states i got this "init 1;
transitions (3,{},{},3);(1,{a},{},3);(1,{},{o},3);(1,{a},{o},3);(1,{},{},3);" which doesn't have any repeated transitions. The tool still rejects it

---

You must have contiguous numbers of states, thus no gaps. You have two states but use numbers 1 and 3 so that the tool assumes that there is another state 2 without transitions. Rename 3 to 2.

---

The labeling is fixed in this task. States can't be renamed.

Also, I meant keeping all states and transitions but not listing the same transition twice.

---

yeah the labels are fixed depending on the state

---

So when I said earlier that you should try removing the redundant transition, I meant just removing this single transition. So keep all the unreachable states, and transitions, and just remove one of the copies of (1,{},{},3).

---

that worked, many thanks.

Answer 1

So you have 

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

which yields the following full DNF:

    ¬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)

So there are seven transitions, and encoding the states, we have: 

    0 -- {}/{} --> 3 
    2 -- {}/{} --> 3
    1 -- {}/{} --> 3
    1 -- {a}/{o} --> 3
    1 -- {a}/{} --> 3
    1 -- {}/{} --> 3
    3 -- {}/{} --> 3

Removing states 0 and 2 will leave

    1 -- {}/{} --> 3
    1 -- {a}/{o} --> 3
    1 -- {a}/{} --> 3
    1 -- {}/{} --> 3
    3 -- {}/{} --> 3

That should be correct. Isn't it?

Comments

why do we remove states 0 and 2 ?

---

I don't know the exercise precisely, you did not mention the problem. But when the task should be to reduce the FSM by removing deadend states and unreachable states, then states 0 and 2 should be removed as unreachable states. Otherwise, it is no problem to have them.