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.

Format

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

Input area

Examples:


Output area




Tool: Implemented by David Purser | Code on GitHub
Paper: Porous Invariants, CAV'21, by Engel Lefaucheux, Joël Ouaknine, David Purser and James Worrell. | Full paper on arXiv