Operations on non-necessarily closed, non-necessarily convex polyhedra: (relatively) simple layer on the Parma Polyhedra Library (PPL), with some hopefully useful additions.
All operations use the Pointset_Powerset NNC_Polyhedron data structure from PPL
Some of the operations allowed by PolyOp:
- intersection
- union
- difference
- negation
- satisfiability
- time elapsing
- time backward-elapsing ("past")
- variable elimination (by existential quantification), or projection onto a variable set
- Boolean tests (inclusion, equality…)
- updates of variable (i.e., replacing their value with a linear combination of variables)
exhibitpoint: exhibition of a concrete point in the polyhedronzonepred: computation of the predecessors of a subset of a zone within a source zone (given the set of variables subject to time-elapsing (typically clocks), and the set of variables reset between the two zones); this function is typically useful to reason about parametric zones in parametric timed automata or parametric time Petri nets [not sure this function corresponds to an actual problem in PTAs / PTPNs]zonepredgu: GivenZn-1andZnsuch thatZnis the successor zone ofZn-1by guardg-1and updating variables inUn-1to some values, givenZn+1a set of concrete points (valuations) successor of zoneZnby elapsing of a set of variablest, by guardgn, updatesRn, thenzonepredgr(Zn-1, gn-1, Un-1, Zn, t, gn, Un, Zn+1)computes the subset of points inZnthat are predecessors ofZn(by updates ofUn, guardgn, elapsing oft), and that are direct successors (without time elapsing) ofZn-1viagn-1andUn-1. This function can typically used when running a backward analysis in a zone graph of a PTA / PTPN.
From version 1.0, several operations can be performed sequentially using the same call to PolyOp
Basic call syntax:
polyop examples/example.polyop
See examples of the input syntax in examples/example.polyop.
(Some more examples in tests/testcases/)
For any information, please feel free to contact me: