The FTS Haskell library implements algorithms for LTL model checking of FTS which are presented in the ICSE’10 paper. For LTL to Büchi conversion, the library uses ltl2ba, by Denis Oddoux and Paul Gastin which is licensed under GPL.
Unzip the archive. The library is the fts.hs file. The library documentation, generated by Haddock is in the haddock folder. You might want to consult the example models which are in the examples folder. More information on these examples can be found in the technical report.
- You need PHP because the ltl2hs script is written in PHP.
- You need to compile ltl2ba (sources are included in the archive) and put the executable into the FTS folder.
1. Create a file, main.hs with the following content:
module Main (main) where import FTS
2. Add your models to the file
myModel :: FTS myModel = FTS (....)
Alternatively: take an example from the examples folder.
3. Use as command line tool with Hugs.
- Install Hugs.
- Type hugs main.hs
- Hugs will load, make sure there were no errors.
- Now you’re all set for exploring your models.
For instance type checkLTL myModel "some ltl property" into the Hugs prompt.
4. Use as batch processing tool with GHC.
- Follow the steps from the previous point.
- Add a line with the action you want to perform in batch mode: e.g.
main = checkLTL myModel "some ltl property"
- Install GHC.
- Type ghc --make main.hs
- GHC will compile, make sure the compilation succeeded.
- Execute using ./main