Spot-announce December 2013

spot-announce@lrde.epita.fr

1 participants
1 discussions

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

10 years, 4 months

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot-announce December 2013