Surprising behavior when using pdkind #54
Description
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.