Correct format for answer in exercise 11

Question

I'm having a problem submitting the solution for the current exercise. After calculating all the ψ equations I tried to submit them in the format given as an example:

[(!b|c)&!a&!b ; (!b|c)&!a ; (!b|c)&!a]

Hence my solution looked like this:

[!c&(c|!b) ; !c ; !b|!c ; !b|!c]

However the exercise portal tells me that the format is not correct, also after trying other versions containing all variables and different variable orderings. In the end I submitted the example given in this exercise which should of course be the wrong solution for my kripke structure and safety properties but nevertheless its format should be accepted by the system. However this is not the case, even the format example given fails with an error saying the format is incorrect.

So, how should we format our solution then?

Answer 1

I guess your message was this one:

Your submission (or part of it) was not in a correct format and could not be checked
Details: Your solution is not the same as the candidate solution, but your solution may be right, please write an email to your tutor, he/she will check it manually for you.

The PDR algorithm we introduced has some non-deterministic choices. For example, there might be more than one counterexample to induction that need to be excluded. Also, there might be several minimal generalizations of a counterexample. In these cases, our online tool might have generated a solution that took different non-deterministic choices than you. In that case, the only option is that me or your tutor checks your answer manually, and gives you the points.

One more thing that I realized: I'm guessing, you property is !a|!b|!c, and your initial states are !b & !c. Shouldn't the property clause be included in every of your Psi? Also, your first answer seems to exclude one of your initial states.

Comments

Thanks for the answer. This is indeed the error message I get. Could you check my solution then? Also Martin Schmitt has exactly the same task so a correct submission would apply for both of us.

V={a,b,c}
φI=  !b&!c
S=  !a|!b|!c

a & !b & !c & !next(a) & !next(b) & !next(c) |
!a & !b & !c & !next(a) & next(b) & !next(c) |
!a & b & !c & next(a) & next(b) & !next(c) |
a & b & !c & !next(a) & !next(b) & next(c) |
!a & !b & c & next(a) & !next(b) & next(c) |
a & !b & c & !next(a) & !next(b) & !next(c) |
!a & b & c & next(a) & next(b) & next(c) |
a & b & c & !next(a) & next(b) & next(c)

Submission:
[!c&(c|!b) ; !c ; !b|!c ; !b|!c]

---

First, I would start with [(!a|!b|!c)&!b&!c;(!a|!b|!c)]. Psi0 is the property intersected with the initials, Psi1 is the property. Then I try which clauses from Psi0 I can propagate to Psi1. I can't propagate !b because then one of the initial states wouldn't be inductive.

Currently, I don't understand your submission. Maybe, you can have a look at the last paragraph that I added to my answer.

---

The submission is in the format mentioned in the exercise portal. This would be the solution I calculated and also the Online Tool gave me, I hope this is the format in which you wanted me to submit the answer here.

ψ[0] = {s0,s4} = !b & !c = CNF{!c ; c | !b}
ψ[1] = {s0,s2,s4,s6} = !c = CNF{!c}
ψ[2] = {s0,s1,s2,s4,s5,s6} = !c | c & !b = CNF{!b | !c}
ψ[3] = {s0,s1,s2,s4,s5,s6} = !c | c & !b = CNF{!b | !c}

---

Hi Martin,

as Nicola said, I have exactly the same exercise. Would be nice if you could also give me the points as we worked together on this.

---

Ah. Your clauses are cleaned up semantically. So you start with the initial states. You propagate !c but not !b to Psi1. Psi2 seems to be (!a|!b|!c)&(!b|!c). The first clause is the property, the second clause is the generalized negated counterexample. !c can't be propagated any more because it is not inductive. Psi3 then gets all clauses from Psi2, and reaches a fixpoint.

Your solution is correct. Although I would just have written down the original clauses. Here's my solution:

ψ[0] = (!a|!b|!c)&!b&!c
ψ[1] = (!a|!b)&!c&(!a|!b|!c)
ψ[2] = !c&(!a|!b|!c)
ψ[3] = (!b|!c)&(!a|!b|!c)
ψ[4] = (!b|!c)&(!a|!b|!c)

You can see that I both propagate !c from ψ[0] to ψ[1], and add a generalized negated counterexample which I wouldn't have needed to. From ψ[2] on, I do the same as you do in your ψ[1].

---

Hi other Martin,

sure. You got the points.

---

It worked! Thx my Namensvetter :D

---

Not exactly. There are two users whose mail addresses both look like they belong to Martin Schmitt.

Isn't it funny: I thought you meant that the points didn't arrive on your account because there was a Namensvetter (thus, thanks to the existence of a Namensvetter …). That was close to the truth as I didn't find you but someone with a similar name. What you actually meant was that you are thanking me, and I am your Namensvetter. It's remarkable how I just wouldn't find it plausible that someone would act grateful towards me.

Answer 2

The solutions looks good to me. When I check it, I find the following state transition system where the green states are the safety property to be proved. 

The initial set-up checks of PDR are not conclusive, so we start PDR and compute with the teaching tool's implementation (whi

    ψ[0] = {s0,s4} = !b & !c = CNF{!c ; c | !b}
    ψ[1] = {s0,s2,s4,s6} = !c = CNF{!c}
    ψ[2] = {s0,s1,s2,s4,s5,s6} = !c | c & !b = CNF{!b | !c}
    ψ[3] = {s0,s1,s2,s4,s5,s6} = !c | c & !b = CNF{!b | !c}

and that has been submitted. Maybe the final ψ[3] doesn't have to be submitted since that only shows that with the ψ[3]=ψ[2] which means that we found an inductive set which is still a subset of the safety property (and it is the only final solution since these are the reachable states).