[PPL-devel] [Fwd: Fwd: Info on PPL]

[Enea Zaffanella]

Giorgio wrote:
> Enea,
>   thanks a lot for the prompt reply.

[...]

I made an small (irrelevant) error:
clearly, the intermediate poly-hull hull_2 cannot have an upper bound 
constraint for dimension y:

>>    Q_2 := hull_2.H79_widening_assign(Q_1) = Q_1 (fixpoint)
>>      where
>>       hull_2 := the poly-hull of P_2 and Q_1
>>               = { x = y, 0 <= y <= 2 }

It is hull_2 = { x = y, 0 <= y }  ( = Q_1)


> Ok. Is this the same as CH78  widening (based on constraint deletion)?

It is basically that one, but enhanced so as to be well-defined even 
when the two arguments have a different affine dimension; the name H79 
refers to the year of the PhD thesis of Halbwachs. For all the details, 
you can also have a look to

    Precise Widening Operators for Convex Polyhedra.
    Roberto Bagnara, Patricia M. Hill, Elisa Ricci, and Enea Zaffanella.
    Science of Computer Programming, 58(1-2), pp. 28-56, 2005.

>  We tried CC76_extrapolation on BDS but we probably forgot to compute 
> the union.

That is an important requirement: all the widening operators in the PPL 
assume that the current iterate, i.e., the object to be modified, is 
greater than (in lattice theoretic terms) of the previous iterate, i.e., 
the argument of the widening method. If such a requirement is not 
satisfied, the behavior is undefined. If you compile the library with 
assertions turned on, it will check the requirement automatically; 
however, this check is too costly to be included in the optimized build.

> To have a similar results for BDS, would it be correct to use something like
> 
> bds1= x=0,y=0
> bds2= x=1,y=1
> 
> bds2=upper_bound_assign(bds1);   // smallest bds union of bds1 and bds2
> bd2=bds2.H79_widening_assign(bds1);
> 
> (I am writing from home and cannot test it right now).
> Thanks,
>  Giorgio & Ahmed

Yes, this should provide the very same result.

Cheers,
Enea.