Property Directed Reachability

Question

Hi, I am trying to solve the following problem:

These are my calculations (I did not write down every step explicitely):

but I got the following error 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.

This irritated me, since I assumed the solution to be unique because there is only one counterexample (s5). Therefore, I assume that I am wrong somewhere - can you help me ?

Comments

I think I found my mistake, it was a transfer error / typo... I propagated !c but added a in psi1

Answer 1

I think I found my mistake, it was a transfer error / typo... I propagated !c but wrote down a in psi1. Here is the corrected version:

Sadly, I still get the same error message (however I now somehow have 55 points??)

I also checked with the tool and got the following solution:

• ψ[0] = {s4,s6} = a & !c = CNF{!c ; a | c}
• ψ[1] = {s0,s2,s4,s6} = !c = CNF{!c}
• ψ[2] = {s0,s2,s3,s4,s6,s7} = !c | b & c = CNF{b | !c}
• ψ[3] = {s0,s2,s3,s4,s6,s7} = !c | b & c = CNF{b | !c}

I guess the tools just removes {!a,b,!c} from psi0,..,3 since {b,!c} already implies {!a,b,!c}.

Same for removing {b,!c} from psi1 ,2 because !c implies {b,!c}.

Comments

Right. I gave you the points. Here's my solution:

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

You can see that I first chose a minimal generalization different from your minimal generalization. Mine then failed. After that incremented the trace with the same generalization you picked.

That's why the solution isn't unique although there's only one counterexample.