- Spot-announce

Spot 2.5 released
by Alexandre Duret-Lutz 20 Jan '18

20 Jan '18

We are happy to announce the release of Spot 2.5. Spot is a library of algorithms for manipulating LTL formulas and omega-automata (objects as commonly used in model checking). A detailed list of new features in this new release is given at the end of this email. The main features of this release are algorithms for working with parity acceptance, new functions to convert to co-Büchi when possible, a new tool for LTL synthesis, and some speedup of our determinization algorithm. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.5.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. (Note that due to some technical issues on our side, it might be a few days before the packages for Debian *unstable* are updated.) This release contains code contributed by Alexandre Gbaguidi Aïsse, Thibaud Michaud, Laurent Xu, Maximilien Colange, Etienne Renault, and myself. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.5 (2018-01-20) Build: - We no longer distribute the doxygen-generated documentation in the tarball of Spot to save space. This documentation is still available online at https://spot.lrde.epita.fr/doxygen/. If you want to build a local copy you can configure Spot with --enable-doxygen, or simply run "cd doc && make doc". - All the images that illustrate the documentation have been converted to SVG, to save space and improve quality. Tools: - ltlsynt is a new tool for synthesizing a controller from LTL/PSL specifications. - ltlcross learned --reference=COMMANDFMT to specify a translator that should be trusted. Doing so makes it possible to reduce the number of tests to be performed, as all other translators will be compared to the reference's output when available. Multiple reference can be given; in that case other tools are compared against the smallest reference automaton. - autcross, ltlcross, and ltldo learned --fail-on-timeout. - ltl2tgba, autfilt, and dstar2tgba have some new '--parity' and '--colored-parity' options to force parity acceptance on the output. Different styles can be requested using for instance --parity='min odd' or --parity='max even'. - ltl2tgba, autfilt, and dstar2tgba have some new '--cobuchi' option to force co-Büchi acceptance on the output. Beware: if the input language is not co-Büchi realizable the output automaton will recognize a superset of the input. Currently, the output is always state-based. - genltl learned to generate six new families of formulas, taken from the SYNTCOMP competition on reactive synthesis, and from from Müller & Sickert's GandALF'17 paper: --gf-equiv=RANGE (GFa1 & GFa2 & ... & GFan) <-> GFz --gf-implies=RANGE (GFa1 & GFa2 & ... & GFan) -> GFz --ms-example=RANGE GF(a1&X(a2&X(a3&...)))&F(b1&F(b2&F(b3&...))) --ms-phi-h=RANGE FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb)|... --ms-phi-r=RANGE (FGa{n}&GFb{n})|((FGa{n-1}|GFb{n-1})&(...)) --ms-phi-s=RANGE (FGa{n}|GFb{n})&((FGa{n-1}&GFb{n-1})|(...)) - autfilt learned --streett-like to convert automata with DNF acceptance into automata with Streett-like acceptance. - autfilt learned --acceptance-is=ACC to filter automata by acceptance condition. ACC can be the name of some acceptance class (e.g. Büchi, Fin-less, Streett-like) or a precise acceptance formula in the HOA syntax. - ltldo learned to limit the number of automata it outputs using -n. - ltlfilt learned to measure wall-time using --format=%r, and cpu-time with --format=%R. - The --format=%g option of tools that output automata used to print the acceptance condition as a *formula* in the HOA format. This %g may now take optional arguments to print the acceptance *name* in different formats. For instance ... | autfilt -o '%[s]g.hoa' will separate a stream of automata into different files named by their acceptance name (Buchi, co-Buchi, Streett, etc.) or "other" if no name is known for the acceptance condition. - Tools that produce formulas now support --format=%[OP]n to display the nesting depth of operator OP. - The new -x tls-impl=N option allows to fine-tune the implication-based simplification rules of ltl2tgba. See the spot-x(7) man page for details. - All tools learned to check the SPOT_OOM_ABORT environment variable. This is only useful for debuging out-of-memory conditions. See the spot-x(7) man page for details. New functions in the library: - spot::iar() and spot::iar_maybe() use index appearance records (IAR) to translate Rabin-like automata into equivalent parity automaton. This translation preserves determinism and is especially useful when the input automaton is deterministic. - spot::print_aiger() encodes an automaton as an AIGER circuit, as required by the SYNTCOMP competition. It relies on a new named property "synthesis outputs" that describes which atomic propositions are to be encoded as outputs of the circuits. - spot::dnf_to_streett() converts any automaton with a DNF acceptance condition into a Streett-like automaton. - spot::nsa_to_nca(), spot::dfn_to_nca(), spot::dfn_to_dca(), and spot::nsa_to_dca(), convert automata with DNF or Streett-like acceptance into deterministic or non-deterministic co-Büchi automata. spot::to_dca() and spot::to_nca() dispatch between these four functions. The language of produced automaton includes the original language, but may be larger if the original automaton is not co-Büchi realizable. Based on Boker & Kupferman FOSSACS'11 paper. Currently only supports state-based output. - spot::scc_info::states_on_acc_cycle_of() returns all states visited by any accepting cycle of the specified SCC. It only works on automata with Streett-like acceptance. - spot::is_recurrence(), spot::is_persistence(), and spot::is_obligation() test if a formula is a recurrence, persistance or obligation. The SPOT_PR_CHECK and SPOT_O_CHECK environment variables can be used to select between multiple implementations of these functions (see the spot-x(7) man page). - spot::is_colored() checks if an automaton is colored (i.e., every transition belongs to exactly one acceptance set). - spot::change_parity() converts between different parity acceptance conditions. - spot::colorize_parity() transforms an automaton with parity acceptance into a colored automaton (which is often what people working with parity automata expect). - spot::cleanup_parity_acceptance() simplifies a parity acceptance condition. - spot::parity_product() and spot::parity_product_or() are specialized (but expensive) products that preserve parity acceptance. - spot::remove_univ_otf() removes universal transitions on the fly from an alternating Büchi automaton using Miyano and Hayashi's breakpoint algorithm. - spot::stutter_invariant_states(), spot::stutter_invariant_letters(), spot::highlight_stutter_invariant_states(), ... These functions help study a stutter-sensitive automaton and detect the subset of states that are stutter-invariant. See https://spot.lrde.epita.fr/ipynb/stutter-inv.html for examples. - spot::acc_cond::name(fmt) is a new method that names well-known acceptance conditions. The fmt parameter specifies the format to use for that name (e.g. to the style used in HOA, or that used by print_dot()). - spot::formula::is_leaf() method can be used to detect formulas without children (atomic propositions, or constants). - spot::nesting_depth() computes the nesting depth of any LTL operator. - spot::check_determinism() sets both prop_semi_deterministic() and prop_universal() appropriately. Improvements to existing functions in the library: - spot::tgba_determinize() has been heavily rewritten and optimized. The algorithm has (almost) not changed, but it is much faster now. It also features an optimization for stutter-invariant automata that may produce slightly smaller automata. - spot::scc_info now takes an optional argument to disable some features that are expensive and not always necessary. By default scc_info tracks the list of all states that belong to an SCC (you may now ask it not to), tracks the successor SCCs of each SCC (that can but turned off), and explores all SCCs of the automaton (you may request to stop on the first SCC that is found accepting). - In some cases, spot::degeneralize() would output Büchi automata with more SCCs than its input. This was hard to notice, because very often simulation-based simplifications remove those extra SCCs. This situation is now detected by spot::degeneralized() and fixed before returning the automaton. A new optional argument can be passed to disable this behavior (or use -x degen-remscc=0 from the command-line). - The functions for detecting stutter-invariant formulas or automata have been overhauled. Their interface changed slightly. They are now fully documented. - spot::postprocessor::set_type() can now request different forms of parity acceptance as output. However currently the conversions are not very smart: if the input does not already have parity acceptance, it will simply be degeneralized or determinized. - spot::postprocessor::set_type() can now request co-Büchi acceptance as output. This calls the aforementioned to_nca() or to_dca() functions. - spot::remove_fin() will now call simplify_acceptance(), introduced in 2.4, before attempting its different Fin-removal strategies. - spot::simplify_acceptance() was already merging identical acceptance sets, and detecting complementary sets i and j to perform the following simplifications Fin(i) & Inf(j) = Fin(i) Fin(i) | Inf(j) = Inf(i) It now additionally applies the following rules (again assuming i and j are complementary): Fin(i) & Fin(j) = f Inf(i) | Inf(j) = t Fin(i) & Inf(i) = f Fin(i) | Inf(i) = t - spot::formula::map(fun) and spot::formula::traverse(fun) will accept additionnal arguments and pass them to fun(). See https://spot.lrde.epita.fr/tut03.html for some examples. Python-specific changes: - The "product-states" property of automata is now accessible via spot.twa.get_product_states() and spot.twa.set_product_states(). - twa_word instances can be displayed as SVG pictures, with one signal per atomic proposition. For some examples, see the use of the show() method in https://spot.lrde.epita.fr/ipynb/word.html - The test suite is now using v4 of the Jupyter Notebook format. - The function rabin_is_buchi_realizable() as its name suggests checks if a rabin aut. is Büchi realizable. It is heavily based on tra_to_tba() algorithm. Deprecation notices: (These functions still work but compilers emit warnings.) - spot::scc_info::used_acc(), spot::scc_info::used_acc_of() and spot::scc_info::acc() are deprecated. They have been renamed spot::scc_info::marks(), spot::scc_info::marks_of() and spot::scc_info::acc_sets_of() respectively for clarity. Backward incompatible changes: - The spot::closure(), spot::sl2(), spot::is_stutter_invariant() functions no longer take && arguments. The former two have spot::closure_inplace() and spot::sl2_inplace() variants. These functions also do not take a list of atomic propositions as an argument anymore. - The spot::bmrand() and spot::prand() functions have been removed. They were not used at all in Spot, and it is not Spot's objective to provide such random functions. - The spot::bdd_dict::register_all_propositions_of() function has been removed. This low-level function was not used anywhere in Spot anymore, since it's better to use spot::twa::copy_ap_of(). Bugs fixed: - spot::simplify_acceptance() could produce incorrect output if the first edge of the automaton was the only one with no acceptance set. In spot 2.4.x this function was only used by autfilt --simplify-acceptance; in 2.5 it is now used in remove_fin(). - spot::streett_to_generalized_buchi() could generate incorrect automata with empty language if some Fin set did not intersect all accepting SCCs (in other words, the fix from 2.4.1 was incorrect). - ltlcross could crash when calling remove_fin() on an automaton with 32 acceptance sets that would need an additional set. - the down_cast() helper function used in severaly headers of Spot was not in the spot namespace, and caused issues with some configurations of GCC. -- Alexandre Duret-Lutz

