Surprising behavior when using `pdkind`

[yav]

Consider the following model: x is the "state" proper, and ok is a bool that keeps track of some property of the state (in this case that 0 <= x). If I ask sally to prove this property using pdkind, it succeeds immediately. However, if I ask it to show that ok will always be true, it loops forever. Looking at the debug output, it would appear that the algorithm gets stuck at the very beginning and keeps exploring various states with x negative, which are immediately rejected.

(define-state-type S ((ok Bool) (x Int)))
(define-transition-system TS S
   (and (= x 0)
        (= ok (<= 0 x))
   )
   (and
      (= next.x  (+ 1 state.x))
      (= next.ok (<= 0 next.x))
  )
)
(query TS (<= 0 x))  ; Query 1, works
(query TS ok)        ; Query 2, does not work

Is there some sort of intuition on the difference between these two? The main difference I can see is that in the first query, the predicate is "obvious", while in the second it is not clear that ok is essentially the same thing all the time.

[dddejan]

Yes, in the second query it is not clear what OK is until you unroll: the 1st query is inductive while 2nd query is 2-inductive.

That aside, the pdkind engine works best with interpolation. Since Yices2 doesn't support it yet, if you can use MathSat5, you can prove this with option --solver y2m5.

./src/sally --engine pdkind --solver y2m5 -v 1 test.mcmt --show-invariant --no-lets
[2018-11-01.08:01:03] Processing test.mcmt
[2018-11-01.08:01:03] pdkind: starting search
[2018-11-01.08:01:03] pdkind: working on induction frame 0 (1) with induction depth 1
[2018-11-01.08:01:03] pdkind: pushed 1 of 1
[2018-11-01.08:01:03] pdkind: search done: valid
valid
(invariant 1 (<= 0 x))
[2018-11-01.08:01:03] pdkind: starting search
[2018-11-01.08:01:03] pdkind: working on induction frame 0 (1) with induction depth 1
[2018-11-01.08:01:03] pdkind: pushed 2 of 2
[2018-11-01.08:01:03] pdkind: search done: valid
valid
(invariant 1 (and ok (<= 0 x)))