Dear all,
If I understand correctly, the input for a PPL solver is a linear constraint system $C$, and the output is a (not always) optimal polyhedron represented as linear constraints that cover the points satisfying the original constraint system $C$.
My question is, to use the library in practice, what are we supposed to do to convert Cousot's propagation-rule into a PPL's input which is a linear constraint system. ( Sankaranarayanan gave an algorithm using dualization and Farkas's lemma to compile a linear transition system into a constraint system, however I think there should be other prefered ways to do that because Sankaranarayanan's paper appeared later than PPL. )
Here is an example:
1 x=0; 2: while (x<10){ 3: x = x+1; 4 } 5
Denote X[i] to be the set of possible values of 'x' at the program point 'i'. Then, the propagation-rule à la Cousot should be direct
X[1] = \emptyset X[2] \supset {0} \union X[4] X[3] \supset X2 \intersect (-\infinity, 10) X[4] \supset {x+1 | x\in X[4]} X[5] \supset X2 \intersect [10,\infinity)
How can we convert these set-constraints into PPL's input ?
Thanks for your ideas. Zell.