PDR Method (Result not accepted)

Question

Good evening to you all,

i was also trying to solve this exercise 11 with the PDR method, having a given problem. You can all read it hear, as well as my approach to solve it.

I also got this message:

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.

I checked my solution with the tool as well, and with the following structure I also got following solution:

On the first glance my solution seems to go with this, however maybe I can not see the wood for the trees.

I would be really grateful if somebody could look over it and tell me or give me some hints in how to make a solution which is accepted in the exercise sheet.

Answer 1

First of all: The message you got does not mean that you are wrong, it just means that you have not submitted the solution the teaching tool has computed, and therefore it may or may not be correct (a tutor has to check this manually to decide whether to give you the points).

So, let me check that here: The initial checks are not conclusive as you found out and that is true. From here, many ways are possible, and our student portal does currently not check all possible correct results. 

So, you started with with the initial states ψ[0] (where you added the clauses of Phi) and the safety property ψ[1]=Phi:

    ψ[0] = {s1,s5} = a & !b = CNF{!b; a; a|b|!c}
    ψ[1] = {s0,s1,s2,s3,s5,s6,s7} = a|b|!c = CNF{a|b|!c}

That is okay (the teaching tool starts differently). Now you check for CTIs, by checking whether ψ[1]->[]Phi is valid, but it is not valid and you get the counterexample s6->s4 since s6 is in ψ[1] but has as successor s4 which is not in Phi. 

So, you need to check reachability of s6 within one step, and you therefore check  ψ[0] & !ψ[s6] -> []!ψ[s6] which is true since the initial states ψ[0] cannot reach s6. So, we can remove s6 from ψ[1] which could be done by adding the clause !ψ[s6] = !(!a&b&c) = a|!b|!c. 

Maybe we can add a generalized clause, i.e., a subset of {a,!b,!c}? To find out, we have to check for all subsets C of {a,!b,!c} whether (1) ψ[0]&C->[]C and (2) Init->C holds.

Here I don't understand your solution, since you could have generalized the clause, but at the end, you did not (which is also correct, since clause generalization is a matter of optimization).

Hence, you added the clause {a,!b,!c} of !ψ[s6] to the assertions and got now

    ψ[0] = {s1,s5}             = CNF{a|b|!c; a|!b|!c; !b; a; }
    ψ[1] = {s0,s1,s2,s3,s5,s7} = CNF{a|b|!c; a|!b|!c}

which is what you can do. As there is not yet a fixpoint, you continue by checking for CTIs again, and check whether ψ[1]->[]Phi is valid. This time, it is valid, so we have to extend the sequence of assertions, and you add ψ[1] = Phi and got

    ψ[0] = {s1,s5}                = CNF{!b; a; a|b|!c; a|!b|!c}
    ψ[1] = {s0,s1,s2,s3,s5,s7}    = CNF{a|b|!c; a|!b|!c}
    ψ[2] = {s0,s1,s2,s3,s5,s6,s7} = CNF{a|b|!c}

Next, you try to propagate clauses, and you find that our added clause a|!b|!c can be propagated from ψ[1] to ψ[2] which yields a fixpoint. 

Yeap, that is a valid PDR computation, I would say. Write your tutor that you should get your points. I just don't understand why you tried the clause generalization and dropped it, but still it is correct.

Comments

Actually, not using this generalization makes it easier. As I said in my answer, the generalization (a) (which is the most general one), and (a ∨ ¬b) would increase the trace as they kick out reachable (but not yet known to be reachable) states.

---

After reading your answer as well Martin, I think i misunderstood the generalization part. But being lucky it did not interfere with my solution. So have I understood this correctly,: I can use every generalization of this list as long as the result is S for psi_0 and psi_I? I have to pick just cleverly?

Thanks Martin, I will PM you.

---

Yes, that is true. Clause generalization is not always good, but for large examples, it typically is the rule that the more states you cut off, the better it is. But that cannot be said in general, and also not for large examples. It is nothing else but a heuristic.

---

There is another difference between the solution of the student and the one computed by the teaching tool. The student followed the slides (great!!) but the teaching tool has a slightly better (in general) initial set-up in that it propagates clauses from ψ[0] to ψ[1] first to narrow ψ[1] (since typically Phi is too big for being inductive and therefore initially narrowing is a good idea in general. In the example, it then starts with

  * ψ[0] = {s1,s5} = a & !b = CNF{!b | !a ; a}
  * ψ[1] = {s1,s3,s5,s7} = a = CNF{a}

then it has to increment the sequence to

  * ψ[0] = {s1,s5} = a & !b = CNF{!b | !a ; a}
  * ψ[1] = {s1,s3,s5,s7} = a = CNF{a}
  * ψ[2] = {s0,s1,s2,s3,s5,s6,s7} = !c & !b & !a | a | b & !a = CNF{b | a | !c}

where the CTI !a & !b & c, i.e., state s6 is found and cut off (the teaching tool has not implemented clause generalization and skips that part of PDR):

  * ψ[0] = {s1,s5} = a & !b = CNF{!b | !a ; a}
  * ψ[1] = {s1,s3,s5,s7} = a = CNF{a}
  * ψ[2] = {s0,s1,s2,s3,s5,s7} = !c & !a | a = CNF{a | !c}

A final incrementation step with propagating clauses then yields:

  * ψ[0] = {s1,s5} = a & !b = CNF{!b | !a ; a}
  * ψ[1] = {s1,s3,s5,s7} = a = CNF{a}
  * ψ[2] = {s0,s1,s2,s3,s5,s7} = !c & !a | a = CNF{a | !c}
  * ψ[3] = {s0,s1,s2,s3,s5,s7} = !c & !a | a = CNF{a | !c}

Answer 2

As discussed in a previous question, the solutions to PDR are not unique. Hence, your solution might be different to the ones our online tool generates. That's why in many cases, the solutions need to be checked manually.

About your solution: I really like this complete and beautiful documentation of your exercise submission.

I think there is no mistake when you check the generalizations of your counterexample. But an interesting decision which generalizations you don't use. In the first line of these checks, in the left column, you check whether  (a ∨ ¬b) is inductive. You say it is. You are right. Yet, you don't use this generalization. This is clever. Two Psis later, you'd get the transition from s0 to s2, which would be inductive. Similarly, you say that (a) is inductive but don't use this generalization. Also that's clever. Due to transition s7 to s0, you wouldn't be able to propagate a to psi2.

But what I don't get is why you don't use the generalization (a ∨ ¬c). It is inductive. Doesn't exclude the initial states. It syntactically looks more general than your solution (a ∨ ¬b ∨ ¬c). Nevertheless, you stick to (a ∨ ¬b ∨ ¬c). That is fine. You solution looks like it additionally allows a state satisfying (¬a ∧ ¬b ∧ c). In fact, this state is already excluded by the property. Hence, it makes no difference, whether one adds the clause (a ∨ ¬c) or (a ∨ ¬b ∨ ¬c) to the CNF of the property.

You then continue correctly by increasing the trace, and correctly propagating the freshly added clause. The newly added formula is hence equivalent to the previous one. Well done. This is a correct PDR solution.

But here's a mistake: You don't write down Psi2 in your submission. Why not? The example in the exercise does so.

You can try to add Psi2 to your submission. If your submission is still not equivalent to the automatically generated one, PM me your mail address or clear name (or send me a mail referring to this question). You'll get your points.

Comments

I also added Psi_2 but it still would not accept it.

---

Here's my solution. As you see, I had several generalizations that failed until I came to the same solution:

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