[PPL-devel] Fwd: Re: Widening operation in Powerset

[Roberto Bagnara]

On Mon, 20 Jun 2011 00:52:47 +0530, Gokul Ramaswamy wrote:
> Prof. Roberto Bagnara,
>
> I need your help again. I have an example (the attached file).
> It gives the following output : { A - C = 0, -A >= -9, A >= 1 }, { B = 63 }
> But I was expecting the answer : { A - C = 0, A >= 1 }, { B = 63 }
> as the constraint A<=9 is violated by A==10 in the powerset poly3.
>
> I may be wrong as I am still learning Powerset Abstraction.

Hi Gokul.

The documentation of

   void BHZ03_widening_assign(const Pointset_Powerset& y, Widening wf);

clearly states that `y' /must/ definitely entail `*this.
In your example,  `*this' is
{ A - C = 0, -A >= -9, A >= 1 }, { B = 63 }
and `y' is { C = 10, A = 10 }, so entailment does not hold.
Cheers,

    Roberto

P.S. Please direct all messages to ppl-devel at cs.unipr.it

-- 
Prof. Roberto Bagnara
Applied Formal Methods Laboratory
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara at cs.unipr.it