alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* NEWS: Summarize recent changes.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2012-08-22 15:16:46 +02:00
parent 8cb68d76b5
commit dce79ffed5
1 changed files with 31 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

32
NEWS
View file

@ -1,6 +1,36 @@
New in spot 0.9.2a: New in spot 0.9.2a:
Nothing yet. * Support for various flavors of Testing Automata.
The flavors are:
- "classical" Testing Automata, as used for instance by
Geldenhuys and Hansen (Spin'06), using Büchi and
livelock acceptance conditions.
- Generalized Testing Automata, extending the previous
with multiple Büchi acceptance sets.
- Transition-based Generalized Testing Automata moving Büchi
acceptance to transitions, and getting rid of livelock
acceptance conditions by expliciting stuttering self-loops.
Supporting algorithms include anything required to run
the automata-theoretic approach using testing automata:
- dedicated synchronized product
- dedicated emptiness-check for TA and GTA, as these
may require two passes because of the two kinds of
acceptance, while a TGTA can be checked for emptiness
with the same one-pass algorithm as a TGBA.
- conversion from a TGBA to any of the above kind, with
options to reduce these automata with bisimulation,
and to produce a BA/GBA that require a single pass
(at the expense of determinism).
- 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.
* TGBA can now be reduced by Reverse Simulation (in addition to
the Direct Simulation introduced in 0.9). A function called
iterated_simulations() will alternate direct and reverse
simulations in a loop as long as it diminishes the size of the
automaton.
New in spot 0.9.2 (2012-07-02): New in spot 0.9.2 (2012-07-02):