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
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
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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
