Commit 35fc975d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* NEWS: mention ltlcheck

parent f03ba4b5
......@@ -12,21 +12,30 @@ New in spot 0.9.2a:
interfaces: they have now been rewritten with better argument
parsing, saner defaults, and they come with man pages.
- genltl: generate LTL formulas from scallable patterns
This offers 20 patterns so far.
- randltl: generate random LTL/PSL formulas
- ltlfilt: filter lists of formulas according to several criteria
(e.g., match only safety formulas that are larger than
some given size). Besides being used as a "grep" tool
for formulas, this can also be used to convert
files of formulas between different syntaxes, apply
some simplifications, check whether to formulas are
equivalent, ...
- ltl2tgba translate LTL/PSL formulas into Büchi automata. A
fondamental change to the interface is that you may
now specify the goal of the translation: do you
you favor deterministic or smaller automata?
- ltl2tgta translate LTL/PSL formulas into Testing Automata.
- genltl: Generate LTL formulas from scallable patterns.
This offers 20 patterns so far.
- randltl: Generate random LTL/PSL formulas.
- ltlfilt: Filter lists of formulas according to several criteria
(e.g., match only safety formulas that are larger than
some given size). Besides being used as a "grep" tool
for formulas, this can also be used to convert
files of formulas between different syntaxes, apply
some simplifications, check whether to formulas are
equivalent, ...
- ltl2tgba: Translate LTL/PSL formulas into Büchi automata. A
fondamental change to the interface is that you may
now specify the goal of the translation: do you
you favor deterministic or smaller automata?
- ltl2tgta: Translate LTL/PSL formulas into Testing Automata.
- ltlcheck: A tool to find bugs in translators from LTL/PSL to
Büchi automata. This is essentially a Spot-based
reimplementation of LBTT that supports PSL in addition
to LTL, and that can output more statistics.
These binaries are built in the src/bin/ directory. The former
test versions of genltl and randltl have been removed from the
......@@ -62,9 +71,9 @@ New in spot 0.9.2a:
+ output in dot format for display
A discussion of these automata, part of Ala Eddine BEN SALEM's
PhD work, should appear in a future edition of ToPNoC.
The web-based interface can build and display these testing
automata.
PhD work, should appear in ToPNoC VI (LNCS 7400). The web-based
interface and the aformentioned ltl2tgta tool, can be used
to build testing automata.
- TGBA can now be reduced by Reverse Simulation (in addition to
the Direct Simulation introduced in 0.9). A function called
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment