search

SRI-CSL / sally

A model checker for infinite-state systems.
http://sri-csl.github.io/sally/
GNU General Public License v2.0
69 stars 12 forks source link

Yices error when invoking sally #53

Open yav opened 6 years ago

yav commented 6 years ago

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 commented 6 years ago

Yes, this is not the best error to report.

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

yav commented 6 years ago

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.