- New operation: integer hull [JLR15]
- Syntax
diff c1 , c2allowed, in addition todiff c1 c2
- New operation: projection onto a variables set
- New operation: union over a list of non-necessarily convex constraints
- New operation: applies updates to a polyhedron (i.e. replacing their value with a linear combination of variables)
- New operation:
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.
- New operation to compute 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
- Add operation for exhibition of a point in a polyhedron
- Allow for more than one operation at a time
- Option
-debugbecomes-verbose
- Results are better organized
- Minor corrections in display (fractions, time)
- Renamed most modules
- Added basic non-regression tests
- Add "time past" operation
- Add non-convex difference
- Fix bugs in non-convex inclusion and equality checks
- Allows
OR,orand||as disjunction symbols
- Strip binary (much smaller size)
- Add negation ("not") operation
- Allow disjunctions (using
or) in input constraints
- Now using
_oasisto compile - Now PolyOp has a build number
- Relying entirely on
PPL.Pointset_Powerset_NNC_Polyhedron(even when no disjunction is used)
- Source code on GitHub
First version of PolyOp