- 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

Paper accepted at TUG 2020
by Didier Verna 31 Mar '20

31 Mar '20

Hello, I'm happy to announce that the following paper has been accepted at TUG 2020, to be held (hopefully) this July in Rochester, USA. Title: Experimenting with Typesetting Algorithms, Interactively, and in Real-Time Abstract: In general, typesetting experimentation is not a very practical thing to do. WYSIWYG typesetting systems are very reactive but do not offer highly configurable algorithms, and TeX, with its separate development / compilation / visualization phases, is not as interactive as its WYSIWYG competitors. Being able to experiment with typesetting algorithms interactively and in real-time is nevertheless desirable, for instance for demonstration purposes, or for rapid prototyping, and debugging new ideas. We present ETAP (Experimental Typesetting Algorithms Platform), a tool written to ease the typesetting experimentation process. ETAP currently provides several paragraph justification algorithms, all with many configuration options such as kerning, ligatures, flexible spaces, sloppiness, hyphenation, etc. The resulting paragraph is displayed with many visual hints as well, such as paragraph, character, and line boxes, baselines, over/underfullness hints, etc. All those parameters, along with the desired paragraph width, are adjustable interactively through a GUI, and the resulting paragraph is displayed and updated in real-time. ETAP can also be used without the GUI, as a scriptable application. In particular, it is able to generate all sorts of statistical reports or charts on the behavior of the various algorithms, for instance, the number of over/underfull boxes per paragraph width, the average compression or stretch ratio per line, whatever else you want. This allows you to quickly demonstrate or evaluate the comparative behavior or merits of the provided algorithms, or whichever you may want to add to the pool. -- Resistance is futile. You will be jazzimilated. Jazz site: http://www.didierverna.com Other sites: http://www.didierverna.info

1 0

(sans objet)
by Didier Verna 29 Mar '20

29 Mar '20

Dear all, here is an update on the current situation of ELS 2020. 1. Given the evolution of the world-wide situation with regard to the COVID pandemic, it will come as no surprise that we have to cancel the Zurich event. 2. I have consequently closed the registrations, and I will proceed with full refunding this afternoon. 3. In the meantime, the reviewing process has continued as usual, and I'm happy to announce that thanks to the authors, the PC, and under the supervision of Ioanna, we now have a preliminary programme online! At least, this will already give you a taste of what we have this year. See http://www.european-lisp-symposium.org/. 4. A fallback solution is still under consideration, so stay tuned for updates. What I can tell you right now is this: a fully online event is very unlikely. More likely would be a semi-interactive online event, with the broadcasting of pre-recorded talks and a real-time channel for interaction. We have not completely ruled out the possibility of just postponing the physical event, but that solution is not very probable. Finally, if we go for an online event, I will make sure that it will be free and open for anyone to "attend". So, this is what I can tell you right now. Finally, I also want to extend my warmest thanks to all the persons who showed their support (notably financial, which is critical), by staying optimistic and registering anyway, hoping for the best. This means a lot. Stay safe! -- Resistance is futile. You will be jazzimilated. Jazz site: http://www.didierverna.com Other sites: http://www.didierverna.info

1 0

[Onward! Essays] COVID-19 update
by Didier Verna 21 Mar '20

21 Mar '20

Dear all, In view of the uncertainties around the COVID-19 pandemic, as an effort to relieve stress on authors: - The SPLASH conference has asked all co-located events to uniformly delay their paper submission deadlines. - The Onward! Essays track submission deadline has been shifted by one month, i.e., to May 23, 2020. The reviewing timeline has also been shifted accordingly. We are currently still planning to hold Onward! as part of SPLASH’20 in November in Chicago. Consult the SPLASH’20 home page for details and updates. Onward! is committed to timely publication of all accepted papers by the originally planned conference date. https://2020.splashcon.org/track/splash-2020-Onward-Essays -- Resistance is futile. You will be jazzimilated. Jazz site: http://www.didierverna.com Other sites: http://www.didierverna.info

1 0

TFM 1.1 "Carolingan Miniscules" is released
by Didier Verna 16 Mar '20

16 Mar '20

I'm happy to announce the release of TFM 1.1, a TeX Font Metrics parser library for Common Lisp. This release provides support for font scaling and freezing. Scaling is done, as in TeX, by overriding the font's design size, all other dimensions remaining relative to it. Freezing, on the other hand, converts all relative dimensions into absolute ones, potentially saving a lot of run-time arithmetic computation. Get it at the usual place: https://www.lrde.epita.fr/~didier/software/lisp/typesetting.php#tfm -- Resistance is futile. You will be jazzimilated. Jazz site: http://www.didierverna.com Other sites: http://www.didierverna.info

1 0

[Seminaire-LRDE] Séminaire du 18 Mars 2020 **Annulé**
by Nicolas BOUTRY 16 Mar '20

16 Mar '20

Bonjour à toutes et à tous, Au vu des circonstances, nous sommes dans l’obligation de reporter le séminaire de Stefan Schwoon à plus tard. Je vous présente toutes mes excuses pour la gène occasionnée. Bien cordialement, Nicolas Boutry _______________________________________________ seminaire mailing list seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

