The Action Language Verifier and the Parma Polyhedra Library

7 Jan 2003

      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@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@cs.unipr.it

diff -rcp2 composite.1/parser/main.c composite/parser/main.c
*** composite.1/parser/main.c	Tue Jan  7 15:38:48 2003
--- composite/parser/main.c	Tue Jan  7 16:39:37 2003
***************
*** 6,9 ****
--- 6,10 ----
  #include <stdlib.h>
  #include <iostream.h>
+ #include <stdexcept>
  #include <bool.h>

*************** temporal operator \n\
*** 99,103 ****

  char *startHeap;
! int main(int argc,char **argv) {

    char *fileName;
--- 100,104 ----

  char *startHeap;
! int main(int argc,char **argv) try {

    char *fileName;
*************** int main(int argc,char **argv) {
*** 338,346 ****

  }
! 
! 
! 
! 
! 
! 
! 
--- 339,345 ----

  }
! catch (const exception& e) {
!   cerr << "Exception caught:\n"
!        << e.what()
!        << endl;
! }
diff -rcp2 composite.1/util/parmiface.c composite/util/parmiface.c
*** composite.1/util/parmiface.c	Tue Jan  7 15:38:48 2003
--- composite/util/parmiface.c	Tue Jan  7 15:43:17 2003
*************** int DomainIsEmpty(Polyhedron *p)
*** 144,149 ****
  int PolyhedronIsUniverse(Polyhedron *p)
  {
!   const PPL::ConSys *cs = &p->_data->constraints();
!   return cs->begin() == cs->end();
  }

--- 144,148 ----
  int PolyhedronIsUniverse(Polyhedron *p)
  {
!   return p->_data->check_universe();
  }

*************** Polyhedron *DomainDifference(Polyhedron 
*** 307,315 ****

    for (p2 = d2; p2 != NULL; p2 = p2->next) {
-     const PPL::ConSys *cs = &p2->_data->constraints();
-     PPL::ConSys::const_iterator i = cs->begin();
      Polyhedron *result = NULL;

!     if (cs->begin() == cs->end()) {
        /* Universe polyhedrons have no constraints, so they need to
           be special-cased, meaning this should result in empty polyhedron. */
--- 306,312 ----

    for (p2 = d2; p2 != NULL; p2 = p2->next) {
      Polyhedron *result = NULL;

!     if (p2->_data->check_universe()) {
        /* Universe polyhedrons have no constraints, so they need to
           be special-cased, meaning this should result in empty polyhedron. */
*************** Polyhedron *DomainDifference(Polyhedron 
*** 317,320 ****
--- 314,320 ----
      }

+     const PPL::ConSys *cs = &p2->_data->constraints();
+     PPL::ConSys::const_iterator i;
+ 
      for (p1 = remainder; p1 != NULL; p1 = p1->next) {
        for (i = cs->begin(); i != cs->end(); ++i) {

Roberto Bagnara

kmixter＠longshot.com

tags (0)

participants (2)