1 0

Spot 2.4.4 is released
by Alexandre Duret-Lutz 25 Dec '17

25 Dec '17

We are happy to announce the release of Spot 2.4.4 This is a maintenance release containing fixes for two serious bugs reported by František Blahoudek. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.4.4.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. New in spot 2.4.4 (2017-12-25) Bugs fixed: - The generic to_generalized_buchi() function would fail if the Fin-less & CNF version of the acceptance condition had several unit clauses. - If the automaton passed to sbacc() was incomplete or non-deterministic because of some unreachable states, then it was possible that the output would marked similarly while it was in fact complete or deterministic. Merry Christmas, -- Alexandre Duret-Lutz

1 0

Spot 2.4.3 released
by Alexandre Duret-Lutz 19 Dec '17

19 Dec '17

We are happy to announce the release of Spot 2.4.3 This is a maintenance release containing only minor bug fixes and documentation changes. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.4.3.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. New in spot 2.4.3 (2017-12-19) Bugs fixed: - couvreur99_new() leaked memory when processing TωA that allocate states. - Some mismatched placement-new/delete reported by ASAN were fixed. - Static compilation was broken on MinGW. - Execution of Jupyter notebooks from the testsuite failed with recent versions of Python. - Fix some warnings triggered by the development version of g++. -- Alexandre Duret-Lutz

