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

[Roberto Bagnara]

-------- 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,
Graduate Student,
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>