[PPL-devel] Write constraints in JAVA interface as in C++ ?

[Zell]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.cs.unipr.it/pipermail/ppl-devel/attachments/20120731/b8158be2/attachment.htm>