1 0

Spot 2.4.2 released
by Alexandre Duret-Lutz 07 Nov '17

07 Nov '17

We are happy to announce the release of Spot 2.4.2 This is a maintenance release containing only minor bug fixes and documentation changes. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.4.2.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. New in spot 2.4.2 (2017-11-07) Tools: - ltlcross and ltldo support ltl3tela, the new name of ltl3hoa. Bugs fixed: - Automata produced by "genaut --ks-nca=N" were incorrectly marked as not complete. - Fix some cases for which the highest setting of formulas simplification would produce worse results than lower settings. -- Alexandre Duret-Lutz

1 0

Spot 2.4.1 released
by Alexandre Duret-Lutz 06 Oct '17

06 Oct '17

We are happy to announce the release of Spot 2.4.1 This is a maintenance release containing only bug fixes. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.4.1.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. This release contains patches contributed by Maximilien Colange, Florian Perlié-Long, Alexandre Gbaguidi Aïsse, and myself. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.4.1 (2017-10-05) Bugs fixed: - The formula class failed to build {a->c[*]} although it is allowed by our grammar. - spot::scc_info::determine_unknown_acceptance() incorrectly considered some rejecting SCC as accepting. - spot::streett_to_generalized_buchi() could generate automata with empty language if some Fin set did not intersect all accepting SCCs. As a consequence, some Streett-like automata were considered empty even though they were not. Also, the same function could crash on input that had a Streett-like acceptance not using all declared sets. - The twa_graph::merge_edges() function relied on BDD IDs to sort edges. This in turn caused some algorithms (like the degeneralization) to produce slighltly different (but still correct) outputs depending on the BDD operations performed before. - spot::simulation() could incorrectly flag an automaton as non-deterministic. -- Alexandre Duret-Lutz

