From dce79ffed5173d6b31c7a494a957bb166cc4bc86 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 22 Aug 2012 15:16:46 +0200 Subject: [PATCH] * NEWS: Summarize recent changes. --- NEWS | 32 +++++++++++++++++++++++++++++++- 1 file changed, 31 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index bc85c63f2..edb69c29e 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,36 @@ 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):