[PPL-devel] Re: The Action Language Verifier and the Parma Polyhedra Library

[kmixter at longshot.com]

Hi Roberto,

This is a strange case.  First, I should mention that even if this
exception were not thrown, I don't expect ALV to be able to run to
completion on statechart.al because RealSym code (which uses PPL) does not
yet implement two necessary functions to support the synchronous
composition operator ('&').  This lack of functionality is more of an
oversight on my part than any kind of limitation, and should be fixed in
the near future.  However, the strange part is that I don't see an
exception thrown or abort when I run the verifier on this file.  Instead,
it executes all the way to the assert(false) in one of the
not-yet-implemented functions (RealSym::domainSet()).  Perhaps we have a
different statechart.al (though I downloaded it from the website) or the
compiler difference (I'm using 2.96) is somehow coming into play.

Thanks for taking the time to bring the C++ code up to date.  I've
submitted those into our repository so future users won't have to go
through the same process.

-Ken

On Tue, 7 Jan 2003, Roberto Bagnara wrote:

> 
> Dear Ken,
> 
> we have started studying your code in order to understand your needs
> and to improve the PPL.  To start with, we have modified parmiface.c
> so as to use the `Polyhedron::check_universe()' method (this results
> in cleaner code that is also more efficient).
> 
> kmixter at longshot.com wrote:
> > You may also want to download the latest version 0.2 for full
> > documentation and examples.
> 
> We did that, in order to have more examples to test with and we
> ran across a bug.  We have modifies ALV's main program so as to
> catch standard exceptions and print them.  With this modification,
> here is what happens:
> 
> $ ~/composite/composite/obj-linux/action -r statechart.al
> Module main
> Local variables
> main.Office.0 of type 1
> main.Occupants.0 of type 1
> main.Light.0 of type 1
> main.turn_off of type 1
> main.turn_on of type 1
> main.exit of type 1
> main.enter of type 1
> main.count of type 4
> Formal variables
> items size 4
> items size 4
> ****************
> domain variables
> type 0
> main.0.Office.0
> main.0.Occupants.0
> main.0.Light.0
> main.0.turn_off
> main.0.turn_on
> main.0.exit
> main.0.enter
> type 1
> main.0.count
> Exception caught:
> PPL::NNC_Polyhedron::inters_assign_and_min(y):
> this->space_dimension() == 2, y->space_dimension() == 1.
> Capacity : 10003
> Total references : 0
> Hits             : 0 ( nan %)
> Misses           : 0 ( nan %)
> Collisions        : 0 ( nan %)
>   Stats
> 
> The important bit is
> 
> Exception caught:
> PPL::NNC_Polyhedron::inters_assign_and_min(y):
> this->space_dimension() == 2, y->space_dimension() == 1.
> 
> This says that NNC_Polyhedron::intersection_assign_and_minimize()
> has been called over two polyhedra of different dimensions.
> The only call to this method is in parmiface.c in the function
> Polyhedron *DomainIntersection(Polyhedron *d1, Polyhedron *d2, int).
> Do you know what might go wrong?
> 
> Meanwhile, please find attached the patch file for the changes
> mentioned above (without the change to `main()' you would see
> an abort instead of the description of the caught exception).
> Notice that this patch assumes you have already applied the
> path we sent you a few days ago.
> All the best
> 
>      Roberto
> 
> -- 
> Prof. Roberto Bagnara
> Computer Science Group
> Department of Mathematics, University of Parma, Italy
> http://www.cs.unipr.it/~bagnara/
> mailto:bagnara at cs.unipr.it
>