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