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.