If an unknown identifier appears in a property, JKind will throw an NPE rather than yielding a descriptive error.

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

If an unknown identifier appears in a property, JKind will throw an NPE rather than yielding a descriptive error. #5

Closed lgwagner closed 11 years ago

lgwagner commented 11 years ago

lgwagner@jepsen:~/patterns/microwavejkind microwave.lus Exception in thread "main" java.lang.NullPointerException at java.util.AbstractCollection.addAll(Unknown Source) at jkind.slicing.LustreSlicer.getPropertyDependencies(LustreSlicer.java:24) at jkind.slicing.LustreSlicer.slice(LustreSlicer.java:17) at jkind.Main.main(Main.java:49)

Please ask me for my microwave.lus file that exhibits the error.