Spot-announce

spot-announce@lrde.epita.fr

105 discussions

by Alexandre Duret-Lutz

Spot 1.2.4 has been released. This maintenance release fixes a crashing scenario in the translation of testing automata, a couple of incorrect PSL simplifications, and a bug in the translation of the fusion operator. You can download the new release here: http://spot.lip6.fr/dl/spot-1.2.4.tar.gz New in spot 1.2.4 (2014-05-15) * New features: - "-B -x degen-lskip" can be used to disable level-skipping in the degeralization procedure called by ltl2tgba and dstar2tgba. This is mostly meant for running experiments. - "-B -x degen-lcache=N" can be used to experiment with different type of level caching during degeneralization. * Bug fixes: - Change the Python bindings to make them compatible with Swig 3.0. - "ltl2tgta --ta" could crash in certain conditions due to the introduction of a simulation-based reduction after degeneralization. - Fix four incorrect formula-simplification rules, three were related to the factorization of Boolean subformulas in operands of the non-length-matching "&" SERE operator, and a fourth one could only be enabled by explicitely passing the favor_event_univ option to the simplifier (not the default). - Fix incorrect translation of the fusion operator (":") in SERE such as {xx;1}:yy[*] where the left operand has 1 as tail. -- Alexandre Duret-Lutz

10 years, 8 months

Spot 1.2.3 released

by Alexandre Duret-Lutz

We are happy to announce that Spot 1.2.3 has been released. This maintenance release addresses more portability issues and other minor bugs listed below. It also supports a new SPOT_SATLOG environment variable to extra more statistics from our SAT-based minimization procedures. It contains contributions from Alexandre Lewkowicz and Étienne Renault. You can download the new release here: http://spot.lip6.fr/dl/spot-1.2.3.tar.gz New in spot 1.2.3 (2014-02-11) * New features: - The SPOT_SATLOG environment variable can be set to a filename to obtain statistics about the different iterations of the SAT-based minimization. For an example, see http://spot.lip6.fr/userdoc/satmin.html - The bench/dtgbasat/ benchmark has been updated to use SPOT_SATLOG and record more statistics. - The default value for the SPOT_SATSOLVER environment variable has been changed to "glucose -verb=0 -model %I >%O". This assumes that glucose 3.0 is installed. For older versions of glucose, remove the "-model" option. * Bug fixes: - More fixes for Python 3 compatibility. - Fix calculation of length_boolone(), were 'Xa|b|c' was considered as length 6 instead of 4 (because it is 'Xa|(b|a)' were (b|a) is Boolean). - Fix Clang-3.5 warnings. - randltl -S did not honor --boolean-priorities. - randltl had trouble generating formulas when all unary, or all binary/n-ary operators were disabled. - Fix spurious testsuite failure when using Pandas 0.13. - Add the time spent in child processes when measuring time with the timer class. - Fix determinism of the SAT-based minimization encoding. (It would sometimes produce different equivalent automata, because of a different encoding order.) - A the SAT-based minimization is asked for a 10-state automaton and return a 6-state automaton, do not ask for a 9-state automaton in the next iteration... - Fix some compilation issue with the version of Apple's Clang that is installed with MacOS X 10.9. - Fix VPATH builds when building from the git repository. - Fix UP links in the html documentation for command-line tools. -- Alexandre Duret-Lutz

10 years, 11 months

Spot 1.2.2 has been released

by Alexandre Duret-Lutz

I'm happy to announce that Spot 1.2.2 has been released. This maintenance release addresses a couple of portability issues and other minor bugs discovered over the last month. You can download the new release here: http://spot.lip6.fr/dl/spot-1.2.2.tar.gz New in spot 1.2.2 (2014-01-24) * Bug fixes: - Fix compilation *and* behavior of bitvectors on 32-bit architectures. - Fix some compilation errors observed using the antique G++ 4.0.1. - Fix compatibility with Python 3 in the test suite. - Fix a couple of new clang warnings (like "unused private member"). - Add some missing #includes that are not included indirectly when the C++ compiler is in C++11 mode. - Fix detection of numbers that are too large in the ELTL parser. - Fix a memory leak in the ELTL parser, and avoid some unnecessary calls to strlen() at the same time. -- Alexandre Duret-Lutz

