Sheet4/Ex2: How are deadend and init solutions accepted?

Question

Continueing with exercise 2, the link for my first question is [here], i got now the Kripke structure and I have already obtained the reachable states, which by now is rather easy for me. However, I also need the deadend states as well as the initial. So i already solved the exercise 3, which is similar to exercise 2, here we got already a state transition diagram for which we need to get a Kripke structure. Here we also needed to get the deadends and the init states.

Here the Kripke structure for my exercise 3:

i) My accepted solution for the deadends here is: (!p&!q&!a)|(!p&q&a)|(p&q&!a)|(p&!q&!a)
ii) My accepted solution for the init state is: (!p&q&!a)|(p&q&a)

For i) please note how every deadend is counted in the solution, also the unreachable ones.
For ii) please note that the additional init states (p&q&!a) (deadend state) and (!p&q&a) (deadend) are not a part of the accepted solution.
Here I wasted a lot of tries, until I finally got my solution accepted.

Having this in mind I also try to get the deadends and init state for my Kripke structure from exercise 2 (for better readability I am using this screenshot of the tool):


Analogous to my solution for 2, I entered...
- ...the deadends as: (!p&!q&!a&!o)|(!p&!q&!a&o)|(!p&!q&a&!o)|(!p&!q&a&o)|(p&q&!a&!o)|(p&q&a&o)|(p&q&!a&o)|(p&q&a&!o)|(p&!q&!a&!o)|(p&!q&!a&o)|(p&!q&!a&o)|(p&q&!a&o)
- ...the init state (without deadends): (!p&q&!a&o)|(!p&q&a&!o)|(!p&q&a&o)|(!p&q&!a&!o)

however both were not accepted. (Besides my reachable states were accepted with no problems at all)

For the init states I also tried to include to the init state without deadends:

- init states which are also deadends, but have predecessors: (!p&q&!a&o)|(!p&q&a&!o)|(!p&q&a&o)|(!p&q&!a&!o)|(p&q&!a&!o)|(p&q&a&o)|(p&q&!a&o)|(p&q&a&!o)
- init states which are also deadends, regardless of having predecessors or not: (!p&q&!a&o)|(!p&q&a&!o)|(!p&q&a&o)|(!p&q&!a&!o)|(p&q&!a&!o)|(p&q&a&o)|(p&q&!a&o)|(p&q&a&!o)|(!p&!q&!a&!o)|(!p&!q&!a&o)|(!p&!q&a&!o)|(!p&!q&a&o)

These were also not accepted.

I am clueless now on how to enter the solutions, because of coming from exercise 3 which just accepted my solutions under the given circumstances. The question therefor arises, what are init states for the solution systems? Every init state regardless the deadend state or not?
Therefore I am asking for help regarding the deadends and init states.
 

Comments

!p&q&!a&!o

Has only finite paths. Try considering it as a deadend.

---

I added this state to my current list of deadends, but it still does not accept it. As well as for the init states.

---

There also seem to be some typos in your deadend states. Of the last three states, (p&!q&!a&o)|(p&!q&!a&o)|(p&q&!a&o) the first two states are the same, the last state is a repetition of an earlier state.

---

The deadends were finally accepted, thank you very much. And analogous to your first comment, I needed to remove (!p&q&!a&!o) from my set of init states, because it does not start an infinite path.
This clears it up for me, thank you again.

Answer 1

Answer to my question found in the comments.