[PPL-devel] Question about ALV & PPL

Tevfik Bultan bultan at cs.ucsb.edu
Fri Mar 28 03:34:25 CET 2008


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.

Best,
-- 
Tevfik

Tevfik Bultan

Associate Professor, Vice Chair
Department of Computer Science
University of California, Santa Barbara
http://www.cs.ucsb.edu/~bultan/

On Tue, 25 Mar 2008, Roberto Bagnara wrote:

> David Rodriguez Velazquez wrote:
>> I have a question. I want to use ALV and PPL  instead of Omega.
>> Do you have any tip how can I start to work on it? Do you have any advice?
>
> Dear David,
>
> I assume by ALV you mean the Action Language Verifier
> (http://www.cs.ucsb.edu/~bultan/composite/index.html).
>
> Back in 2003 Ken Mixter, under the direction of Tevfik Bultan
> (both in CC), produced a version of ALV that is based on
> the PPL.  That version was never released to the public,
> but I have a copy (I don't know if it is up-to-date).
> The problem is that this was based on ALV 0.2 and PPL 0.4.2
> whereas the current version of ALV is 0.4 and the current
> version of PPL is 0.9: I don't know if the PPL interface
> developed by Ken is compatible with these new versions.
> For the PPL side there is no problem at all: we can make the
> required changes in a matter of minutes.  I don't know
> if the changes between ALV 0.2 to ALV 0.4 are more difficult
> to accommodate.
>
> Let us see if Ken and or Tevfik have something
> more up-to-date or some suggestion to offer.
> All the best,
>
>    Roberto
>
>



More information about the PPL-devel mailing list