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 (CC BY-NC-SA 4.0)
Paper: Porous Invariants, CAV 2021, by Engel Lefaucheux, Joël Ouaknine, David Purser and James Worrell. | Published Version | Full paper on arXiv
Data Protection | Imprint