- Annonce

Accepted paper at ELS 2018
by Jim Newton 05 Apr '18

05 Apr '18

Greetings, I am pleased to announce that our paper "Approaches in Typecase Optimization” has been accepted to the next European Lisp Symposium, April 16-17, Marbella, Spain. Please find the abstract below. If anyone would like to take a look at the paper, your comments are welcome. https://www.lrde.epita.fr/dload/papers/newton.18.els.pdf <https://www.lrde.epita.fr/dload/papers/newton.18.els.pdf> Abstract We contrast two approaches to optimizing the Common Lisp typecase macro expansion. The first approach is based on heuristics intended to estimate run time performance of certain type checks involving Common Lisp type specifiers. The technique may, depending on code size, exhaustively search the space of permutations of the type checks, intent on finding the optimal order. With the second technique, we represent a typecase form as a type specifier, encapsulating the side-effecting non-Boolean parts so as to appear compatible with the Common Lisp type algebra operators. The encapsulated expressions are specially handled so that the Common Lisp type algebra functions preserve them, and we can unwrap them after a process of Boolean reduction into efficient Common Lisp code, maintaining the appropriate side effects but eliminating unnecessary type checks. Both approaches allow us to identify unreachable code, test for exhaustiveness of the clauses and eliminate type checks which are calculated to be redundant.

1 0

Vcsn 2.7 is released!
by Akim Demaille 29 Mar '18

29 Mar '18

We are happy to announce the release of Vcsn 2.7! As most of our efforts are currently on Vcsn 3, this is mostly a bug fix release, with improvements in the documentation based on user feedback. For more information see the detailed news below. Release page: https://vcsn.lrde.epita.fr/Vcsn2.7 Tarball: https://www.lrde.epita.fr/dload/vcsn/2.7/vcsn-2.7.tar.xz Home page: https://vcsn.lrde.epita.fr The various packages (Arch, Debian, Docker, MacPorts, etc.) will appear soon. ## New features ### Improved compatibility between single- and multitape expressions The automatic promotion from single-tape to multitape is more general. For instance (| separates tapes and @ denotes composition): In [2]: c = vcsn.context('lat<lan, lan>, b') In [3]: c.expression('a') Out[3]: a|a In [4]: c.expression('a*b* @ (ab)*') Out[4]: (a|a)*(b|b)*@((a|a)(b|b))* In [5]: c.expression('a*b* @ (ab)*').shortest(10) Out[5]: \e|\e + ab|ab ### vcsn doc is a new tool Run `vcsn doc automaton.determinize`, or `vcsn doc Automata`, etc. The special shortcuts `vcsn doc` opens the Read-me-first notebook, and `vcsn doc index` leads to Algorithms, the page that lists the existing documentation of algorithms (`automata.determinize`, etc.). ### Compressed efsm files Vcsn can read efsm files compressed with bzip2 and xz. In some extreme cases, the xz-compressed efsm file was reduced to 5% of the original size. The files for the sms2fr demo are now compressed with xz. ### vcsn score has several new options The command `vcsn score` benchmarks Vcsn. Its output can be processed with `vcsn score-compare` to see the trends in performances between versions. Benchmarks are now numbered, to give a hint of the progress: $ vcsn score vcsn version: 2.6-085-g6dcae17ef 1/116 0.25s : a.is_proper() # a = "", 1000000x 2/116 0.11s : b.format("text") # b = [abc] -> B, 100000x 3/116 0.35s : b.expression(e) # e = [ab]{20000}, 1000x ... 115/116 0.75s : a.weight_series() # a = std(a{12000}+<1>[b-z]{12000}), c = [a-z] -> Nmin, 200x 116/116 0.89s : a.weight_series() # a = std([a-z]{200}), c = [a-z] -> Z, 10x The new option `-o`/`--output` allows to specify the output file name. Better yet: option `-d`/`--dir` specifies the directory in which the score file is saved; its name will be forged from `git describe`, something like `v2.5-050-g01dbf326`. Such names are interpreted by `vcsn score-compare` to relate the benches to the git commit title. Both features need that you run these commands from a git repository of Vcsn. Option `-j`/`--job` allows to run the benchmarks concurrently. This can be very useful to "warm" vcsn (have it compile the needed algorithms), or to get a nice approximation of the actual benches, however, sticking to a single bench at a time is recommended to get faithful measurements. Option `-l`/`--list` lists the benches without running them. Option `-s`/`--sort` sorts the benchmarks before running them. ### Documentation Several errors were fixed. The page `expression.compose.ipynb` is new. ### Examples of C++ The directories `tests/demo` and `tests/benchmarks` contain more examples using the Vcsn C++ library. ## Bug fixes ### Incorrect order for 8bit characters Calling `compare` on labels would lead to surprising results with 8bit characters (seen as negative ints). This resulted in the incorrect display of the expression `[\x01-\xfe]` as `[\x80-\xfe] + [\x01-\x7f]`. Both are fixed, and 1 is less than 254 again.

