April 2020 - Annonce

Spot 2.9 released
by Alexandre Duret-Lutz 30 Apr '20

30 Apr '20

We are happy to announce the release of Spot 2.9 Spot is a library of algorithms for manipulating LTL formulas and omega-automata. This is a major release that has been under development for 9 months. It contains new features contributed by from Florian Renkin and myself. A summary of those changes is given at the end of this email. Note that version 2.9 and the following 2.9.x minor releases are likely to be the last releases using C++14. We plan is to switch to C++17 for the next major release. The current code-base is already compatible with C++17, so tools using Spot as a library may consider switching to C++17 already. You can find the new release here: http://www.lrde.epita.fr/dload/spot/spot-2.9.tar.gz See https://spot.lrde.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot(a)lrde.epita.fr>. New in spot 2.9 (2020-04-30) Command-line tools: - When the --check=stutter-sensitive-example option is passed to tools like ltl2tgba, autfilt, genaut, or ltldo, the produced automata are checked for stutter-invariance (as in the --check=stutter-invariant case), additionally a proof of stutter-sensitiveness is provided as two stutter-equivalent words: one accepted, and one rejected. These sample words are printed in the HOA output. % ltl2tgba --check=stutter-sensitive-example Xa | grep word: spot-accepted-word: "!a; cycle{a}" spot-rejected-word: "!a; !a; cycle{a}" - autfilt learned the --partial-degeneralize option, to remove conjunctions of Inf, or disjunctions of Fin that appears in arbitrary conditions. - ltlfilt and autfilt learned a --nth=RANGE (a.k.a. -N) option to select a range of their input formulas or automata (assuming a 1-based numbering). - When running translators, ltlcross will now display {names} when supplied. - ltlcross is now using the generic emptiness check procedure introduced in Spot 2.7, as opposed to removing Fin acceptance before using a classical emptiness check. - ltlcross learned a --save-inclusion-products=FILENAME option. Its use cases are probably quite limited. We use that to generate benchmarks for our generic emptiness check procedure. - ltlsynt --algo=lar uses the new version of to_parity() mentionned below. The old version is available via --algo=lar.old - ltlsynt learned --csv=FILENAME, to record some statistics about the duration of its different phases. - The dot printer is now automatically using rectangles with rounded corners for automata states if one state label have five or more characters. This saves space with very long labels. Use --dot=c, --dot=e, or --dot=E to force the use of Circles, Ellipses, or rEctangles. Library: - Historically, Spot only supports LTL with infinite semantics so it had automatic simplifications reducing X(1) and X(0) to 1 and 0 whenever such formulas are constructed. This caused issues for users of LTLf formulas, where it is important to distinguish a "weak next" (for which X(1)=1 but X(0)!=0) from a "strong next" (for which X(0)=0 but X(1)!=1). To accommodate this, this version introduces a new operator op::strong_X in addition to the existing op::X (whose interpretation is now weak in LTLf). The syntax for the strong next is X[!] as a reference to the PSL syntax (where the strong next is written X!). Trivial simplification rules for X are changed to just X(1) = 1 (and not X(0)=0 anymore) while we have X[!]0 = 0 The X(0)=0 and X[!]1=1 reductions are now preformed during LTL simplification, not automatically. Aside from the from_ltlf() function, the other functions of the library handle X and X[!] in the same way, since there is no difference between X and X[!] over infinite words. Operators F[n:m!] and G[n:m!] are also supported as strong variants of F[n:m] and G[n:m], but those four are only implemented as syntactic sugar. - acc_cond::acc_code::parity(bool, bool, int) was not very readable, as it was unclear to the reader what the boolean argument meant. The following sister functions can now improve readability: parity_max(is_odd, n) = parity(true, is_odd, n) parity_max_odd(n) = parity_max(true, n) parity_max_even(n) = parity_max(false, n) parity_min(is_odd, n) = parity(false, is_odd, n) parity_min_odd(n) = parity_min(true, n) parity_min_even(n) = parity_min(false, n) - partial_degeneralize() is a new function performing partial degeneralization to get rid of conjunctions of Inf terms, or disjunctions of Fin terms in acceptance conditions. - simplify_acceptance_here() and simplify_acceptance() learned to simplify subformulas like Fin(i)&Fin(j) or Inf(i)|Inf(j), or some more complex variants of those. If i is uniquely used in the acceptance condition, these become respectively Fin(i) or Inf(i), and the automaton is adjusted so that i also appears where j appeared. - acc_code::unit_propagation() is a new method for performing unit propagation in acceptance condition. E.g. Fin(0) | (Inf(0) & Inf(1)) becomes Fin(0) | Inf(1). This is now called by simplify_acceptance_here(). - propagate_marks_vector() and propagate_marks_here() are helper functions for propagating marks on the automaton: ignoring self-loops and out-of-SCC transitions, marks common to all the input transitions of a state can be pushed to all its outgoing transitions, and vice-versa. This is repeated until a fix point is reached. propagate_marks_vector() does not modify the automaton and returns a vector of the acc_cond::mark_t that should be on each transition; propagate_marks_here() actually modifies the automaton. - rabin_to_buchi_if_realizable() is a new variant of rabin_to_buchi_maybe() that converts a Rabin-like automaton into a Büchi automaton only if the resulting Büchi automaton can keep the same transition structure (where the ..._maybe() variant would modify the Rabin automaton if needed). - to_parity() has been rewritten. It now combines several strategies for paritizing automata with any acceptance condition. - relabel_bse(), used by ltlfilt --relabel-bool, is now better at dealing with n-ary operators and isolating subsets of operands that can be relabeled as a single term. - print_dot()'s default was changed to use circles for automata with fewer than 10 unamed states, ellipses for automata with up to 1000 unamed states (or named states with up to 4 characters), and rounded rectangles otherwise. Rectangles are also used for automata with acceptance bullets on states. The new "E" option can be used to force rectangles in all situations. - The generic emptiness check has been slightly improved (doing fewer recursive calls in the worst case). Backward-incompatible changes: - iar() and iar_maybe() have been moved from spot/twaalgos/rabin2parity.hh spot/twaalgos/toparity.hh and marked as deprecated, they should be replaced by to_parity(). In case the input is Rabin-like or Streett-like, to_parity() should be at least as good as iar(). - The twa_graph::is_alternating() and digraph::is_alternating() methods, deprecated in Spot 2.3.1 (2017-02-20), have been removed. Bugs fixed: - Relabeling automata could introduce false edges. Those are now removed. - Emptiness checks, and scc_info should now ignore edges labeled with false. - relabel_bse() could incorrectly relabel Boolean subformulas that had some atomic propositions in common. -- Alexandre Duret-Lutz

