Dear all, <br>
<br> 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$. <br>
<br>
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. ) <br>
<br>
Here is an example: <br>
<br>
1    x=0;<br>
2:   while (x<10){<br>

3:           x = x+1;<br>
4    }<br>
5<br>
<br>
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<br>
<br>
<br>
X[1]        =   \emptyset<br>

X[2] \supset {0} \union X[4]<br>
X[3] \supset X2 \intersect (-\infinity, 10)<br>
X[4] \supset {x+1 | x\in X[4]}<br>
X[5] \supset X2 \intersect [10,\infinity)<br>
<br>
How can we convert these set-constraints into PPL's input ? <br>
<br>
Thanks for your ideas.<br>
Zell.<br><br><br>