search

loonwerks / jkind

JKind - An infinite-state model checker for safety properties in Lustre
http://loonwerks.com/tools/jkind.html
Other
52 stars 32 forks source link

Inductive Counterexample #2

Closed lgwagner closed 11 years ago

lgwagner commented 11 years ago

pKind supports an inductive counterexample which can be useful to determine which invariant is necessary to prove a property.

Is this easy to support?

agacek commented 11 years ago

It would take about a day to implement so I can do it when I have time. I think Mike has requested this as well. For now, you can use the -scratch option and look for the last outputs from yices in the yc_induct scratch file. It's not the prettiest, but it at least gives you something for now.

agacek commented 11 years ago

Added in commit a46a779241e8e44e32999693bc7369f801ea9931.