1 0

Accepted paper at ELS 2018
by Didier Verna 20 Mar '18

20 Mar '18

Greetings, I'm pleased to announce that my paper entitled "Method Combinators" has been accepted to the next European Lisp Symposium, April 16-17, Marbella, Spain. Please find the abstract below. Method Combinators In traditional object-oriented languages, the dynamic dispatch algorithm is hardwired: for every polymorphic call, only the most specific method is used. CLOS, the Common Lisp Object System, goes beyond the traditional approach by providing an abstraction known as "method combinations": when several methods are applicable, it is possible to select several of them, decide in which order they will be called and how to combine their results, essentially making the dynamic dispatch algorithm user-programmable. Although a powerful abstraction, method combinations are under-specified in the Common Lisp standard, and the MOP, the Meta-Object Protocol underlying many implementations of CLOS, worsens the situation by either contradicting it or providing unclear protocols. As a consequence, too much freedom is granted to conforming implementations, the exact or intended behavior of method combinations is unclear and not necessarily coherent with the rest of CLOS. In this paper, we provide a detailed analysis of the problems posed by method combinations, the consequences of their lack of proper specification in one particular implementation, and a MOP-based extension called "method combinators", aiming at correcting these problems and possibly offer new functionality. -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 0

[CfPart] European Lisp Symposium 2018, 16-17 April, Marbella, Spain
by Didier Verna 14 Mar '18

14 Mar '18

ELS'18 - 11th European Lisp Symposium Centro Cultural Cortijo de Miraflores Marbella, Málaga Spain April 16-17 2018 Sponsored by Brunner Software GmbH, Franz Inc., LispWorks Ltd., and EPITA http://www.european-lisp-symposium.org/ Recent news: - Invited speakers announced (see below) - Registration open. Don't miss the March 25 deadline for the early bird discount! The purpose of the European Lisp Symposium is to provide a forum for the discussion and dissemination of all aspects of design, implementation and application of any of the Lisp and Lisp-inspired dialects, including Common Lisp, Scheme, Emacs Lisp, AutoLisp, ISLISP, Dylan, Clojure, ACL2, ECMAScript, Racket, SKILL, Hop and so on. We encourage everyone interested in Lisp to participate. Keynote speakers: - Vsevolod Domkin -- Lisp in a Startup: the Good, the Bad, and the Ugly - R. Matthew Emerson -- This Old Lisp (a look at Clozure CL) Important dates: - 25 Mar 2018 Early registration deadline - 16-17 Apr 2018 Symposium Programme chair: David Cooper, Genworks Intl., USA Local chairs: Andrew Lawson, Ravenpack, Spain Programme committee: Andy Wingo, Igalia, Spain Christophe Rhodes, Goldsmiths University, UK Christopher Wellons Null Program Canada Irène Durand, LaBRI, Université de Bordeaux, France Julian Padget, University of Bath, UK Ludovic Courtès, Inria, France Michael Sperber, DeinProgramm, Germany Nicolas Neuss, FAU Erlangen-Nürnberg, Germany Olin Shivers Northeastern University USA Philipp Marek, Austria Robert Strandh, LaBRI, Université de Bordeaux, France Sacha Chua Living an Awesome Life Canada Scott McKay, Future Fuel, USA Search Keywords: #els2018, ELS 2018, ELS '18, European Lisp Symposium 2018, European Lisp Symposium '18, 10th ELS, 10th European Lisp Symposium, European Lisp Conference 2018, European Lisp Conference '18 -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 0