1 0

[CfP] Reminder: Onward! Essays / SPLASH 2020, Nov. 15-20, Chicago.
by Didier Verna 22 Apr '20

22 Apr '20

Onward! Essays 2020 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software Renaissance Chicago Downtown Hotel Chicago, USA November 15--20 2020 Part of SPLASH 2020 Systems, Programming Languages and Applications: Software for Humanity https://2020.splashcon.org/track/splash-2020-Onward-essays Onward! is a premier multidisciplinary conference focused on everything to do with programming and software: including processes, methods, languages, communities, applications and education. Compared to other conferences, Onward! is more radical, more visionary, and more open to ideas that are well-argued but not yet proven. It is not looking for research-as-usual papers. To allow room for bigger, bolder and/or less mature ideas, it accepts less exact methods of validation, such as compelling arguments, exploratory implementations, and substantial examples. Onward! Essays is looking for clear and compelling pieces of writing about topics important to the software community (there is also a parallel Papers track with a seperate announcement). An essay can be an exploration of the topic and its impact, or a story about the circumstances of its creation; it can present a personal view of what is, explore a terrain, or lead the reader in an act of discovery; it can be a philosophical digression or a deep analysis. It can describe a personal journey, perhaps the one the author took to reach an understanding of the topic. The subject area—software, programming, and programming languages—should be interpreted broadly and can include the relationship of software to human endeavors, or its philosophical, sociological, psychological, historical, or anthropological underpinnings. Format and Selection: Onward! essays must describe unpublished work that is not currently submitted for publication elsewhere as described by SIGPLAN's Republication Policy. Submitters should also be aware of ACM's Policy and Procedures on Plagiarism. Onward! essays should use the ACM SIGPLAN Conference acmart format. Please refer to the conference's website above for full details. The Onward! Essays track follows a two-phase review process. Essays are peer-reviewed in a single-blind manner. Accepted essays will appear in the Onward! Proceedings in the ACM Digital Library, and must be presented at the conference. Submissions will be judged on the potential impact of the ideas and the quality of the presentation. Important dates: All deadlines are midnight, anywhere on Earth. Essay submission: 23 Mai (#COVID19 extended by one month!) First-round notification: 11 June Second-round submission: 15 July Final notification: 30 July Conference: 18--20 November Programme Committee: Didier Verna, EPITA Research lab, France (Program Chair) Anya Helene Bagge, University of Bergen, Norway Alexandre Bergel, University of Chile Jean Bresson, Ableton, Germany Maxime Chevalier-Boisvert, Université de Montréal, Québec Elisa Gonzalez Boix, Vrije Universiteit Brussel, Belgium Hidehiko Masuhara, Tokyo Institute of Technology, Japan Kent Pitman, PTC, USA Donya Quick, Stevens Institute of Technology, USA Gordana Rakić, University of Novi Sad, Serbia -- Resistance is futile. You will be jazzimilated. Jazz site: http://www.didierverna.com Other sites: http://www.didierverna.info

