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

Roberto Bagnara bagnara at cs.unipr.it
Sun Jun 19 21:37:21 CEST 2011

```
-------- Original Message --------
Subject: 	Re: [PPL-devel] Widening operation in Powerset
Date: 	Mon, 20 Jun 2011 00:52:47 +0530
From: 	Gokul Ramaswamy <gokulhcramaswamy at gmail.com>
To: 	Roberto Bagnara <bagnara at cs.unipr.it>

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.

On Sat, Jun 18, 2011 at 12:32 PM, Roberto Bagnara <bagnara at cs.unipr.it <mailto:bagnara at cs.unipr.it>> wrote:

On 06/17/11 21:22, Gokul Ramaswamy wrote:

I have understood that, in the polyhedron class, there is a BHRZ03_widening_assign() function which
basically does the widening operation. But I am dealing with set of Polyhedrons, so I am using a Powerset
class for it. But in the powerset class, I cannot find any widening operator. I want to do widening on my set
of polyherdrons. Can someone please point me in the right direction in this regard.

Hi Gokul.

for the Pointset_Powerset (applied to any class of polyhedra) you can use
BHZ03_widening_assign().  If an extrapolation operator (as opposed to a
proper widening operator) is OK for you, there is also
BGP99_extrapolation_assign().

Notice though that widening powersets of polyhedra is a rather advanced
topic: you really have to read the library documentation.
Cheers,

Roberto

--
Prof. Roberto Bagnara
Applied Formal Methods Laboratory
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~__bagnara/ <http://www.cs.unipr.it/%7Ebagnara/>
mailto:bagnara at cs.unipr.it <mailto:bagnara at cs.unipr.it>
_________________________________________________
PPL-devel mailing list
PPL-devel at cs.unipr.it <mailto:PPL-devel at cs.unipr.it>
http://www.cs.unipr.it/__mailman/listinfo/ppl-devel <http://www.cs.unipr.it/mailman/listinfo/ppl-devel>

--
Regards,
Gokul Ramaswamy,
Department of CSE, IIT Bombay
+919757417460
http://www.cse.iitb.ac.in/~ramaswamy <http://www.cse.iitb.ac.in/%7Eramaswamy>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: getWidenPoly_PPL.cpp
Type: text/x-c++src
Size: 961 bytes
Desc: not available
URL: <http://www.cs.unipr.it/pipermail/ppl-devel/attachments/20110619/c5b6dbfe/attachment.cpp>
```