1 0

[Seminaire-LRDE] Mercredi 18 mars 2020: Stefan Schwoon, ENS Paris-Saclay
by Nicolas BOUTRY 08 Mar '20

08 Mar '20

Chers collègues, La prochaine session du séminaire Performance et Généricité du LRDE (Laboratoire de Recherche et Développement de l'EPITA) aura lieu le Mercredi 18 mars 2020 (11h -- 12h), Amphi Masters. Vous trouverez sur le site du séminaire [1] les prochaines séances, les résumés, captations vidéos et planches des exposés précédents [2], le détail de cette séance [3] ainsi que le plan d'accès [4]. [1] http://seminaire.lrde.epita.fr [2] http://seminaire.lrde.epita.fr/Archives [3] http://seminaire.lrde.epita.fr/2020-03-18 [4] http://www.lrde.epita.fr/wiki/Contact Au programme du Mercredi 18 mars 2020 : * 11h -- 12h: Diagnosis and Opacity in Partially Observable Systems -- Stefan Schwoon, ENS Paris-Saclay http://www.lsv.fr/~schwoon/ In a partially observable system, diagnosis is the task of detecting the certain events, for instance fault occurrences. In the presence of hostile observers, on the other hand, one is interested in rendering a system opaque, i.e. making it impossible to detect certain "secret" events. The talk will present some decidability and complexity results for these two problems when the system is represented as a finite automaton or a Petri net. We then also consider the problem of active diagnosis, where the observer has some control over the system. In this context, we study problems such as the computational complexity of the synthesis problem, the memory required for the controller, and the delay between a fault occurrence and its detection by the diagnoser. The talk is based on joint work with B.Bérard, S.Haar, S.Haddad, T.Melliti, and S.Schmitz. -- Stefan Schwoon studied Computer Science at the University of Hildesheim and received a PhD from the Technical University of Munich in 2002. He held the position of Scientific Assistent at the University of Stuttgart from 2002 to 2007, and at the Technical University in Munich from 2007 to 2009. He is currently Associate Professor (Maître de conférences) in the Laboratoire Spécification et Vérification (LSV), ENS Paris-Saclay, and a member of the INRIA team Mexico. His research interests include model checking and diagnosis on concurrent and partially-observable systems. L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette information le plus largement possible. N'hésitez pas à nous faire parvenir vos suggestions d'orateurs. -------------- section suivante -------------- Une pièce jointe HTML a été nettoyée... URL: <http://lists.lrde.epita.fr/pipermail/seminaire/attachments/20200308/89850cb…> _______________________________________________ seminaire mailing list seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

1 0

[Seminaire-LRDE] Mercredi 18 mars 2020: Stefan Schwoon, ENS Paris-Saclay
by Nicolas BOUTRY 08 Mar '20

08 Mar '20

Chers collègues, La prochaine session du séminaire Performance et Généricité du LRDE (Laboratoire de Recherche et Développement de l'EPITA) aura lieu le Mercredi 18 mars 2020 (11h -- 12h), Amphi Masters. Vous trouverez sur le site du séminaire [1] les prochaines séances, les résumés, captations vidéos et planches des exposés précédents [2], le détail de cette séance [3] ainsi que le plan d'accès [4]. [1] http://seminaire.lrde.epita.fr [2] http://seminaire.lrde.epita.fr/Archives [3] http://seminaire.lrde.epita.fr/2020-03-18 [4] http://www.lrde.epita.fr/wiki/Contact Au programme du Mercredi 18 mars 2020 : * 11h -- 12h: Diagnosis and Opacity in Partially Observable Systems -- Stefan Schwoon, ENS Paris-Saclay http://www.lsv.fr/~schwoon/ In a partially observable system, diagnosis is the task of detecting the certain events, for instance fault occurrences. In the presence of hostile observers, on the other hand, one is interested in rendering a system opaque, i.e. making it impossible to detect certain "secret" events. The talk will present some decidability and complexity results for these two problems when the system is represented as a finite automaton or a Petri net. We then also consider the problem of active diagnosis, where the observer has some control over the system. In this context, we study problems such as the computational complexity of the synthesis problem, the memory required for the controller, and the delay between a fault occurrence and its detection by the diagnoser. The talk is based on joint work with B.Bérard, S.Haar, S.Haddad, T.Melliti, and S.Schmitz. -- Stefan Schwoon studied Computer Science at the University of Hildesheim and received a PhD from the Technical University of Munich in 2002. He held the position of Scientific Assistent at the University of Stuttgart from 2002 to 2007, and at the Technical University in Munich from 2007 to 2009. He is currently Associate Professor (Maître de conférences) in the Laboratoire Spécification et Vérification (LSV), ENS Paris-Saclay, and a member of the INRIA team Mexico. His research interests include model checking and diagnosis on concurrent and partially-observable systems. L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette information le plus largement possible. N'hésitez pas à nous faire parvenir vos suggestions d'orateurs. _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

1 0