-
Notifications
You must be signed in to change notification settings - Fork 1
Convert LTL formulas into finite-state automata for monitoring
License
nondeterministic/ltl3tools
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
LTL3 tools README -=-=-=-=-=-=-=-=- What you need to properly use the LTL3 tools: --------------------------------------------- Download: 1. AT&T's fsmlibrary version 4.0. It used to be widely available under a free-to-use license for noncommercial purposes, but now seems to be available only upon request. Perhaps, these folks can help: https://github.com/att Otherwise use a web search, as many universities still use the library in their courses and offer binaries to download. 2. LTL2BA: http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ (tested with version 1.1 of the translator) 3. Optional: AT&T's Graphviz, which includes the programs dot, dotty, etc. Note that most modern Linux systems have these preinstalled. Then simply copy the binaries of 1. and 2. into the third-party/ directory of the LTL3 tools distribution. (2. may have to be compiled first.) How to run ltl2mon / the LTL3 tools: ------------------------------------ 1. Change into the directory where you extracted the package 2. Optional: Check the settings inside ltl2mon (ltl2mon is the main entry point to the LTL3 tools) 3. Run, for example, "./ltl2mon "(! a) U b" | dot -Tps > graph.ps" How to compile the LTL3 tools: ------------------------------ If you are on i686 GNU/Linux, you do not have to compile the LTL3 tools as there are some statically linked binaries in the bin/ directory. Otherwise, follow these steps to compile the LTL3 tools: 1. Change into the directory where you extracted the package 2. Run "make install" Notice, ltl2mon is written in Ocaml. So, you will need an Ocaml tool chain. For further information read the files AUTHORS and COPYING, or visit http://ltl3tools.sf.net/.
About
Convert LTL formulas into finite-state automata for monitoring
Topics
Resources
License
Stars
Watchers
Forks
Packages 0
No packages published