This post has 257 words. Reading it will take approximately 1 minute.
I just finished integrating LTL model-checking into ASAP. This is joint work with Sami Evangelista and Thomas Vestergaard. Basically, I’ve made the translation from LTL to a Büchi automaton, Sami made the nested depth-first checker, and Thomas put it together, added a bunch of utility functions, and made the initial integration into ASAP. After that I cleaned up the integration a bit and added a nifty user-interface for entering LTL formulae.
With no further ado, check out the video below. If it’s loading too slowly (or my flash-video thingy is still borked), try using the Youtube versions below (despite being unlovingly chopped over and in crappy quality).
Get the Flash Player to see this content.
Hi Michael,
could you please tell me when and where your LTL-model checking plugin will be available (if…).
Many thanks,
Davide
Hi Davide,
I have checked in the source in our repository (see more at here and here). You may or may not need a password to check out the code; I don’t remember.
If you are interested, I can also look at building a new release of ASAP with the checker (as well as a bunch of optimizations I made subsequently) later this week. You can get releases here, but the latest release is quite old and contains no LTL checker code.
Regards,
Michael
Hi Michael,
thanks for your answer! I’ve checked in your repository and I’ve been asked for a user/pwd input.
I am surely interested in a new release (for your info, I’m a Mac user) with checker, it’s very kind of you.
Best regards,
Davide
Hi Michael,
I hope everything it’s ok now!
I’m writing to ask you if you’ve had time to prepare the ASAP release with the LTL checker.
Thank in advance.
Best regards,
Davide
Sorry for not getting back to you – things have been a bit hectic the last couple months. The most recent version of ASAP from http://www.cs.au.dk/~ascoveco/download.html does indeed have LTL built in.
Thanks a lot, Michael!
I knew what happened at your home…Surely you have had a lot of more important things to do than getting back to me about ASAP !!!
Good luck and many thanks,
Davide