11 years

Spot 1.2.1 released (a release focused on CSV output and input)

by Alexandre Duret-Lutz

I'm happy to announce that Spot 1.2.1 has been released. These release improves the CSV reporting of ltlcross (including size for Rabin or Streett automata, separate measurements in case multiple products are used, and information about the exit status of the translators). As a consequence the order of columns has changed slightly, and it will break scripts that use hardcoded column positions. If you want to get a CSV output that is closest to what ltlcross used to output before, use the --omit-missing option (but even with that the "time" column has been shifted left). Other tools have also learned how to read CSV files, and have some options to help creating CSV files. You can download the new release here: http://spot.lip6.fr/dl/spot-1.2.1.tar.gz New in spot 1.2.1 (2013-12-11) * New features: - commands for translators specified to ltlcross can now be given "short names" to be used in the CSV or JSON output. For instance ltlcross '{small} ltl2tgba -s --small %f >%N' ... will run the command "ltl2tgba -s --small %f >%N", but only print "small" in output files. - ltlcross' CSV and JSON output now contains two additional columns: exit_status and exit_code, used to report failures of the translator. If the translation failed, only the time is reported, and the rest of the statistics, which are missing, area left empty (in CVS) or null (in JSON). A new option, --omit-missing can be used to remove lines for failed translations, and remove these two columns. - if ltlcross is used with --products=+5 instead of --products=5 then the stastics for each of the five products will be output separately instead of being averaged. - if ltlcross is used with tools that produce deterministic Streett or Rabin automata (as specified with %D), then the statistics output in CSV or JSON will have some extra columns to report the size of these input automata before ltlcross converts them into TGBA to perform its regular checks. - ltlfilt, ltl2tgba, ltl2tgta, and ltlcross can now read formulas from CSV files. Use option -F FILE/COL to read formulas from column COL of FILE. Use -F FILE/-COL if the first line of FILE be ignored. - when ltlfilt processes formulas from a CSV file, it will output each CSV line whose formula matches the given constraints, with the rewriten formula. The new escape sequence %< (text in columns before the formula) and %> (text after) can be used with the --format option to alter this output. - ltlfile, genltl, randltl, and ltl2tgba have a --csv-escape option to help escape formulas in CSV files. - Please check http://spot.lip6.fr/userdoc/csv.html for some discussion and examples of the last few features. * Bug fixes: - ltlcross' CSV output has been changed to be more RFC 4180 compliant: it no longuer output useless cosmetic spaces, and use double-quotes with proper escaping for strings. The only RFC 4180 rule that it does not follow is that it will terminate lines with \n instead of \r\n because the latter cause issues with a couple of tools. - ltlcross failed to report missing input or output escape sequences on all but the first configured translator. -- Alexandre Duret-Lutz

11 years, 1 month

Spot 1.2 released

by Alexandre Duret-Lutz

