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

Uncaught Exception #44

Closed lgwagner closed 6 years ago

lgwagner commented 6 years ago

The IVC engine is crashing with the following error:

jkind.JKindException: Unable to find property event7_false_c4 during reduction at jkind.engines.IvcReductionEngine.getInvariantByName(IvcReductionEngine.java:77) at jkind.engines.IvcReductionEngine.reduce(IvcReductionEngine.java:65) at jkind.engines.IvcReductionEngine.handleMessage(IvcReductionEngine.java:289) at jkind.engines.messages.ValidMessage.accept(ValidMessage.java:43) at jkind.engines.messages.MessageHandler.handleMessage(MessageHandler.java:31) at jkind.engines.messages.MessageHandler.processMessagesAndWaitUntil(MessageHandler.java:39) at jkind.engines.IvcReductionEngine.main(IvcReductionEngine.java:59) at jkind.engines.Engine.run(Engine.java:35) at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37) at java.lang.Thread.run(Thread.java:748)

The lustre file to exercise the error is attached as a text file.

bug.txt

lgwagner commented 6 years ago

oops...

jkind -solver z3 -ivc bug.lus also occurs with jkind -ivc bug.lus

mwwhalen commented 6 years ago

Very good.

Mike

On Wed, Feb 21, 2018 at 9:30 AM, Lucas Wagner notifications@github.com wrote:

oops...

jkind -solver z3 -ivc bug.lus also occurs with jkind -ivc bug.lus

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/agacek/jkind/issues/44#issuecomment-367364180, or mute the thread https://github.com/notifications/unsubscribe-auth/AE-autSBPW5cAMdE2q5L2Mg_QxdV5Aqpks5tXDaigaJpZM4SNyxU .

-- Michael Whalen Director, University of Minnesota Software Engineering Center (UMSEC) 200 Union St. 4-192 Minneapolis, MN 55455 Office: 612-624-5130 Cell: 651-442-8834