# Syntax Problem: Kripke structure parsing

+1 vote

Hello there. I could need some help with the syntax of the Kripke structure parsing.

In VRS Ex. 7 Question 2 a i want to submit my solution. The online parser raises the error: "Your submission (or part of it) was not in a correct format and could not be checked

Details: Kripke structure parsing failed"

My input is:
labels 0:s2,s3; 1:s0,s1; 2:; 3:s1,s3; 4:s4; 5:s0,s1,s3; 6:s1;
labels 0:; 1:s1; 2:; 3:s1,s3; 4:; 5:s1,s3; 6:s1;
init 0;
transitions (0,{},1); (0,{a},2); (1,{},3); (1,{a},4); (2,{a},2); (2,{},2); (3,{a},2); (3,{},5); (4,{a},2); (4,{},6); (5,{a},2); (5,{},6); (6,{a},2); (6,{},3);
accept 1,3,5,6;

Can anyone figure out where my mistake is?

I tried but couldn't find it :(
If you input it in the Automata Construction Tool your solution seems to work with no syntax error. Strange...

+1 vote

I think the graph you described might have a semantic and not a syntactic error. Maybe the graph you described can't be output as the solution of an automaton determinization of a co-büchi automaton. I'd suggest to check your solution again.
by (1.7k points)
selected
The problem was not in the syntax but sitting in front of the computer

In the transitions you are missing a comma in all the transition. Because - I assume in your Kripke structure as well there is no output, like in my exercise - you still have to denote that there could be an output. Putting it in simple words:

You wrote this: (0,{},1)

But it should be this: (0,{},,1)

Other than that I see no formatting issues.

by (650 points)
Sadly, this does not help. I tried it with the double-comma but it doesn't change anything
it still says "parsing failed"? I take another look at that
Yes, the exact same error message was given
Weird, other than that I am not finding any other mistakes beside adding the additional comma for every transition. Sorry
+1 vote

We first need to clarify what you want to describe. Should it be a Kripke Structure or an automaton? States of Kripke structures have labels, but their transitions don't; and Kripke structures have no accepting states. Automata have inputs and outputs which are the labels of their transitions, but their states don't have labels. Accepting automata do not have outputs.

What you described above is a kind a mixture of both. You have labels, but neither inputs nor outputs and your transitions have labels. Also, you have two sections of labels that both describe states starting with index 0.

Looking at the exercise, I can see that your task is to determinize a co-Büchi automaton. Let's consider as an example the one from the lecture notes. The following text describes that automaton:

```inputs a0,a1;
init 0,2;
transitions
(0,a1,3); (3,a1,2); (2,a1,1);(1,a1,0);
(0,a0,0); (1,a0,1); (2,a0,2);(3,a0,3);
accept 2,3;```

where a1 means that we have input a and where a0 means that we have input !a (note that the above text is an explicit description of the automaton where we do not use propositional logic). The state transition diagram looks as follows:

Determinizing this automaton with the breakpoint construction, you will obtain the following automaton:

If you need to describe this one in text format, it should be done as follows:

```inputs a0,a1;
init 0;
transitions
(0,a0,1); (0,a1,3);
(1,a0,1); (1,a1,2);
(2,a0,3); (2,a1,1);
(3,a0,3); (3,a1,1);
accept 1,3;```

Note that it is still an automaton in explicit form, and not a Kripke structure. It is not required to order the transitions in any way, but I recommend for deterministic automata to write per state one line and list the transitions for that state in that line. This way you can double check quickly that you described it complete and correct.

by (166k points)
Thank you for the clarification