math/ltl2ba 1.3 DragonFly
Fast translation from LTL formulae to Buchi automata
- System
- DragonFly
- Repository
- DPorts
- Maintainer
- [email protected] (as in FreeBSD)
- License
- GPLv2
- Categories
- math
- Package size
- 29.7 KiB, 72.7 KiB installed
Description
ltl2ba implements an algorithm of P. Gastin and D. Oddoux to generate Buchi automata from linear temporal logic (LTL) formulae. This algorithm generates a very weak alternating automaton and then transforms it into a Buchi automaton, using a generalized Buchi automaton as an intermediate step. Each automaton is simplified on-the-fly in order to save memory and time. As usual the LTL formula is simplified before any treatment. ltl2ba is more efficient than Spin 3.4.1, with regard to the size of the resulting automaton, the time of the computation, and the memory used.
In the other systems
| System | Port | Version |
|---|---|---|
| DragonFly | math/ltl2ba | 1.3 |
| FreeBSD | math/ltl2ba | 1.3 |
| NetBSD | wip/ltl2ba | 1.3 |
| HardenedBSD | math/ltl2ba | 1.3 |
| GhostBSD | math/ltl2ba | 1.3 |
Install
Binary package:
pkg install ltl2ba
From DPorts:
cd /usr/dports/math/ltl2ba && make install clean
Dependencies
No port depends on this one.