[Final CfP] European Lisp Symposium 2018 -- Deadline extension
by Didier Verna 20 Feb '18

20 Feb '18

ELS'18 - 11th European Lisp Symposium Centro Cultural Cortijo de Miraflores Marbella, Málaga Spain April 16-17 2018 Sponsored by Brunner Software GmbH and EPITA http://www.european-lisp-symposium.org/ *** Important: submission deadline extended to Sunday Feb. 25! The purpose of the European Lisp Symposium is to provide a forum for the discussion and dissemination of all aspects of design, implementation and application of any of the Lisp and Lisp-inspired dialects, including Common Lisp, Scheme, Emacs Lisp, AutoLisp, ISLISP, Dylan, Clojure, ACL2, ECMAScript, Racket, SKILL, Hop and so on. We encourage everyone interested in Lisp to participate. The 11th European Lisp Symposium invites high quality papers about novel research results, insights and lessons learned from practical applications and educational perspectives. We also encourage submissions about known ideas as long as they are presented in a new setting and/or in a highly elegant way. Topics include but are not limited to: - Context-, aspect-, domain-oriented and generative programming - Macro-, reflective-, meta- and/or rule-based development approaches - Language design and implementation - Language integration, inter-operation and deployment - Development methodologies, support and environments - Educational approaches and perspectives - Experience reports and case studies We invite submissions in the following forms: Papers: Technical papers of up to 8 pages that describe original results or explain known ideas in new and elegant ways. Demonstrations: Abstracts of up to 2 pages for demonstrations of tools, libraries, and applications. Tutorials: Abstracts of up to 4 pages for in-depth presentations about topics of special interest for at least 90 minutes and up to 180 minutes. The symposium will also provide slots for lightning talks, to be registered on-site every day. All submissions should be formatted following the ACM SIGS guidelines and include ACM Computing Classification System 2012 concepts and terms. Submissions should be uploaded to Easy Chair, at the following address: https://www.easychair.org/conferences/?conf=els2018 Note: to help us with the review process please indicate the type of submission by entering either "paper", "demo", or "tutorial" in the Keywords field. Important dates: - 25 Feb 2018 Submission deadline (*** extended! ***) - 19 Mar 2018 Notification of acceptance - 25 Mar 2018 Early registration deadline - 02 Apr 2018 Final papers due - 16-17 Apr 2018 Symposium Programme chair: David Cooper, Genworks Intl., USA Local chairs: Andrew Lawson, Ravenpack, Spain Programme committee: Andy Wingo, Igalia, Spain Christophe Rhodes, Goldsmiths University, UK Christopher Wellons Null Program Canada Irène Durand, LaBRI, Université de Bordeaux, France Julian Padget, University of Bath, UK Ludovic Courtès, Inria, France Michael Sperber, DeinProgramm, Germany Nicolas Neuss, FAU Erlangen-Nürnberg, Germany Olin Shivers Northwestern University USA Philipp Marek, Austria Robert Strandh, LaBRI, Université de Bordeaux, France Sacha Chua Living an Awesome Life Canada Scott McKay, Future Fuel, USA Search Keywords: #els2018, ELS 2018, ELS '18, European Lisp Symposium 2018, European Lisp Symposium '18, 10th ELS, 10th European Lisp Symposium, European Lisp Conference 2018, European Lisp Conference '18 -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 0

[CfP] ELS 2018, April 16-17, Marbella, Spain
by Didier Verna 13 Feb '18

13 Feb '18

