- New operation: integer hull [JLR15]
- Syntax
diff c1 , c2
allowed, 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-1
andZn
such thatZn
is the successor zone ofZn-1
by guardg-1
and updating variables inUn-1
to some values, givenZn+1
a set of concrete points (valuations) successor of zoneZn
by 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 inZn
that are predecessors ofZn
(by updates ofUn
, guardgn
, elapsing oft
), and that are direct successors (without time elapsing) ofZn-1
viagn-1
andUn-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
-debug
becomes-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
,or
and||
as disjunction symbols
- Strip binary (much smaller size)
- Add negation ("not") operation
- Allow disjunctions (using
or
) in input constraints
- Now using
_oasis
to 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