POROUS: Invariant Builder And Reachability Checker for Affine Programs

Input Format Explanation

On the first line write the start point, target and optionally whether you expect it to be reachable. Supported targets are single numbers, or Z-linear sets, with {b+pZ} specified as b+p (note, b+-p is equivalent).
On subsequent lines, write the functions by writing the multiplier and the adder, i.e. a b means f(x) = ax+b.
On the line after the last function, optionally, write ENDS. Everything after ENDS will be ignored, for example here we provide some explanation.


start target[+period] [True|False]
a b
a b

Input area


Output area

Tool implemented by David Purser, for the paper Porous Invariants by Engel Lefaucheux, Joël Ouaknine, David Purser and James Worrell
Code on GitHub