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

Non-constant division #30

Closed lememta closed 8 years ago

lememta commented 8 years ago

The non-constant division is a bit restrictive. Is there a way to by-pass this? Maybe via an option.

jkind --xml_to_stdout -main AltitudeControl_Demo_SAFETY_REQUIREMENT_1 AltitudeControl_Demo.lus

AltitudeControl_Demo.lus.zip

agacek commented 8 years ago

If you use -solver z3 the non-constant division error becomes just a warning. Z3 is the only solver with non-linear support that JKind uses.

lememta commented 8 years ago

OK Thanks. Btw, is it possible when --xml_to_stdout is specified not output non xml infos, e.g. 'Warning at line 136:74 non-constant division'. It makes the parsing a bit 'dirty'.

agacek commented 8 years ago

I took a look and it would be rather annoying to redirect the warnings and errors in that case. Sorry.