I'm very pleased to announce the release of Spot 1.2. Spot is a model-checking library developed collaboratively by LRDE and LIP6. It provides algorithms and data structures to implement the automata-theoretic approach to LTL model checking. This release contains several new features (summarized below), but the most notable are the interface with ltl2dstar (i.e., Spot can read deterministic Rabin and Streett automata and convert them into Büchi automata) and algorithms for minimizing deterministic TGBA or BA using a SAT-solver. You can find the new version here: http://spot.lip6.fr/dl/spot-1.2.tar.gz Please report any issue to <spot(a)lrde.epita.fr>. New in spot 1.2 (2013-10-01) * Changes to command-line tools: - ltlcross has a new option --color to color its output. It is enabled by default when the output is a terminal. - ltlcross will give an example of infinite word accepted by the two automata when the product between a positive automaton and a negative automaton is non-empty. - ltlcross can now read the Rabin and Streett automata output by ltl2dstar. This type of output should be specified using '%D': ltlcross 'ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-s %L %D' However because Spot only supports Büchi acceptance, these Rabin and Streett automata are immediately converted to TGBAs before further processing by ltlcross. This is still interesting to search for bugs in translators to Rabin or Streett automata, but the statistics (of the resulting TGBAs) might not be very relevant. - When ltlcross obtains a deterministic automaton from a translator it will now complement this automaton to perform additional intersection checks. This is complementation is done only for deterministic automata (because that is cheap) and can be disabled with --no-complement. - To help with debugging problems detected by ltlcross, the environment variables SPOT_TMPDIR and SPOT_TMPKEEP control where temporary files are created and if they should be erased. Read the man page of ltlcross for details. - There is a new command, named dstar2tgba, that converts a deterministic Rabin or Streett automaton (expressed in the output format of ltl2dstar) into a TGBA, BA or Monitor. In the case of Rabin acceptance, the conversion will output a deterministic Büchi automaton if one such automaton exist. Even if no such automaton exists, the conversion will actually preserves the determinism of any SCC that can be kept deterministic. In the case of Streett acceptance, the conversion produces non-deterministic Büchi automata with Generalized acceptance. These are then degeneralized if requested. See http://spot.lip6.fr/userdoc/dstar2tgba.html for some examples, and the man page for more reference. - The %S escape sequence used by ltl2tgba --stats to display the number of SCCs in the output automaton has been renamed to %c. This makes it more homogeneous with the --stats option of the new dstar2tgba command. Additionally, the %p escape can now be used to show whether the output automaton is complete, and the %r escape will give the number of seconds spent building the output automaton (excluding the time spent parsing the input). - ltl2tgba, ltl2tgta, and dstar2tgba have a --complete option to output complete automata. - ltl2tgba, ltl2tgta, and dstar2tgba can use a SAT-solver to minimize deterministic automata. Doing so is only needed on properties that are stronger than obligations (for obligations our WDBA-minimization procedure will return a minimimal deterministic automaton more efficiently) and is disabled by default. See the spot-x(7) man page for documentation about the related options: sat-minimize, sat-states, sat-acc, state-based. See also http://spot.lip6.fr/userdoc/satmin.html for some examples. - ltlfilt, genltl, and randltl now have a --latex option to output formulas in a way that its easier to embed in a LaTeX document. Each operator is output as a command such as \U, \F, etc. doc/tl/spotltl.sty gives one possible definition for each macro. - ltlfilt, genltl, and randltl have a new --format option to indicate how to present the output formula, possibly with information about the input. - ltlfilt as a new option, --relabel-bool, to abstract independent Boolean subformulae as if they were atomic propositions. For instance "a & GF(c | d) & b & X(c | d)" would be rewritten as "p0 & GF(p1) & Xp1". * New functions and classes in the library: - dtba_sat_synthetize(): Use a SAT-solver to build an equivalent deterministic TBA with a fixed number of states. - dtba_sat_minimize(), dtba_sat_minimize_dichotomy(): Iterate dtba_sat_synthetize() to reduce the number of states of a TBA. - dtgba_sat_synthetize(), dtgba_sat_minimize(), dtgba_sat_minimize_dichotomy(): Likewise, for deterministic TGBA. - is_complete(): Check whether a TGBA is complete. - tgba_complete(): Complete an automaton by adding a sink state if needed. - dtgba_complement(): Complement a deterministic TGBA. - satsolver(): Run an (external) SAT solver, honoring the SPOT_SATSOLVER environment variable if set. - tba_determinize(): Run a power-set construction, and attempt to fix the acceptance simulation to build a deterministic TBA. - dstar_parse(): Read a Streett or Rabin automaton in ltl2dstar's format. Note that this format allows only deterministic automata. - nra_to_nba(): Convert a (possibly non-deterministic) Rabin automaton to a non-deterministic Büchi automaton. - dra_to_ba(): Convert a deterministic Rabin automaton to a Büchi automaton, preserving acceptance in all SCCs where this is possible. - nsa_to_tgba(): Convert a (possibly non-deterministic) Streett automaton to a non-deterministic TGBA. - dstar_to_tgba(): Convert any automaton returned by dstar_parse() into a TGBA. - build_tgba_mask_keep(): Build a masked TGBA that shows only a subset of states of another TGBA. - build_tgba_mask_ignore(): Build a masked TGBA that ignore a subset of states of another TGBA. - class tgba_proxy: Helps writing on-the-fly algorithms that delegate most of their methods to the original automaton. - class bitvect: A dynamic bit vector implementation. - class word: An infinite word, stored as prefix + cycle, with a simplify() methods to simplify cycle and prefix in obvious ways. - class temporary_file: A temporary file. Can be instanciated with create_tmp_file() or create_open_tmpfile(). - count_state(): Return the number of states of a TGBA. Implement a couple of specializations for classes where is can be know without exploration. - to_latex_string(): Output a formula using LaTeX syntax. - relabel_bse(): Relabeling of Boolean Sub-Expressions. Implements ltlfilt's --relabel-bool option describe above. * Noteworthy internal changes: - When minimize_obligation() is not given the formula associated to the input automaton, but that automaton is deterministic, it can still attempt to call minimize_wdba() and check the correcteness using dtgba_complement(). This allows dstar2tgba to apply WDBA-minimization on deterministic Rabin automata. - tgba_reachable_iterator_depth_first has been redesigned to effectively perform a DFS. As a consequence, it does not inherit from tgba_reachable_iterator anymore. - postproc::set_pref() was used to accept an argument among Any, Small or Deterministic. These can now be combined with Complete as Any|Complete, Small|Complete, or Deterministic|Complete. - operands of n-ary operators (like & and |) are now ordered so that Boolean terms come first. This speeds up syntactic implication checks slightly. Also, literals are now sorted using strverscmp(), so that p5 comes before p12. - Syntactic implication checks have been generalized slightly (for instance 'a & b & F(a & b)' is now reduced to 'a & b' while it was not changed in previous versions). - All the parsers implemented in Spot now use the same type to store locations. - Cleanup of exported symbols All symbols in the library now have hidden visibility on ELF systems. Public classes and functions have been marked explicitely for export with the SPOT_API macro. During this massive update, some of functions that should not have been made public in the first place have been moved away so that they can only be used from the library. Some old of unused functions have been removed. removed: - class loopless_modular_mixed_radix_gray_code hidden: - class acc_compl - class acceptance_convertor - class bdd_allocator - class free_list * Bug fixes: - Degeneralization was not indempotant on automata with an accepting initial state that was on a cycle, but without self-loop. - Configuring with --enable-optimization would reset the value of CXXFLAGS. -- Alexandre Duret-Lutz

