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

Handle assertions and properties in subnodes #10

Open agacek opened 11 years ago

agacek commented 11 years ago

JKind should do something with assertions and properties in subnodes. There are different possible semantics for this, but one thing might be to just treat them all as proposed invariants.

agacek commented 11 years ago

I no longer like the idea of using them as proposed invariants. That's too wishy washy. Instead the assertions and properties of a subnode should be treated as full fledged properties (assuming we can figure out reasonable naming). We may want to include an option to not inline a node and instead rely on its properties.