PolyOp v1.2

release 1.2 (2019-06-18, build 170)

Features

• New operation: applies updates to a polyhedron (i.e. replacing their value with a linear combination of variables)
• New operation: zonepredgu: Given Zn-1 and Zn such that Zn is the successor zone of Zn-1 by guard g-1 and updating variables in Un-1 to some values, given Zn+1 a set of concrete points (valuations) successor of zone Zn by elapsing of a set of variables t, by guard gn, updates Rn, then zonepredgr(Zn-1, gn-1, Un-1, Zn, t, gn, Un, Zn+1) computes the subset of points in Zn that are predecessors of Zn (by updates of Un, guard gn, elapsing of t), and that are direct successors (without time elapsing) of Zn-1 via gn-1 and Un-1. This function can typically used when running a backward analysis in a zone graph of a PTA / PTPN.