11 years, 4 months

Spot 1.1.4 released

by Alexandre Duret-Lutz

Spot 1.1.4 has been released. This maintenance release fixes a couple of bugs reported over the last weeks. These include a regression preventing 1.1.3 to parse neverclaims produced by ltl2ba or ltl3ba, and a bug in the interpretation of the closure of some SERE. You can download the new release here: http://spot.lip6.fr/dl/spot-1.1.4.tar.gz New in spot 1.1.4 (2013-07-29) * Bug fixes: - The parser for neverclaim, updated in 1.1.3, would fail to parse guards of the form (a) || (b) output by ltl2ba or ltl3ba, and would only understand ((a) || (b)). - When used from ltlcross, the same parser would fail to parse further neverclaims after the first failure. - Add a missing newline in some error message of ltlcross. - Expressions like {SERE} were wrongly translated and simplified for SEREs that accept the empty word: they were wrongly reduced to true. Simplification and translation rules have been fixed, and the doc/tl/tl.pdf specifications have been updated to better explain that {SERE} has the semantics of a closure operator that is not exactly what one could expect after reading the PSL standard. - Various typos. -- Alexandre Duret-Lutz (off for three weeks)

11 years, 6 months

Spot 1.1.3 has been released

by Alexandre Duret-Lutz

I'm pleased to announce the release of Spot 1.1.3. This maintenance release fixes a couple of bugs reported over the last month, and add support for reading the new neverclaims output by Spin 6.24+ (they can be parsed by ltlcross, for instance). You can download the new release here: http://spot.lip6.fr/dl/spot-1.1.3.tar.gz New in spot 1.1.3 (2013-07-09) * New feature: - The neverclaim parser now understands the new style of output used by Spin 6.24 and later. * Bug fixes: - The scc_filter() function could abort with a BDD error. If all the acceptance sets of an SCC but the first one were useless. - The script in bench/spin13/ would not work on MacOS X because of some non-portable command. - A memory corruption in ltlcross. -- Alexandre Duret-Lutz

11 years, 7 months

Spot 1.1.2 released

by Alexandre Duret-Lutz