1 0

Spot 2.4 released
by Alexandre Duret-Lutz 06 Sep '17

06 Sep '17

We are happy to announce the release of Spot 2.4. Spot is a library of algorithms for manipulating LTL formulas and omega-automata (objects as commonly used in model checking). A detailed list of new features in this new release is given at the end of this email. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.4.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. This release contains code contributed by Clément Gillard, Etienne Renault, Henrich Lauko, Maximilien Colange, Thomas Medioni and myself. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.4 (2017-09-06) Build: - Spot is now built in C++14 mode, so you need at least GCC 5 or clang 3.4. The current version of all major linux distributions ship with at least GCC 6, which defaults to C++14, so this should not be a problem. In *this* release of Spot, most of the header files are still C++11 compatible, so you should be able to include Spot in a C++11 project in case you do not yet want to upgrade. There is also an --enable-c++17 option to configure in case you want to force a build of Spot in C++17 mode. Tools: - genaut is a new binary that produces families of automata defined in the literature (in the same way as we have genltl for LTL formulas). - autcross is a new binary that compares the output of tools transforming automata (in the same way as we have ltlcross for LTL translators). - genltl learned two generate two new families of formulas: --fxg-or=RANGE F(p0 | XG(p1 | XG(p2 | ... XG(pn)))) --gxf-and=RANGE G(p0 & XF(p1 & XF(p2 & ... XF(pn)))) The later is a generalization of --eh-pattern=9, for which a single state TGBA always exists (but previous version of Spot would build larger automata). - autfilt learned to build the union (--sum) or the intersection (--sum-and) of two languages by putting two automata side-by-side and fiddling with the initial states. This complements the already implemented intersection (--product) and union (--product-or), both based on a product. - autfilt learned to complement any alternating automaton with option --dualize. (See spot::dualize() below.) - autfilt learned --split-edges to convert labels that are Boolean formulas into labels that are min-terms. (See spot::split_edges() below.) - autfilt learned --simplify-acceptance to simplify some acceptance conditions. (See spot::simplify_acceptance() below.) - autfilt --decompote-strength has been renamed to --decompose-scc because it can now extract the subautomaton leading to an SCC specified by number. (The old name is still kept as an alias.) - The --stats=%c option of tools producing automata can now be restricted to count complete SCCs, using %[c]c. - Tools producing automata have a --stats=... option, and tools producing formulas have a --format=... option. These two options work similarly, the use of different names is just historical. Starting with this release, all tools that recognize one of these two options also accept the other one as an alias. Library: - A new library, libspotgen, gathers all functions used to generate families of automata or LTL formulas, used by genltl and genaut. - spot::sum() and spot::sum_and() implements the union and the intersection of two automata by putting them side-by-side and using non-deterministim or universal branching on the initial state. - twa objects have a new property: prop_complete(). This obviously acts as a cache for the is_complete() function. - spot::dualize() complements any alternating automaton. Since the dual of a deterministic automaton is still deterministic, the function spot::dtwa_complement() has been deprecated and simply calls spot::dualize(). - spot::decompose_strength() was extended and renamed to spot::decompose_scc() as it can now also extract a subautomaton leading to a particular SCC. A demonstration of this feature via the Python bindings can be found at https://spot.lrde.epita.fr/ipynb/decompose.html - The print_dot() function will now display names for well known acceptance conditions under the formula when option 'a' is used. We plan to enable 'a' by default in a future release, so a new option 'A' has been added to hide the acceptance condition. - The print_dot() function has a new experimental option 'x' to output labels are LaTeX formulas. This is meant to be used in conjunction with the dot2tex tool. See https://spot.lrde.epita.fr/oaut.html#dot2tex - A new named property for automata called "original-states" can be used to record the origin of a state before transformation. It is currently defined by the degeneralization algorithms, and by transform_accessible() and algorithms based on it (like remove_ap::strip(), decompose_scc()). This is realy meant as an aid for writing algorithms that need this mapping, but it can also be used to debug these algorithms: the "original-states" information is displayed by the dot printer when the 'd' option is passed. For instance in % ltl2tgba 'GF(a <-> Fb)' --dot=s % ltl2tgba 'GF(a <-> Fb)' | autfilt -B --dot=ds the second command outputs an automaton with states that show references to the first one. - A new named property for automata called "degen-levels" keeps track of the level of a state in a degeneralization. This information complements the one carried in "original-states". - A new named property for automata called "simulated-states" can be used to record the origin of a state through simulation. The behavior is similar to "original-states" above. Determinization takes advantage of this in its pretty print. - The new function spot::acc_cond::is_streett_like() checks whether an acceptance condition is conjunction of disjunctive clauses containing at most one Inf and at most one Fin. It builds a vector of pairs to use if we want to assume the automaton has Streett acceptance. The dual function is spot::acc_cond::is_rabin_like() works similarly. - The degeneralize() function has learned to consider acceptance marks common to all edges comming to a state to select its initial level. A similar trick was already used in sbacc(), and saves a few states in some cases. - There is a new spot::split_edges() function that transforms edges (labeled by Boolean formulas over atomic propositions) into transitions (labeled by conjunctions where each atomic proposition appear either positive or negative). This can be used to preprocess automata before feeding them to algorithms or tools that expect transitions labeled by letters. - spot::scc_info has two new methods to easily iterate over the edges of an SCC: edges_of() and inner_edges_of(). - spot::scc_info can now be passed a filter function to ignore or cut some edges. - spot::scc_info now keeps track of acceptance sets that are common to all edges in an SCC. These can be retrieved using scc_info::common_sets_of(scc), and they are used by scc_info to classify some SCCs as rejecting more easily. - The new function acc_code::remove() removes all the given acceptance sets from the acceptance condition. - It is now possible to change an automaton acceptance condition directly by calling twa::set_acceptance(). - spot::cleanup_acceptance_here now takes an additional boolean parameter specifying whether to strip useless marks from the automaton. This parameter is defaulted to true, in order to keep this modification backward-compatible. - The new function spot::simplify_acceptance() is able to perform some simplifications on an acceptance condition, and might lead to the removal of some acceptance sets. - The function spot::streett_to_generalized_buchi() is now able to work on automata with Streett-like acceptance. - The function for converting deterministic Rabin automata to deterministic Büchi automata (when possible), internal to the remove_fin() procedure, has been updated to work with transition-based acceptance and with Rabin-like acceptance. - spot::relabel_here() was used on automata to rename atomic propositions, it can now replace atomic propositions by Boolean subformula. This makes it possible to use relabeling maps produced by relabel_bse() on formulas. - twa_graph::copy_state_names_from() can be used to copy the state names from another automaton, honoring "original-states" if present. - Building automata for LTL formula with a large number N of atomic propositions can be costly, because several loops and data-structures are exponential in N. However a formula like ((a & b & c) | (d & e & f)) U ((d & e & f) | (g & h & i)) can be translated more efficiently by first building an automaton for (p0 | p1) U (p1 | p2), and then substituting p0, p1, p2 by the appropriate Boolean formula. Such a trick is now attempted for translation of formulas with 4 atomic propositions or more (this threshold can be changed, see -x relabel-bool=N in the spot-x(7) man page). - The LTL simplification routines learned that an LTL formula like G(a & XF(b & XFc & Fd) can be simplified to G(a & Fb & Fc & Fd), and dually F(a | XG(b | XGc | Gd)) = F(a | Gb | Gc | Gd). When working with SERE, the simplification of "expr[*0..1]" was improved. E.g. {{a[*]|b}[*0..1]} becomes {a[*]|b} instead of {{a[+]|b}[*0..1]}. - The new function spot::to_weak_alternating() is able to take an input automaton with generalized Büchi/co-Büchi acceptance and convert it to a weak alternating automaton. - spot::sbacc() is can now also convert alternating automata to state-based acceptance. - spot::sbacc() and spot::degeneralize() learned to merge accepting sinks. - If the SPOT_BDD_TRACE environment variable is set, statistics about BDD garbage collection and table resizing are shown. - The & and | operators for acceptannce conditions have been changed slightly to be more symmetrical. In older versions, operator & would move Fin() terms to the front, but that is not the case anymore. Also operator & was already grouping all Inf() terms (for efficiency reasons), in this version operator | is symmetrically grouping all Fin() terms. - The automaton parser is now reentrant, making it possible to process automata from different streams at the same time (i.e., using multiple spot::automaton_stream_parser instances at once). - The print_hoa() and parse_automaton() functions have been updated to recognize the "exist-branch" property of the non-released HOA v1.1, as well as the new meaning of property "deterministic". (In HOA v1 "properties: deterministic" means that the automaton has no existential branching; in HOA v1.1 it disallows universal branching as well.) The meaning of "deterministic" in Spot has been adjusted to these new semantics, see "Backward-incompatible changes" below. - The parser for HOA now recognizes and verifies correct use of the "univ-branch" property. This is known to be a problem with option -H1 of ltl3ba 1.1.2 and ltl3dra 0.2.4, so the environment variable SPOT_HOA_TOLERANT can be set to disable the diagnostic. Python: - The 'spot.gen' package exports the functions from libspotgen. See https://spot.lrde.epita.fr/ipynb/gen.html for examples. Bugs fixed: - When the remove_fin() function was called on some automaton with Inf-less acceptance involving at least one disjunction (e.g., generalized co-Büchi), it would sometimes output an automaton with transition-based acceptance but marked as state-based. - The complete() function could complete an empty co-Büchi automaton into an automaton accepting everything. Backward-incompatible changes: - spot::acc_cond::mark_t::operator bool() has been marked as explicit. The implicit converion to bool (and, via bool, to int) was a source of bugs. - spot::twa_graph::set_init_state(const state*) has been removed. It was never used. You always want to use spot::twa_graph::set_init_state(unsigned) in practice. - The previous implementation of spot::is_deterministic() has been renamed to spot::is_universal(). The new version of spot::is_deterministic() requires the automaton to be both universal and existential. This should not make any difference in existing code unless you work with the recently added support for alternating automata. - spot::acc_cond::mark_t::sets() now returns an internal iterable object instead of an std::vector<unsigned>. - The color palette optionally used by print_dot() has been extended from 9 to 16 colors. While the first 8 colors are similar, they are a bit more saturated now. Deprecation notices: (These functions still work but compilers emit warnings.) - spot::decompose_strength() is deprecated, it has been renamed to spot::decompose_scc(). - spot::dtwa_complement() is deprecated. Prefer the more generic spot::dualize() instead. - The spot::twa::prop_deterministic() methods have been renamed to spot::twa::prop_universal() for consistency with the change to is_deterministic() listed above. We have kept spot::twa::prop_deterministic() as a deprecated synonym for spot::twa::prop_universal() to help backward compatibility. - The spot::copy() function is deprecated. Use spot::make_twa_graph() instead. -- Alexandre Duret-Lutz

