Rantanplan

This is the temporary home for Rantanplan, a formal verification tool for Lustre.

Download

Quick start guide

To verify a Lustre program, the top-level node must be an observer with one boolean output stream for each property. For a file named car.lus and a top level node v1, the command is 

[anders@kmsweng183 examples]$ rantanplan --verify car.lus --node v1
Valid. All checks succeeded. Maximal depth was 1.

The examples above all include a supplementary file combinators.lus. Rantaplan looks for included files in the current directory by default. This can be changed with the flag --root: 

[anders@kmsweng183 examples]$ rantanplan --verify car.lus --root /path/to/examples/ --node v1
Valid. All checks succeeded. Maximal depth was 1.

In the examples, top nodes for valid properties have names matching v[1-9][0-9]*.

(Incomplete) flag reference

--cutoff number Stop the proof attempt at a given depth
Default: off
--filter method Sets the IIS filtering method used in GLPK. The possible values are:
deletionDeletion filtering
rdeletionReverse deletion filtering
additiveAdditive filtering
radditiveReverse additive filtering
additive/deletionAdditive/Deletion filtering
radditive/deletionReverse additive/deletion filtering
elasticElastic (+deletion) filtering
noneNo filtering
Default: --filter deletion
--help Prints a help message.
--mathsat [base|ind|both] Generate MathSAT instances. Used together with cutoff.
Default: off
--method translation Changes the translation scheme for integer arithmetic. The possible values are:
bitvecUse bit vectors
guardedGuarded constraints
maximalOrdinary constraints
nodelevelOrdinary constraints
Default: --method maxgen
--node name The name of the top node
--nusmv [generic|number] Generate NuSMV problems
Default: off
--offline solver(s) Sets the offline constraint solver(s). The possible values are:
glpkGLPK
pooh,glpkIncomplete procedure & GLPK
rpooh,glpkIncomplete procedure (reverse order) & GLPK
poohm,glpkIncomplete procedure (multiple ISs) & GLPK
rpoohm,glpkIncomplete procedure (reverse order, multiple ISs) & GLPK
noneNone. (Not recommended)
Default: --offline rpooh,glpk
--online solver Sets the online constraint solver. The possible values are:
glpkGLPK
poohIncomplete procedure
noneNo online procedure
Default: --online none
--root path The directory where Rantanplan will search for included files
Default: --root .
--verbose Be verbose. Prints one line per base case/induction step on standard output.
Default: off
--verify Verify all boolean outputs of the top node.
Default: off

All flags from Luke work in the same way in Rantanplan.

This document last modified Monday February 21, 2005