Reminder: submission deadline this sunday! ELS'18 - 11th European Lisp Symposium Centro Cultural Cortijo de Miraflores Marbella, Málaga Spain April 16-17 2018 Sponsored by Brunner Software GmbH and EPITA http://www.european-lisp-symposium.org/ The purpose of the European Lisp Symposium is to provide a forum for the discussion and dissemination of all aspects of design, implementation and application of any of the Lisp and Lisp-inspired dialects, including Common Lisp, Scheme, Emacs Lisp, AutoLisp, ISLISP, Dylan, Clojure, ACL2, ECMAScript, Racket, SKILL, Hop and so on. We encourage everyone interested in Lisp to participate. The 11th European Lisp Symposium invites high quality papers about novel research results, insights and lessons learned from practical applications and educational perspectives. We also encourage submissions about known ideas as long as they are presented in a new setting and/or in a highly elegant way. Topics include but are not limited to: - Context-, aspect-, domain-oriented and generative programming - Macro-, reflective-, meta- and/or rule-based development approaches - Language design and implementation - Language integration, inter-operation and deployment - Development methodologies, support and environments - Educational approaches and perspectives - Experience reports and case studies We invite submissions in the following forms: Papers: Technical papers of up to 8 pages that describe original results or explain known ideas in new and elegant ways. Demonstrations: Abstracts of up to 2 pages for demonstrations of tools, libraries, and applications. Tutorials: Abstracts of up to 4 pages for in-depth presentations about topics of special interest for at least 90 minutes and up to 180 minutes. The symposium will also provide slots for lightning talks, to be registered on-site every day. All submissions should be formatted following the ACM SIGS guidelines and include ACM Computing Classification System 2012 concepts and terms. Submissions should be uploaded to Easy Chair, at the following address: https://www.easychair.org/conferences/?conf=els2018 Note: to help us with the review process please indicate the type of submission by entering either "paper", "demo", or "tutorial" in the Keywords field. Important dates: - 18 Feb 2018 Submission deadline - 19 Mar 2018 Notification of acceptance - 25 Mar 2018 Early registration deadline - 02 Apr 2018 Final papers due - 16-17 Apr 2018 Symposium Programme chair: David Cooper, Genworks Intl., USA Local chairs: Andrew Lawson, Ravenpack, Spain Programme committee: Christophe Rhodes, Goldsmiths University, UK Christopher Wellons Null Program Canada Irène Durand, LaBRI, Université de Bordeaux, France Julian Padget, University of Bath, UK Ludovic Courtès, Inria, France Michael Sperber, DeinProgramm, Germany Nicolas Neuss, Universität Karlsruhe, Germany Olin Shivers Northwestern University USA Robert Strandh, LaBRI, Université de Bordeaux, France Sacha Chua Living an Awesome Life Canada Scott McKay, Future Fuel, USA Search Keywords: #els2018, ELS 2018, ELS '18, European Lisp Symposium 2018, European Lisp Symposium '18, 10th ELS, 10th European Lisp Symposium, European Lisp Conference 2018, European Lisp Conference '18 -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

1 0

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

Séminaire des étudiants CSI : Mercredi 24 janvier 2018 - Salle L7
by Daniela Becker 18 Jan '18

18 Jan '18