Spot 1.1.2 has been released. This maintainance release fixes a couple minor bugs. If you have version 1.1.1 already installed, there is no reason to upgrade unless you are using ltlcross to generate statistics. You can download the new release here: http://spot.lip6.fr/dl/spot-1.1.2.tar.gz New in spot 1.1.2 (2013-06-09) * Bug fixes: - Uninitialized variables in ltlcross (affect the count of terminal weak, and strong SCCs). - Workaround an old GCC bug to allow compilation with g++ <= 4.5 - Fix several Doxygen comments so that they display correctly. -- Alexandre Duret-Lutz

11 years, 8 months

Spot 1.1.1 released

by Alexandre Duret-Lutz

This is to announce the release of Spot 1.1.1. The main motivation for this release is to fix a bug introduced in version 1.1 in the post-processing of (degeneralized) Büchi automata. Although the NEWS excerpt at the end of this email shows several new features, most of them are related to the discovery and fix of this bug: 1) With this release, ltl2tgba --ba --lbtt has been changed to output automata using the state-based acceptance flavor of the LBTT format. This makes more sense when you work with Büchi automata. 2) This lead to the discovery that previously, when --lbtt always output automata with transition-based acceptance, there were some rare formulas where ltl2tgba --ba --lbtt could output automata that where not Büchi automata (although they had the correct language), and worse: ltl2tgba --spin could output an incorrect neverclaim. 3) fixing this required to reimplement two functions we started using in 1.0 but that messed the structure of Büchi automata: namely reverse simulation and SCC-based simplification of acceptance condition. Two small and easy options have also been added to ltlcross. You can find the new release here: http://spot.lip6.fr/dl/spot-1.1.1.tar.gz A summary of the changes follows. Please report any issue to <spot(a)lrde.epita.fr>. New in spot 1.1.1 (2013-05-13): * New features: - lbtt_reachable(), the function that outputs a TGBA in LBTT's format, has a new option to indicate that the TGBA being printed is in fact a Büchi automaton. In this case it outputs an LBTT automaton with state-based acceptance. The output of the guards has also been changed in two ways: 1. atomic propositions that do not match p[0-9]+ are always double-quoted. This avoids issues where t or f were used as atomic propositions in the formula, output as-is in the automaton, and read back as true or false. Other names that correspond to LBT operators would cause problem as well. 2. formulas that label transitions are now output as irredundant-sums-of-products. - 'ltl2tgba --ba --lbtt' will now output automata with state-based acceptance. You can use 'ltl2tgba --ba --lbtt=t' to force the output of transition-based acceptance like in the previous versions. Some illustrations of this point and the previous one can be found in the man page for ltl2tgba(1). - There is a new function scc_filter_states() that removes all useless states from a TGBA. It is actually an abbridged version of scc_filter() that does not alter the acceptance conditions of the automaton. scc_filter_state() should be used when post-processing TGBAs that actually represent BAs. - simulation_sba(), cosimulation_sba(), and iterated_simulations_sba() are new functions that apply to TGBAs that actually represent BAs. They preserve the imporant property that if a state of the BA is is accepting, the outgoing transitions of that state are all accepting in the TGBA that represent the BA. This is something that was not preserved by functions cosimultion() and iterated_simulations() as mentionned in the bug fixes below. - ltlcross has a new option --seed, that makes it possible to change the seed used by the random graph generator. - ltlcross has a new option --products=N to check the result of each translation against N different state spaces, and everage the statistics of these N products. N default to 1; larger values increase the chances to detect inconsistencies in the translations, and also make the average size of the product built against the translated automata a more pertinent statistic. - bdd_dict::unregister_all_typed_variables() is a new function, making it easy to unregister all BDD variables of a given type owned by some object. * Bug fixes: - genltl --gh-r generated the wrong formulas due to a typo. - ltlfilt --eventual and --universal were not handled properly. - ltlfilt --stutter-invariant would trigger an assert on PSL formulas. - ltl2tgba, ltl2tgta, ltlcross, and ltlfilt, would all choke on empty lines in a file of formulas. They now ignore empty lines. - The iterated simulation applied on degeneralized TGBA was bogus for two reasons: one was that cosimulation was applied using the generic cosimulation for TGBA, and the second is that SCC-filtering, performed between iterations, was also a TGBA-based algorithm. Both of these algorithms could lose the property that if a TGBA represents a BA, all the outgoing transitions of a state should be accepting. As a consequence, some formulas where translated to incorrect Büchi automata. -- Alexandre Duret-Lutz

