-------- Original Message -------- Subject: Re: Asking help using PPL's C interface Date: Fri, 30 Jan 2004 13:40:52 -0500 From: Hosung Song hosungs@umich.edu To: Roberto Bagnara bagnara@cs.unipr.it References: 4019F848.2010809@umich.edu 4019FF57.8070707@cs.unipr.it

Thank you very much for your prompt and kind reply. Shame on me. I knew the existence of the directory, but I just glanced it and I didn't thought it was a C interface example. Yeah, I didn't look into it so far. I just tried that and compilation alone was not easy. After couple of 'gcc lpenum.c', I found I needed GLPK library. Downloaded and installed. Still 'make' or 'make all' or 'make lpenum' didn't work, so I tried 'gcc -o lpenum lpenum.c -l...' and finally it took me to figure out that I need about 5 -l flags like 'gcc -o lpenum lpenum.c -lglpk -lppl_c -lppl -lgmpxx -lgmp'. It compiled and linked well, and I got the same result as in 'expected'. I hope the compilation was easy and GLPK's necessity was stated. Maybe they are all done in some place, and I may be just lazy and impatient... It looks like using the C interface is a little tedious than using the C++ interface. I wish I could use C++ library directly from my C program. I'll look into the lpenum example for a while. Thanks again.

Regarding desired features, I'm wondering if you have any plan to support machine integer types as coefficients. I'm just guessing that using GMP can be quite time consuming. Of course, that can give us the ability to describe arbitrarily large polyhedra, but I suppose it can be also desirable to have faster library even with some restrictions. I checked out three libraries (PPL, new Polka, and IRISA one), and it seemed PPL is the only one supporting dimension addition/deletion, and best documented/packaged. The support of flexible dimensions is very important to me because the model checker I'm working on should be able to instantiate new analog variables as hybrid processes are instantiated in the middle of system executions. The necessity of a polyhedron library for my case is that we need to store values of analog variables with polyhedra, which are time-abstracted representation of sets of points in n-dimensional space R^n. Mostly I will just need intersections, time-elapse, and equality check operations. Thanks again and let me email you if I come up with desired features or improvements.

Best wishes,

Hosung

Roberto Bagnara wrote:

Hosung Song wrote:

...

Professor Bagnara,

Greetings. I've got some help request on PPL usage. I'm sorry if I should have sent this email to someone else, but I didn't think the developer mailing list was appropriate, and there's no contact information in the PPL website (other than mailing lists). I'm currently working on extending a software model checker (Spin) to hybrid settings. This requires extensive polyhedra manipulations and naturally I was led to your PPL package. First of all, I'd like to thank you for your thorough work on the library. Unfortunately, Spin is written in C language and I myself am not a good C++ programmer, so I think I have to use C language interface of PPL. While C++ usage seems quite intuitive (I could see from the examples in the tests directory), there's no example using C interface, and the documentation about it seems quite terse. I'm wondering if you could provide some very simple example of C interface usage (e.g. C interface version of one example in the tests directory). I guess we can manipulate constraints, polyhedra and so on, but I don't know how to deal with variables. Are variables just indexed as integers as ppl_dimension_type? Anyway, a brief example would be greatly helpful. Thanks again for your wonderful package, and I look forward to your little help.

Best wishes,

Hosung Song

Dear Hosung,

the developer's mailing list is indeed the appropriate place if you want to get in touch with the PPL's developers. On their behalf, let me thank you for your nice words.

Coming to the C interface, what you write makes me suspect you did not look into the `interfaces/C/lpenum/' directory. It contains a toy LP solver written in C and using the PPL's C interface. There you can find examples of how to use several functions provided by that interface.

You guess right: a variable is represented by its index, and such indices are of type `ppl_dimension_type'. For example,

ppl_LinExpression_add_to_coefficient(le, i, k);

adds `k*x' to the linear expression represented by `le', where x is the variable corresponding to dimension `i'.

Your message indicates a number of things we can do to improve the PPL's web site and documentation. Thank you very much for your feedback and, please, do not hesitate to come back to us. All the best,

Roberto

P.S. A number of quite exciting new features are in preparation for the future releases of the PPL. These include support for more precise domains and for restricted classes of polyhedra for which very efficient algorithms are available. If you would like to tell us more about the application you are developing and how our library could make your life easier, please do so: this may help us to better direct our development efforts.