1 0

Spot 2.3.5 released
by Alexandre Duret-Lutz 22 Jun '17

22 Jun '17

We are happy to announce the release of Spot 2.3.5 This is a maintenance release containing only bug fixes. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.3.5.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Furthermore, as Debian 9 "Stretch" was recently released, the stable Debian packages we distribute (see http://www.lrde.epita.fr/install.html) are now built for Stretch. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.3.5 (2017-06-22) Bugs fixed: - We have fixed new cases where translating multiple formulas in a single ltl2tgba run could produce automata different from those produced by individual runs. - The print_dot() function had a couple of issues when printing alternating automata: in particular, when using flag 's' (display SCC) or 'y' (split universal destination by colors) universal edges could be connected to undefined states. - Using --stats=%s or --stats=%s or --stats=%t could take an unnecessary long time on automata with many atomic propositions, due to a typo. Furthermore, %s/%e/%t/%E/%T were printing a number of reachable states/edges/transitions, but %S was incorrectly counting all states even unreachable. - Our verson of BuDDy had an incorrect optimization for the biimp operator. -- Alexandre Duret-Lutz

1 0

Spot 2.3.4 released
by Alexandre Duret-Lutz 11 May '17

11 May '17

We are happy to announce the release of Spot 2.3.4 This is a maintenance release that only contains bug fixes (listed below), and also corrects some minor build issues and typos. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.3.4.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.3.4 (2017-05-11) Bugs fixed: - The transformation to state-based acceptance (spot::sbacc()) was incorrect on automata where the empty acceptance mark is accepting. - The --help output of randaut and ltl2tgba was showing an unsupported %b stat. - ltldo and ltlcross could leave temporary files behind when aborting on error. - The LTL simplifcation rule that turns F(f)|q into F(f|q) when q is a subformula that is both eventual and universal was documented but not applied in some forgotten cases. - Because of some caching inside of ltl2tgba, translating multiple formula in single ltl2tgba run could produce automata different from those produced by individual runs. -- Alexandre Duret-Lutz

1 0

Spot 2.3.3 released
by Alexandre Duret-Lutz 11 Apr '17

11 Apr '17

We are happy to announce the release of Spot 2.3.3. This is a maintenance release that only contains minor bug fixes, and minor enhancements, as listed below. This release contains contributions from Thomas Medioni, Maximilien Colange, and myself. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.3.3.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.3.3 (2017-04-11) Tools: - ltldo and ltlcross learned shorthands to talk to ltl2da, ltl2dpa, and ltl2ldba (from Owl) without needing to specify %f>%O. - genltl learned --spec-patterns as an alias for --dac-patterns; it also learned two new sets of LTL formulas under --hkrss-patterns (a.k.a. --liberouter-patterns) and --p-patterns (a.k.a. --beem-patterns). Bugs fixed: - In "lenient" mode the formula parser would fail to recover from a missing closing brace. - The output of 'genltl --r-left=1 --r-right=1 --format=%F' had typos. - 'ltl2tgba Fa | autfilt --complement' would incorrectly claim that the output is "terminal" because dtwa_complement() failed to reset that property. - spot::twa_graph::purge_unreachable_states() was misbehaving on alternating automata. - In bench/stutter/ the .cc files were not compiling due to warnings being caught as errors. - The code in charge of detecting DBA-type Rabin automata is actually written to handle a slightly larger class of acceptance conditions (e.g., Fin(0)|(Fin(1)&Inf(2))), however it failed to correctly detect DBA-typeness in some of these non-Rabin acceptance. -- Alexandre Duret-Lutz

1 0

Spot 2.3.2 released
by Alexandre Duret-Lutz 15 Mar '17

15 Mar '17

We are happy to announce the release of Spot 2.3.2. This is a maintenance release that only contains minor bug fixes, and minor enhancements, as listed below. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.3.2.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. As always, please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.3.2 (2017-03-15) Tools: - In tools that output automata, the number of atomic propositions can be output using --stats=%x (output automaton) or --stats=%X (input automaton). Additional options can be passed to list atomic propositions instead of counting them. Tools that output formulas also support --format=%x for this purpose. Python: - The bdd_to_formula(), and to_generalized_buchi() functions can now be called in Python. Documentation: - https://spot.lrde.epita.fr/tut11.html is a new page describing how to build monitors in Shell, Python, or C++. Bugs fixed: - The tests using LTSmin's patched version of divine would fail if the current (non-patched) version of divine was installed. - Because of a typo, the output of --stats='...%P...' was correct only if %p was used as well. - genltl was never meant to have (randomly attributed) short options for --postive and --negative. - a typo in the code for transformating transition-based acceptance to state-based acceptance could cause a superfluous initial state to be output in some cases (the result was still correct). - 'ltl2tgba --any -C -M ...' would not complete automata. - While not incorrect, the HOA properties output by 'ltl2tgba -M' could be 'inherently-weak' or 'terminal', while 'ltl2tgba -M -D' would always report 'weak' automata. Both variants now report the most precise between 'weak' or 'terminal'. - spot::twa_graph::set_univ_init_state() could not be called with an initializer list. - The Python wrappers for spot::twa_graph::state_from_number and spot::twa_graph::state_acc_sets were broken in 2.3. - Instantiating an emptiness check on an automaton with unsupported acceptance condition should throw an exception. This used to be just an assertion, disabled in release builds; the difference matters for the Python bindings. Deprecation notice: - Using --format=%a to print the number of atomic propositions in ltlfilt, genltl, and randltl still works, but it is not documented anymore and should be replaced by the newly-introduced --format=%x for consistency with tools producing automata, where %a means something else. -- Alexandre Duret-Lutz

1 0