Annonce October 2012

annonce@lrde.epita.fr

1 participants
2 discussions

TUG 2011
by Didier Verna 12 Feb '13

12 Feb '13

I'm happy to announce that my contribution to TUG 2011, the next TeX Users Group International conference, has been accepted. Please find the title and abstract below. LaTeX Coding Standards Because LaTeX (and ultimately TeX) is only a macro-expansion system, the language does not impose any kind of good software engineering practice, program structure or coding style whatsoever. As a consequence, writing beautiful code (for some definition of "beautiful") requires a lot of self-discipline from the programmer. Maybe because in the LaTeX world, collaboration is not so widespread (most packages are single-authored), the idea of some LaTeX Coding Standards is not so pressing as with other programming languages. Some people may, and probably have developed their own programming habits, but when it comes to the LaTeX world as a whole, the situation is close to anarchy. Over the years, the permanent flow of personal development experiences contributed to shape my own taste in terms of coding style. The issues involved are numerous and their spectrum is very large: they range from simple code layout (formatting, indentation, naming schemes etc.), mid-level concerns such as modularity and encapsulation, to very high-level concerns like package interaction/conflict management and even some rules for proper social behavior. In this talk, I will report on all these experiences and describe what I think are good (or at least better) programming practices. I believe that such practices do help in terms of code readability, maintainability and extensibility, all key factors in software evolution. They help me, perhaps they will help you too. -- Resistance is futile. You will be jazzimilated. Scientific site: http://www.lrde.epita.fr/~didier Music (Jazz) site: http://www.didierverna.com EPITA/LRDE, 14-16 rue Voltaire, 94276 Le Kremlin-Bicêtre, France Tel. +33 (0)1 44 08 01 85 Fax. +33 (0)1 53 14 59 22

1 1

Spot 1.0 released
by Alexandre Duret-Lutz 27 Oct '12

27 Oct '12

After 9 years of releases with a leading "0." in their version number, this might be unexpected: We are pleased to announce the release of Spot 1.0. 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 major new releases features a set of completely rewritten command-line tools, an implementation of reverse simulation, and support for testing automata. You can find the new release here: http://spot.lip6.fr/dl/spot-1.0.tar.gz A more detailed listing of the changes follows. New in spot 1.0 (2012-10-27): * License change: Spot is now distributed using GPL v3+ instead of GPL v2+. This is because we started using some third-party files distributed under GPL v3+. * Command-line tools Useful command-line tools are now installed in addition to the library. Some of these tools were originally written for our test suite and had evolved organically into useful programs with crappy interfaces: they have now been rewritten with better argument parsing, saner defaults, and they come with man pages. - genltl: Generate LTL formulas from scalable patterns. This offers 20 patterns so far. - randltl: Generate random LTL/PSL formulas. - ltlfilt: Filter lists of formulas according to several criteria (e.g., match only safety formulas that are larger than some given size). Besides being used as a "grep" tool for formulas, this can also be used to convert files of formulas between different syntaxes, apply some simplifications, check whether to formulas are equivalent, ... - ltl2tgba: Translate LTL/PSL formulas into Büchi automata (TGBA, BA, or Monitor). A fundamental change to the interface is that you may now specify the goal of the translation: do you you favor deterministic or smaller automata? - ltl2tgta: Translate LTL/PSL formulas into Testing Automata. - ltlcross: Compare the output of translators from LTL/PSL to Büchi automata, to find bug or for benchmarking. This is essentially a Spot-based reimplementation of LBTT that supports PSL in addition to LTL, and that can output more statistics. An introduction to these tools can be found on-line at http://spot.lip6.fr/userdoc/tools.html The former test versions of genltl and randltl have been removed from the source tree. The old version of ltl2tgba with its gazillion options is still is src/tgbatest/ and is meant to be used for testing only. Although ltlcross is meant to replace LBTT, we are still using both tools in this release; however this is likely to be the last release of Spot that redistributes LBTT. * New features in the Spot library: - 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 ToPNoC VI (LNCS 7400). The web-based interface and the aforementioned ltl2tgta tool can be used to build 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. - The enumerate_cycles class implements the Loizou-Thanisch algorithm to enumerate elementary cycles in a SCC. As an example of use, is_weak_scc() will tell whether an SCC is inherently weak (all its cycles are accepting, or none of them are). - parse_lbt() will parse an LTL formula expressed in the prefix syntax used (at least) by LBT, LBTT and Scheck. to_lbt_string() can be used to print an LTL formula using this syntax. - to_wring_string() can be used to print an LTL formula into Wring's syntax. - The LTL/PSL parser now has a lenient mode that can be useful to interpret atomic proposition with language-specific constructs. In lenient mode, any (...) or {...} block that cannot be parsed as formula will be assumed to be an atomic proposition. For instance the input (a < b) U (process[2]@ok), normally flagged as a syntax error, is read as "a < b" U "process[2]@ok" in lenient mode. - minimize_obligation() has a new option to disable WDBA minimization it cases it would produce a deterministic automaton that is bigger than the original TGBA. This can help choosing between less states or more determinism. - new functions is_deterministic() and count_nondet_states() (The count of nondeterministic states is now displayed on automata generated with the web interface.) - A new class, "postprocessor", makes it easier to apply all available simplification algorithms on a TGBA/BA/Monitors. * Minor changes: - The '*' operator can (again) be used as an AND in LTL formulas. This is for compatibility with formula written in Wring's syntax. However inside SERE it is interpreted as the Kleen star. - When printing a formula using Spin's LTL syntax, we don't double-quote complex atomic propositions (that was not valid Spin input anyway). For instance F"foo == 2" used to be output as <>"foo == 2". We now output <>(foo == 2) instead. The latter syntax is understood by Spin 6. It can be read back by Spot in lenient mode (see above). - The gspn-ssp benchmark has been removed.

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Annonce October 2012