Bonjour, nous avons le plaisir de vous inviter au Séminaire des étudiants du LRDE. Il aura lieu le mercredi 24 janvier 2018 à partir de 14h00 en L7 au LRDE (KB). Les étudiants ING3 présenteront le résultat de leurs travaux des derniers mois. Au programme : SPOT — BIBLIOTHEQUE DE MODEL CHECKING 14h00 : Traduction efficace de formules LTL d’équité en automates déterministes – LAURENT XU En vérification formelle de la logique temporelle linéaire (LTL) à l’aide d’!-automates, la négation d’une formule LTL est traduite en !-automate. La construction d’un automate plus petit réduit beaucoup le temps d’exécution et la consommation mémoire des opérations suivantes de la chaîne de traitement de la vérification formelle. Müller et Sickert ont présenté une méthode efficace pour traduire n’importe quelle formule LTL en un petit automate déterministe. Cette méthode consiste à découper la formule en trois ensembles de sous-formules qui appartiennent respectivement au fragment de sureté ou de garantie, au fragment d’équité et au reste. Ils traduisent ensuite individuellement ces ensembles de sous-formules en automates déterministes qu’ils combinent par la suite. Spot peut déjà traduire les formules d’obligation en automates déterministes minimaux. Les formules d’obligation étant un surensemble des formules de sureté et de garantie, on généralise la traduction de Müller et Sickert en remplaçant le fragment de sureté ou de garantie par le fragment d’obligation. En ce qui concerne le fragment d’équité, ils ont présenté un algorithme de traduction efficace qui produit de petits automates déterministes. Ils ont également présenté comment construire efficacement un produit de ces automates avec d’autres automates. Nous présentons comment nous implémentons ces deux méthodes dans Spot. 14h30 : Tester l’appartenance à Persistence ou Récurrence dans Spot – ALEXANDRE GBAGUIDI AÏSSE Il existe une hiérarchie de propriétés temporelles, définie par Manna et Pnueli (1990). Cette hiérarchie contient entre autres les classes de récurrence et persistence. Savoir si une formule de logique temporelle à temps linéaire (LTL) f est récurrente (respectivement persistente) est intéressant car cela guarantit que f peut être traduit en un automate de Büchi déterministe (respectivement en un automate de co-Büchi). Auparavant, Spot, une bibliothèque de manipulation de formules LTL avait une unique façon de tester l’appartenance d’une formule aux classes de persistence ou récurrence. Grâce à nos précédents travaux présentés dans A co-Büching Toolbox, Spot a désormais deux façons de procéder. Nous avons comparé et amélioré ces deux méthodes en matière de temps d’exécution. 15h00 : Approches incrémentales pour la synthèse de contrôleur – THIBAUD MICHAUD Nous proposons deux approches incrémentales pour le problème de la synthèse de contrôleur à partir de spécifications en logique temporelle. Dans un travail antérieur, nous avons decrit notre implémentation d’un outil de synthèse de contrôleur reposant sur la réductibilité du problème à la résolution d’un jeu à parité, et avons établi que l’étape la plus coûteuse était la déterminisation d’un !-automate. Nous décrivons maintenant deux approches pour mitiger le problème : l’une est basée sur les automates good-for-games, et l’autre restreint les actions du contrôleur afin de simplifier la déterminisation. Nos expérimentations montrent que la deuxième approche est bien plus prometteuse que la première. Attention : le LRDE a déménagé, il se trouve au 24 rue Pasteur, 2e étage, au fond de la cour Pasteur (https://www.lrde.epita.fr/wiki/Contact) -- Daniela Becker Responsable administrative du LRDE

1 0

New Publication: "CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving"
by Colange Maximilien 05 Jan '18

05 Jan '18

We are happy to announce that the following article has been accepted for publication in the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18), to be held in Thessaloniki, Greece, from April 14th to April 20th 2018. "CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving" Hakan Metin (1), Souheib Baarir (1,2,3), Maximilien Colange (3), Fabrice Kordon (1) (1): Sorbonne Universités, UPMC, LIP6 CNRS UMR 7606, France (2): Université Paris Nanterre (3): LRDE, EPITA, Le Kremlin-Bicêtre, France Abstract: SAT solvers are now widely used to solve a large variety of problems, including formal verification of systems. SAT problems derived from such applications often exhibit symmetry properties that could be exploited to speed up their solving. /Static symmetry breaking /is so far the most popular approach to take advantage of symmetries. It relies on a symmetry preprocessor which augments the initial problem with constraints that force the solver to consider only a few configurations among the many symmetric ones. This paper presents a new way to handle symmetries, that avoids the main problem of the current static approaches: the prohibitive cost of the preprocessing phase. Extensive experiments on the benchmarks of last six SAT competitions show that our approach is competitive with the best state-of-the-art static symmetry breaking solutions. -- Maximilien Colange Assistant Professor LRDE -- EPITA (+33) 1 53 14 59 45

1 0

New journal publication: Derived-Term Automata of Multitape Expressions with Composition
by Akim Demaille 29 Dec '17

29 Dec '17

The Vcsn team is happy to announce that the following paper was accepted and published in Volume XXVII of the Scientific Annals of Computer Science. Derived-Term Automata of Multitape Expressions with Composition Akim Demaille EPITA/LRDE Rational expressions are powerful tools to define automata, but often restricted to single-tape automata. Our goal is to unleash their expressive power for transducers, and more generally, any multitape automaton; for instance (a⁺|x + b⁺|y)*. We generalize the construction of the derived-term automaton by using expansions. This approach generates small automata, and even allows us to support a composition operator. The paper on the Scientific Annals of Computer Science's website http://www.info.uaic.ro/bin/Annals/Article?v=XXVII2&a=1 For more information about this publication see http://publis.lrde.epita.fr/demaille.17.sacs To play with Vcsn on the topic of this paper http://vcsn-sandbox.lrde.epita.fr/notebooks/Doc/SACS-2017.ipynb Vcsn's home page http://vcsn.lrde.epita.fr

1 0