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
LTL Model-checking in ASAP
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