Yices error when invoking sally

[yav]

Hello,

Consider the following trivial transition system:

(define-state-type S () ())
(define-transition-system TS S (= 1 2) (= 1 1))
(query TS (= 1 1))

When I run sally (master, git commit 0b88fe996f230) I get:

Yices error (push): the context state does not allow operation

I am guessing that this has something to do with the initial set of states being empty.

[dddejan]

Yes, this is not the best error to report.

Just to clarify, which do you think it's better to report:

• system is valid,
• system is in deadlock,
• system is valid with warning "might be deadlock".

[yav]

I am not really sure. As far as I understand, the meaning of query is to check if the property holds in all reachable states described by the system, so I guess valid seems reasonable, given that there are no states.

I haven't played around with sally's support for deadlock detection yet, but perhaps if one of the check-deadlock flags is enabled, it would make sense to also report a deadlock as there is certainly no next-possible state. What seems odd about that is that if we wanted to show a trace that leads to the deadlock, the trace would have to be empty.