[PPL-devel] Re: Convex hull

[Roberto Bagnara]

Enrico Oliosi wrote:
> 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....

Enrico,

I don't have the 1978 paper by Cousot & Halbwachs at hand.
However, if I interpret correctly what you write, P-true is the
entry condition to the true branch and P-false is the entry
condition to the false branch.  So up to here we all agree.

Where we disagree is that your annotations p1 and p2 still
have the constraint `j = 0', which is wrong.  I don't know
what you are doing.  What you should do is, I believe, to compute
p1 as the affine image of P-true with respect to j = i+2 and
p2 as the affine image of P-false with respect to j = i.
These images would not have the constraints `j = 0' that
you have.

To summarize, here is what you should have and what I obtain
with the PPL:

*** P_true ***
j = 0,
i >= 0.
*** P_false ***
j = 0,
-i > 0.
*** After P_true.affine_image(j, i+2), call this p1 ***
i - j = -2,
j >= 2.
*** After P_false.affine_image(j, i), call this p2 ***
i - j = 0,
-i > 0.
*** After p1.poly_hull_assign_and_minimize(p2) ***
i - j >= -2,
-i + j >= 0.

Please, let us know if this clarifies things enough.
Ciao,

       Roberto

-- 
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara at cs.unipr.it