-------- Original Message -------- Subject: Re: [PPL-devel] Widening operation in Powerset Date: Mon, 20 Jun 2011 00:52:47 +0530 From: Gokul Ramaswamy gokulhcramaswamy@gmail.com To: Roberto Bagnara bagnara@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@cs.unipr.it mailto:bagnara@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@cs.unipr.it mailto:bagnara@cs.unipr.it _________________________________________________ PPL-devel mailing list PPL-devel@cs.unipr.it mailto:PPL-devel@cs.unipr.it http://www.cs.unipr.it/__mailman/listinfo/ppl-devel http://www.cs.unipr.it/mailman/listinfo/ppl-devel