From 78fd7beaaff74b33e5a6c62a9371cc2d94757ffa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 21 Jan 2016 18:58:46 +0100 Subject: [PATCH] org: Add a Concepts page. * doc/org/concepts.org: New file. * doc/Makefile.am: Add it. * doc/org/oaut.org: Add anchor. * doc/org/index.org, doc/org/tut.org: Add links to concepts.org. * doc/org/spot.css: Set up boxes for implementation details. * NEWS: Mention the new page. --- NEWS | 6 +- doc/Makefile.am | 5 +- doc/org/concepts.org | 960 +++++++++++++++++++++++++++++++++++++++++++ doc/org/index.org | 11 +- doc/org/oaut.org | 3 + doc/org/spot.css | 2 + doc/org/tut.org | 3 + 7 files changed, 982 insertions(+), 8 deletions(-) create mode 100644 doc/org/concepts.org diff --git a/NEWS b/NEWS index 4970e44ea..05d9152ed 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,10 @@ New in spot 1.99.7a (not yet released) - Nothing yet. + Documentation: + + * There is a new page giving informal illustrations (and extra + pointers) for some concepts used in Spot. + See https://spot.lrde.epita.fr/concepts.html New in spot 1.99.7 (2016-01-15) diff --git a/doc/Makefile.am b/doc/Makefile.am index 7ce54e920..fc597501b 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2010, 2011, 2013, 2014, 2015 Laboratoire de Recherche et -## Développement de l'Epita (LRDE). +## Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016 Laboratoire de +## Recherche et Développement de l'Epita (LRDE). ## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris ## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ## Université Pierre et Marie Curie. @@ -68,6 +68,7 @@ ORG_FILES = \ org/autfilt.org \ org/csv.org \ org/compile.org \ + org/concepts.org \ org/dstar2tgba.org \ org/genltl.org \ org/hoa.org \ diff --git a/doc/org/concepts.org b/doc/org/concepts.org new file mode 100644 index 000000000..dffe90cf6 --- /dev/null +++ b/doc/org/concepts.org @@ -0,0 +1,960 @@ +# -*- coding: utf-8 -*- +#+TITLE: Concepts +#+SETUPFILE: setup.org +#+HTML_LINK_UP: index.html + +This page documents some of the concepts used in Spot, and whose +knowledge is usually assumed throughout the documentation. The +presentation is informal on purpose. + +* Atomic proposition (AP) + :PROPERTIES: + :CUSTOM_ID: ap + :END: + +An /atomic proposition/ is a named Boolean variable that represents a +simple property that must be true or false. It usually represents +some property of a system. For instance =light_on= and =door_open= +could be the names of two atomic propositions that are respectively +true if the light is on and the door open, and false otherwise. + +Atomic propositions are used to construct temporal logic formulas (see +below) to specify properties of the system: for instance we might want +to state that /whenever the the door is open, the light should be on/. +We could write that as the [[#ltl][LTL formula]] =G(door_open -> light_on)= in +which =G= is a temporal operator that means /always/. + +Atomic propositions are also used to form the [[#boolean][Boolean formulas]] that +label the edges of automata. + +* Boolean formula + :PROPERTIES: + :CUSTOM_ID: boolean + :END: + +A /Boolean formula/ is formed from [[#ap][atomic propositions]], the Boolean +constants true and false, and standard Boolean operators like /and/, +/or/, /implies/, /xor/, etc. + +* Binary Decision Diagrams (BDD) + :PROPERTIES: + :CUSTOM_ID: bdd + :END: + +A Binary Decision Diagram is a data structure for efficient +manipulation of [[#boolean][Boolean formulas]]. + +BDDs correspond to a kind of /if-then-else normal form/ for Boolean +formulas. If we fix the order in which the atomic propositions will +be tested, that normal form is unique. BDDs are stored as directed +acyclic graphs with sharing of subformulas. + +For further information about BDDs, read for instance [[http://configit.com/configit_wordpress/wp-content/uploads/2013/07/bdd-eap.pdf][Henrik Reif +Andersen's lecture notes]]. + +In Spot, BDDs are one way to represent Boolean formulas, and in +particular, they are used to labels the edges of [[#buchi][automata]]. Spot uses a +customized version of [[http://sourceforge.net/projects/buddy/][the BuDDy library]] for manipulating BDDs. + +* ω-word + :PROPERTIES: + :CUSTOM_ID: word + :END: + +An ω-word (omega-word) is a word of infinite length. In our context, +each letter is used to describe the state of a system at a given time, +and the sequence of letters shows the evolution of the system as the +(discrete) time is incremented. + +If the set $AP$ of [[#ap][atomic propositions]] is fixed, an ω-word over $AP$ +is an infinite sequence of subsets of $AP$. In other words, there are +$2^{|AP|}$ possible letters to choose from, and these letters denote +the set of atomic propositions that are true at a given instant. + +For instance if $AP=\{a,b,c\}$, the infinite sequence +\[\{a,b\};\{a\};\{a,b\};\{a\};\{a,b\};\{a\};\ldots\] is an example of +ω-word over $AP$. This particular ω-word can be interpreted as the +following scenario: atomic proposition $a$ is always true, $b$ is true +at each other instant, and $c$ is always false. + +Note that instead of using sets of atomic propositions, it is equivalent +to write that word using [[https://en.wikipedia.org/wiki/Canonical_normal_form#Minterms][minterms]] over $AP$: +\[(a\land b\land \bar c);(a\land \bar b\land \bar c); + (a\land b\land \bar c);(a\land \bar b\land \bar c); + (a\land b\land \bar c);(a\land \bar b\land \bar c);\ldots\] + +* ω-Automaton + :PROPERTIES: + :CUSTOM_ID: automaton + :END: + +An ω-automaton is used to represent sets of ω-word. + +Those look like the classical [[https://en.wikipedia.org/wiki/Nondeterministic_finite_automaton][Nondeterministic Finite Automata]] in the +sense that they also have states and transitions. However ω-automata +recognize [[#word][ω-words]] instead of finite words. In this context, the +notion of /final state/ makes no sense, and is replaced by the notion +of [[#acceptance-condition][acceptance condition]]: a run of the automaton (i.e., an infinite +sequence alternating states and edges in a way that is compatible with +the structure of the automaton) is /accepting/ if it satisfies the +constraint given by the acceptance condition. + +In Spot, ω-automata have their edges labeled by [[#boolean][Boolean formulas]] +represented using [[#bdd][BDDs]]. An ω-word is accepted by an ω-automaton if +there exists an accepting run whose labels (those Boolean formulas) +are compatible with the minterms used as letters in the word. + +The /language/ of an automaton is the set of ω-words it accepts. + +There are many kinds of ω-Automata and they mostly differ by their +[[#acceptance-condition][acceptance condition]]. The different types of acceptance condition, +and whether the automata are deterministic or can affect their +expressive power. + +One of the simplest and most common type of ω-Automata is the [[#buchi][Büchi +automaton]] described next. + +* Büchi automaton + :PROPERTIES: + :CUSTOM_ID: buchi + :END: + +A Büchi automaton is a simple kind of [[#automaton][ω-Automaton]] in which a run is +accepting iff it visits some /accepting state/ infinitely often. +Those accepting states are often denoted using a double circle. + +For instance here is a Büchi automaton that accepts only words in +which $a$ is always true, and $b$ is true infinitely often. + +#+NAME: buchi-example1 +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba 'G(a) & GF(b)' -B -d +#+END_SRC + +#+BEGIN_SRC dot :file concept-buchi1.png :cmdline -Tpng :var txt=buchi-example1 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:concept-buchi1.png]] + + +The above automaton would accept the [[#word][ω-word we used previously as an +example]]. + + +As a more concrete example, here is a (complete) Büchi automaton for +the [[#ltl][LTL formula]] =G(door_open -> light_on)= that specifies that +=light_on= should be true whenever =door_open= is true. + +#+NAME: buchi-example2 +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba 'G(door_open -> light_on)' -d -C +#+END_SRC + +#+BEGIN_SRC dot :file concept-buchi2.png :cmdline -Tpng :var txt=buchi-example2 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:concept-buchi.png]] + +The =1= displayed on the edge that loops on state =1= should be +read as /true/, i.e., the Boolean formula that accepts +any valuation of the atomic propositions. + +The above automaton is complete: any possible ω-word over +$AP=\{\mathit{door\_open}, \mathit{light\_on}\}$ is recognized by some +run. But not all those runs are accepting. In fact, there is only one +run that is accepting: the one that loops continuously on state 0. + +All the remaining runs eventually reach state 1 and stay there. Those +runs recognize scenarios where at some point the door is open and the +light is off. There is an infinite number of those runs: they differ +by the number of times they loop on state 0. But since those runs +reach state 1, it means they visited state 0 only a finite number of +times, so they do not validate the acceptance condition. + + +There can be multiple accepting states, but it is enough to visit one +infinitely often. For instance the following Büchi automaton accept +all runs in which at all point $a$ is true iff $b$ is true at the next +instant. + +#+NAME: buchi-example3 +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba 'G(a <-> Xb)' -B -d +#+END_SRC +#+BEGIN_SRC dot :file concept-buchi3.png :cmdline -Tpng :var txt=buchi-example3 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:concept-buchi3.png]] + +* Transitions vs. Edges + :PROPERTIES: + :CUSTOM_ID: trans-edge + :END: + +Since automata are labeled by Boolean formulas instead of letters it +is sometimes useful to think of the formula-labeled *edges* of an +automaton as a way to aggregate several letter-labeled *transitions*. + +Whenever the distinction is important, for instance when giving the +size of an automaton, we use the terms *edge* and *transition* to +distinguish whether we are looking at the automaton as a graph, or +whether we are actually considering all possible letters that may +have been aggregated in an edge. + +Here is a simple example: +#+NAME: te1 +#+BEGIN_SRC sh :results verbatim :exports none +cat >concept-te.hoa < tmp.$$ +ltl2tgba -s6 'p0 | GFp1' | pr -m -t tmp.$$ - +#+END_SRC + +#+RESULTS: +#+begin_example +never { /* p0 | GFp1 */ never { /* p0 | GFp1 */ +T0_init: T0_init: + if do + :: (p0) -> goto accept_all :: atomic { (p0) -> assert(!(p0)) + :: (!(p0)) -> goto accept_S2 :: (!(p0)) -> goto accept_S2 + fi; od; +accept_S2: accept_S2: + if do + :: (p1) -> goto accept_S2 :: (p1) -> goto accept_S2 + :: (!(p1)) -> goto T0_S3 :: (!(p1)) -> goto T0_S3 + fi; od; +T0_S3: T0_S3: + if do + :: (p1) -> goto accept_S2 :: (p1) -> goto accept_S2 + :: (!(p1)) -> goto T0_S3 :: (!(p1)) -> goto T0_S3 + fi; od; +accept_all: accept_all: + skip skip +} } +#+end_example + +#+NAME: never-ex1 +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba -Bd 'p0 | GFp1' +#+END_SRC +#+BEGIN_SRC dot :file concept-never1.png :cmdline -Tpng :var txt=never-ex1 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:concept-never1.png]] + +The two different types of never claims differ only in a few syntactic +elements: =do..od= instead of =if..fi=, =assert= instead of =goto +accept_all=, etc. Older Spin releases used to output the first one, while +newer Spin releases (starting with Spin 6.2.4) use the second syntax +as they help Spin to produce more precise counterexamples. + +Spot can read and write never claims in both syntaxes, but it cannot +parse never claim that use other features (such as variables) of the +Promela language. + +* LBTT's format + :PROPERTIES: + :CUSTOM_ID: lbtt + :END: + +This format was originally introduced by [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][LBT]], a tool for translating +LTL to (state-based) generalized Büchi automata, and then used by +[[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], a tool for testing LTL-to-Büchi translators. + +For instance the Büchi automaton we used as an example for never +claims can be encoded as follows: + +#+BEGIN_SRC sh :results verbatim :exports results +ltl2tgba --ba --lbtt 'p0 | GFp1' +#+END_SRC + +#+RESULTS: +#+begin_example +4 1 +0 1 -1 +1 p0 +2 ! p0 +-1 +1 0 0 -1 +1 t +-1 +2 0 0 -1 +2 p1 +3 ! p1 +-1 +3 0 -1 +2 p1 +3 ! p1 +-1 +#+end_example + +[[file:concept-never1.png]] + +The format has been extended in two ways. First, LBTT extended it to +support transition-based acceptance. This is indicated by a =t= on +the first line: + +#+BEGIN_SRC sh :results verbatim :exports results +ltl2tgba --lbtt 'p0 | GFp1' +#+END_SRC + +#+RESULTS: +#+begin_example +3 1t +0 1 +1 -1 p0 +2 -1 ! p0 +-1 +1 0 +1 0 -1 t +-1 +2 0 +2 0 -1 p1 +2 -1 ! p1 +-1 +#+end_example + +#+NAME: lbtt-ex2 +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba -d 'p0 | GFp1' +#+END_SRC +#+BEGIN_SRC dot :file concept-lbtt2.png :cmdline -Tpng :var txt=lbtt-ex2 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:concept-lbtt2.png]] + +We call this format the LBTT format because of this extension. + +A second, but independent extension, was done in [[http://ltl2dstar.de/][=ltl2dstar=]], allowing +atomic propositions that are different from =p0=, =p1=, =p2=, etc. + +Both extensions are supported by Spot. + +* DSTAR format + :PROPERTIES: + :CUSTOM_ID: dstar + :END: + +The DSTAR format is the native format of [[http://ltl2dstar.de/][=ltl2dstar=]]. It allows +representing Deterministic STreett And Rabin automata, hence the +name. + +Spot can read the DSTAR format, but it does not output it. Adding +output for this format would not be difficult, but it would also not +be very useful: for all intents and purposes, the [[#hoa][HOA]] format should be +preferred. =ltl2dstar= can now also output HOA directly. + +Here is one Rabin automaton in the DSTAR format: + +#+BEGIN_SRC sh :results verbatim :exports results +echo '| F G p0 G F p1' | ltl2dstar --output-format=native - - +#+END_SRC + +#+RESULTS: +#+begin_example +DRA v2 explicit +Comment: "Union{Safra[NBA=2],Safra[NBA=2]}" +States: 4 +Acceptance-Pairs: 2 +Start: 0 +AP: 2 "p0" "p1" +--- +State: 0 +Acc-Sig: -0 +0 +1 +2 +3 +State: 1 +Acc-Sig: +0 +0 +1 +2 +3 +State: 2 +Acc-Sig: -0 +1 +0 +1 +2 +3 +State: 3 +Acc-Sig: +0 +1 +0 +1 +2 +3 +#+end_example + +#+NAME: dstar-example1 +#+BEGIN_SRC sh :results verbatim :exports none +echo '| F G p0 G F p1' | ltl2dstar --output-format=native - - | autfilt -d.a +#+END_SRC +#+BEGIN_SRC dot :file concept-dstar.png :cmdline -Tpng :var txt=dstar-example1 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:concept-dstar.png]] + + +* Hanoi Omega-Automaton format (HOA) + :PROPERTIES: + :CUSTOM_ID: hoa + :END: + +The [[http://adl.github.io/hoaf/][HOA format]] inherits several features from the [[:dstar][DSTAR format]], but +extends it in many ways, including support for non-deterministic +automata and for arbitrary acceptance conditions. + +#+BEGIN_SRC sh :results verbatim :exports results +ltldo ltl2dstar -f 'FGp0 | GFp1' --name=%f +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +name: "FGp0 | GFp1" +States: 4 +Start: 0 +AP: 2 "p0" "p1" +acc-name: Rabin 2 +Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 {0} +[!0&!1] 0 +[0&!1] 1 +[!0&1] 2 +[0&1] 3 +State: 1 {1} +[!0&!1] 0 +[0&!1] 1 +[!0&1] 2 +[0&1] 3 +State: 2 {0 3} +[!0&!1] 0 +[0&!1] 1 +[!0&1] 2 +[0&1] 3 +State: 3 {1 3} +[!0&!1] 0 +[0&!1] 1 +[!0&1] 2 +[0&1] 3 +--END-- +#+end_example + +#+NAME: hoa1 +#+BEGIN_SRC sh :results verbatim :exports none +ltldo ltl2dstar -f 'FGp0 | GFp1' -d.a +#+END_SRC +#+BEGIN_SRC dot :file concept-hoa.png :cmdline -Tpng :var txt=hoa1 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:concept-hoa.png]] + + +Since this file format is the only one able to represent the range of +ω-automata supported by Spot, and it its default output format. + +However note that Spot does not (yet?) support all automata that can +be expressed using the HOA format. For instance it has no support for +alternating automata, or for the =Alphabet:=-based automata introduced +in v1.1 of HOA (only =AP:=-based automata are supported). + +The present support for the HOA format in Spot, is discussed on [[file:hoa.org][a +separate page]]. + +* Linear-time Temporal Logic (LTL) + :PROPERTIES: + :CUSTOM_ID: ltl + :END: + +The Linear-time Temporal Logic (LTL) extends propositional logic with +operators that refer to the future. Some definitions of LTL also +include past operators, but Spot only supports future operators. The +view of the time is discrete: a scenario can be seen as a succession +of steps in which each [[#ap][atomic proposition]] can have a different value. + +The following basic operators are supported: + +| LTL formula | meaning | +|-------------+------------------------------------------------------------------------------------------------| +| =f= | the formula =f= is true immediately | +| =X f= | =f= will be true in the next step | +| =F f= | =f= will become true eventually (it could be true immediately, or on the future) | +| =G f= | =f= is always true from now on | +| =f U g= | =f= has to be true until =g= becomes true (and =g= /will/ become true) | +| =f W g= | =f= has to be true until =g= becomes true (=f= should stay true if =g= never becomes true) | +| =f R g= | =g= has to be true until =f&g= becomes true (=g= should stay true if =f&g= never becomes true) | +| =f M g= | =g= has to be true until =f&g= becomes true (and =f&g= /will/ become true) | + +For instance the LTL formula =G(request -> F(response))= specifies that +whenever =request= atomic proposition is true, there exists a later +instant (possibly the same) where =response= is true. + +Spot supports [[file:ioltl.org][several syntaxes for writing LTL formulas]]. For example +some people prefer to write =<>= and =[]= instead of =F= and =G=, =R= +is written =V= in some tools, etc. + +For more discussion about the temporal operators and their semantics, +see the [[https://spot.lrde.epita.fr/tl.pdf][tl.pdf]] document. + +* Property Specification Language (PSL) + :PROPERTIES: + :CUSTOM_ID: psl + :END: + +Spot supports the linear fragment of PSL, this basically extends LTL +with semi-extended regular expressions. Those regular expressions can +express finite languages and PSL introduces operators to use these +finite languages as a prefix of a PSL formula. + +| PSL formula | meaning | +|--------------+-------------------------------------------------------------------------| +| ={e}<>->f | =f= should hold on the last instant of some one prefix that matches =e= | +| ={e}[]->f | =f= should hold on the last instant of all prefixes that match =e= | + +In the above table =e= is a semi-extended expression, and =f= is a PSL (or LTL) formula. + +Semi-extended regular expressions can be formed using Boolean +expressions over [[#ap][atomic propositions]] and the following +operators: + +| SERE | meaning | +|--------------------+-----------------------------------------------------------------------------------| +| =e1;e2= | =e1= followed by =e2= (concatenation) | +| =e1:e2= | =e1= fused with =e2=: =e2= has to start matching on the last letter matching =e1= | +| =e1 \vert\vert e2= | =e1= or =e2= have to match (union) | +| =e1 && e2= | =e1= and =e2= have to match (intersection) | +| =e1 & e2= | =e2= should match a prefix of what =e1= matches, or vice-versa | +| =e[*]= | =e= should be matched a finite number of times (Kleene star) | +| =e[*2..3]= | same as =(e;e)\vert\vert(e;e;e)= | +| =e[+]= | =e= should be matched a finite number of times, and at least once | + + +For example the formula ={(1;1)[*]}[]->a= can be interpreted as follows: +- the SERE =(1;1)[*]= matches all prefixes of even length (here =1= + stands for the true formula, so it matches anything) +- the part =...[]->a= requests that =a= should be true at the end of each + matched prefix. + +Therefore this formula ensures that =a= is true at every even instant +(if we consider the first instant to be odd). This is the canonical +example of formula that can be expressed in PSL but not in LTL. + +A few other operators and syntactic sugar are supported. For more +discussion about the temporal operators and their semantics, see the +[[https://spot.lrde.epita.fr/tl.pdf][tl.pdf]] document. + +* Translation of temporal logic to automata + :PROPERTIES: + :CUSTOM_ID: ltl2tgba + :END: + +Spot can translate any LTL or PSL formula into Büchi automata, or generalized Büchi automata. + +Internally the translator produces [[#trans-acc][Transition-based Generalized Büchi Automata (TGBA)]] but that +automaton can then be simplified using several algorithms depending on what options were given. + +Here is for instance a translation of ={(1;1)[*]}[]->a= discussed [[#psl][above]]. + +#+NAME: ltl2tgba1 +#+BEGIN_SRC sh :results verbatim :exports both +ltl2tgba '{(1;1)[*]}[]->a' -d +#+END_SRC +#+BEGIN_SRC dot :file concept-ltl2tgba.png :cmdline -Tpng :var txt=ltl2tgba1 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:concept-ltl2tgba.png]] + + +[[file:tut10.org][Another page shows how to translate an LTL formula into a never claim]] +from the command-line, Python, or C++. + +* Architecture of Spot + :PROPERTIES: + :CUSTOM_ID: architecture + :END: + +The Spot project can be broken down into several main parts: + + - =libbddx=: a customized version of [[http://sourceforge.net/projects/buddy/][the BuDDy library]], for manipulating [[#bdd][BDDs]]. + - =libspot=: the main library, containing a C++11 implementation of all the + data structures and algorithms. This depends on =libddx=. + - [[file:tools.org][command-line tools]]: built upon the =libspot= library, exporting some of its + features to shell users + - Python bindings for =libbddx= and =libspot=: those make it possible to write + python scripts for specific tasks, and allow interactive use of the library + via environments such a [[http://ipython.org][IPython/Jupyter]]. diff --git a/doc/org/index.org b/doc/org/index.org index 10c0ce291..76162acff 100644 --- a/doc/org/index.org +++ b/doc/org/index.org @@ -6,16 +6,17 @@ Spot is a C++11 library for ω-automata manipulation and model checking. It has the following notable features: -- Support for LTL (several syntaxes supported) and the linear fragment - of PSL. -- Support for ω-automata with arbitrary acceptance condition. -- Support for transition-based acceptance (state-based acceptance is +- Support for [[file:concepts.org::#ltl][LTL]] (several syntaxes supported) and + [[file:concepts.org::#psl][the linear fragment of PSL]]. +- Support for ω-automata with [[file:concepts.org::#acceptance-condition][arbitrary acceptance condition]]. +- Support for [[file:concepts.org::#trans-acc][transition-based acceptance]] (state-based acceptance is supported by a reduction to transition-based acceptance). - The automaton parser can read a stream of automata written in any of four syntaxes ([[file:hoa.org][HOA]], [[http://spinroot.com/spin/Man/never.html][never claims]], [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT]], [[http://www.ltl2dstar.de/docs/ltl2dstar.html][DSTAR]]). - Several algorithms for formula manipulation including: simplifying formulas, testing implication or equivalence, testing - stutter-invariance, removing some operators by rewriting, ... + stutter-invariance, removing some operators by rewriting, translation + to automata... - Several algorithms for automata manipulation including: product, emptiness checks, simulation-based reductions, minimization of weak-DBA, removal of useless SCCs, acceptance-condition diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 72628d920..204348ddd 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -845,6 +845,9 @@ export SPOT_DOTEXTRA='node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee #+END_SRC * Statistics + :PROPERTIES: + :CUSTOM_ID: stats + :END: The =--stats= option takes format string parameter to specify what and how statistics should be output. diff --git a/doc/org/spot.css b/doc/org/spot.css index 61794afd1..12c526e38 100644 --- a/doc/org/spot.css +++ b/doc/org/spot.css @@ -49,3 +49,5 @@ img{max-width:100%} .org-hoa-header-uppercase{font-weight:bold;color:#00adad} .org-hoa-header-lowercase{color:#00adad} .org-hoa-ap-number{color:#d70079} +.implem{background:#f1f0a6;padding:0.5ex 1ex 0.5ex 1ex;margin:1ex;border-color:#ffe35e;border-style:solid none} +.implem:before{background:#ffe35e;content:"Implementation detail";padding:.5ex;position:relative;top:0;left:0;font-weight:bold} diff --git a/doc/org/tut.org b/doc/org/tut.org index 43d8da865..ca08eac5b 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -11,6 +11,9 @@ to see illustrated here. If you have difficulties compiling the C++ examples, check out [[file:compile.org][these instructions]]. +Reading the [[file:concepts.org][concepts page]] might help if you are not familiar with some +of the objects manipulated here. + * Examples with Shell, Python, and C++ All the following pages show how to perform the same task using the -- GitLab