[PPL-devel] Re: Convex hull
Enrico Oliosi
enrico.oliosi at students.univr.it
Thu Oct 7 14:37:43 CEST 2004
On Thu, 7 Oct 2004, Roberto Bagnara wrote:
> Enrico Oliosi wrote:
>> I analysed this program:
>>
>> BEGINPRG
>> Read(i);
>> j:=0;
>> IF (i >= 0) THEN {
>> j:= i+2;
>> [p1]={j=0; i>=0; j-i=2}
>> } ELSE {
>> j:= i;
>> [p2]={j=0; -i>0; j-i=0}
>> }
>> FI;
>> [1=0]
>> ENDPRG
>>
>> when I done the convex-hull using:
>>
>> [p1].poly_hull_assign_and_minimize([p2]);
>>
>> the result has been the empty polyhedron ([1=0]).
>
> Dear Enrico,
>
> what you obtain is not surprising at all: since both p1 and p2
> are empty polyhedra, their poly-hull is the empty polyhedron.
>
>> (if I use the function [p1].poly_hull_assign([p2]) the poly_hull
>> returns [p2]);
>
> This is still OK: the method poly_hull_assign() does not minimize
> the result and, since p1 is empty it simply gives you back p2.
>
> I think that the problem is elsewhere: the constraint `j=0'
> should not, I believe, be in p1 nor in p2.
OK but in Cousot&Halbwachs76 if I have a linear test C and P the
enter polyhedron P-true is defined as:
P-true = P intersection C ( P-false = P intersecrion not(C) ).
If P is [j=0] and C is [i>=0] the intersection (P.intersection_assign_and_minimize(C);)
returns the Polyhedron P' = [j=0,i>=0]; the same holds for P_false ([j=0,i<0]).
What do I wrong? Probably I don't understand the guard rules very well....
Thanks,
Enrico
More information about the PPL-devel
mailing list