11 years, 8 months

Spot 1.1 released

by Alexandre Duret-Lutz

We are pleased to announce the release of Spot 1.1. Spot is a model-checking library developed collaboratively by LRDE and LIP6. It provides algorithms and data structures to implement the automata-theoretic approach to LTL model checking. This release features several improvements developped with our collegues from the Mazaryk University (also authors of the ltl3ba translator) as detailed in the following paper: Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský, Jan Strejček: Compositional Approach to Suspension and Other Improvements to LTL Translation. To appear in the proceedings of SPIN'13. You can find the new release here: http://spot.lip6.fr/dl/spot-1.1.tar.gz A summary of the changes follows. Please report any issue to <spot(a)lrde.epita.fr>. New in spot 1.1 (2013-04-28): * New features in the library: - The postprocessor class now takes an optional option_map argument that can be used to specify fine-tuning options, making it easier to benchmark different scenarios while developing new postprocessings. - A new translator class implements a complete translation chain, from LTL/PSL to TGBA/BA/Monitor. It performs pre- and post-processings in addition to the core translation, and offers an interface similar to that used in the postprocessor class, to specify the intent of the translation. - The degeneralization algorithm has learned three new tricks: level reset, level caching, and SCC-based ordering. The former two are enabled by default. Benchmarking has shown that the latter one does not always have a positive effect, so it is disabled by default. (See SPIN'13 paper.) - The scc_filter() function, which removes dead SCCs and also simplify acceptance conditions, has learnt how to simplify acceptance conditions in a few tricky situations that were not simplified previously. (See SPIN'13 paper.) - An experimental "don't care" (direct) simulation has been implemented. This simulations consider the acceptance of out-of-SCC transitions as "don't care". It is not enabled by default because it currently is very slow. - remove_x() is a function that take a formula, and rewrite it without the X operator. The rewriting is only correct for stutter-insensitive LTL formulas (See K. Etessami's paper in IFP vol. 75(6). 2000) This algorithm is accessible from the command-line using ltlfilt's --remove-x option. - is_stutter_insensitive() takes any LTL formula, and check whether it is stutter-insensitive. This algorithm is accessible from the command-line using ltlfilt's --stutter-insensitive option. - A new translation, called compsusp(), for "Compositional Suspension" is implemented on top of ltl_to_tgba_fm(). (See SPIN'13 paper.) - Some experimental LTL rewriting rules that trie to gather suspendable formulas are implemented and can be activated with the favor_event_univ option of ltl_simplifier. As always please check doc/tl/tl.tex for the list of rules. - Several functions have been introduced to check the strength of an SCC. is_inherently_weak_scc() is_weak_scc() is_syntactic_weak_scc() is_complete_scc() is_terminal_scc() is_syntactic_terminal_scc() Beware that the costly is_weak_scc() function introduced in Spot 1.0, which is based on a cycle enumeration, has been renammed to is_inherently_weak_scc() to match established vocabulary. * Command-line tools: - ltl2tgba and ltl2tgta now honor a new --extra-options (or -x) flag to fine-tune the algorithms used. The available options are documented in the spot-x (7) manpage. For instance use '-x comp-susp' to use the afore-mentioned compositional suspension. - The output format of 'ltlcross --json' has been changed slightly. In a future version we will offer some reporting script that turn such JSON output into various tables and graphs, and these change are required to make the format usable for other benchmarks (not just ltlcross). - ltlcross will now count the number of non-accepting, terminal, weak, and strong SCCs, as well as the number of terminal, weak, and strong automata produced by each tool. * Documentation: - org-mode files used to generate the documentation about command-line tools (shown at http://spot.lip6.fr/userdoc/tools.html) is distributed in doc/org/. The resulting html files are also in doc/userdoc/. * Bug fixes: - There was a memory leak in the LTL simplification code, that could only be triggered when disabling advanced simplifications. - The translation of the PSL formula !{xxx} was incorrect when xxx simplified to false. - Various warnings triggered by new compilers. -- Alexandre Duret-Lutz

11 years, 9 months

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot-announce