1 0

[CfPart] 13th European Lisp Symposium, happening online, free of charge!
by Didier Verna 14 Apr '20

14 Apr '20

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 13th European Lisp Symposium Special Focus on Compilers In cooperation with: ACM SIGPLAN Call for participation April 27 - April 28, 2020 Sponsored by EPITA, Igalia S.L., and RavenPack ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ #COVID19 important information ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In the context of the current pandemic, the symposium has been turned into an online event, and will be open to anyone, free of charge! Connection instructions will be posted on the website when available. Invited Speakers ~~~~~~~~~~~~~~~~ Andrew W. Keep (Cisco Systems, Inc.), on the Nanopass Framework. Daniel Kochmański (Turtleware), on ECL, the Embeddable Common Lisp. Scope ~~~~~ 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 dialects, including Common Lisp, Scheme, Emacs Lisp, Clojure, Racket, ACL2, AutoLisp, ISLISP, Dylan, ECMAScript, SKILL and so on. We encourage everyone interested in Lisp to participate. This year's focus is directed towards "Compilers". Programme Chair ~~~~~~~~~~~~~~~ Ioanna M. Dimitriou H. - Igalia, Spain/Germany Local Chair ~~~~~~~~~~~ Nicolas Hafner - Shinmera, Switzerland Programme Committee ~~~~~~~~~~~~~~~~~~~ Andy Wingo - Igalia, Spain/France Asumu Takikawa - Igalia, Spain/USA Charlotte Herzeel - Imec, ExaScience Lab, Belgium Christophe Rhodes - Google, UK Irène Durand - Université Bordeaux 1, France Jim Newton - EPITA Research Lab, France Kent Pitman - HyperMeta, USA Leonie Dreschler-Fischer - University of Hamburg, Germany Marco Heisig - FAU Erlangen-Nürnberg, Germany Mark Evenson - not.org, Austria Max Rottenkolber - Interstellar Ventures, Germany Metin Evrim Ulu - Middle East Technical University, Turkey Paulo Matos - Igalia, Spain/Germany Robert Goldman - SIFT, USA Robert Strandh - Université Bordeaux 1, France Sky Hester - consultant, USA -- Resistance is futile. You will be jazzimilated. Jazz site: http://www.didierverna.com Other sites: http://www.didierverna.info

1 0