Tevfik Bultan wrote:
This was an extension to Action Language Verifier (ALV) that was done as a class project. We did not integrate it to the later versions of ALV. The current version of ALV that is available at: http://www.cs.ucsb.edu/~bultan/composite/ uses two different representations for integer variables: 1) polyhedra representation as implemented in Omega library and 2) automata representation built on top off the MONA automata package. Both representations can handle the full Presburger arithmetic.
I think it should be possible to modify Ken's interface to the newer version of the ALV.
Thanks Tevfik. I have put the archive Ken sent me on 2003 in
ftp://ftp.cs.unipr.it/pub/ppl/applications/composite-parma-alpha.tgz
David, if you want to try to modify Ken's interface to the newer versions of PPL and the ALV you can count on the PPL developers' for assistance, provided you are willing to let us have the final modified version. All the best,
Roberto