org: add some help for upgrading old code
* doc/org/upgrade2.org: New file. * doc/Makefile.am, doc/org/index.org: Add it. * doc/org/tut22.org: Add some custom id for reference. * doc/org/spot.css: Style the tables. * NEWS: Mention the new doc.
This commit is contained in:
Alexandre Duret-Lutz
parent
65726c0f60
commit
892e648970
6 changed files with 668 additions and 1 deletions
6
NEWS
6
NEWS
|
|
@ -4,6 +4,12 @@ New in spot 1.99.8a (not yet released)
|
|||
|
||||
* twa::ap_var() renamed to twa::ap_vars().
|
||||
|
||||
Documentation:
|
||||
|
||||
* The page https://spot.lrde.epita.fr/upgrade2.html should help
|
||||
people migrating old C++ code written for Spot 1.2.x, and update
|
||||
it for Spot 2.0.
|
||||
|
||||
New in spot 1.99.8 (2016-02-18)
|
||||
|
||||
Command-line tools:
|
||||
|
|
|
|||
|
|
@ -99,6 +99,7 @@ ORG_FILES = \
|
|||
org/tut21.org \
|
||||
org/tut22.org \
|
||||
org/tut30.org \
|
||||
org/upgrade2.org \
|
||||
org/satmin.org \
|
||||
org/satmin.tex \
|
||||
org/setup.org \
|
||||
|
|
|
|||
|
|
@ -35,10 +35,12 @@ The latest version is *{{{LASTRELEASE}}}* and was released on
|
|||
|
||||
* Documentation
|
||||
|
||||
- [[file:concepts.org][Basic concepts]].
|
||||
- [[file:tools.org][Command-line tools]].
|
||||
- [[file:tut.org][Code examples]].
|
||||
- [[http://spot.lrde.epita.fr/doxygen/][Doxygen documentation]], generated automatically from the source code.
|
||||
- [[https://spot.lrde.epita.fr/tl.pdf][Definition of the temporal operators supported by Spot]].
|
||||
- [[file:upgrade2.org][Help for upgrading existing code written for Spot 1.2.x to Spot 2]].
|
||||
|
||||
* Try Spot On-line
|
||||
|
||||
|
|
|
|||
|
|
@ -34,6 +34,12 @@ img{max-width:100%}
|
|||
#table-of-contents{border:1px solid #ffd300}
|
||||
#org-div-home-and-up{visibility:hidden}
|
||||
}
|
||||
|
||||
thead tr {background: #ffe35e;}
|
||||
tbody:nth-child(odd) tr:nth-child(even) {background: #fff0a6;}
|
||||
tbody:nth-child(odd) tr:nth-child(odd) {background: #fff7cf;}
|
||||
tbody:nth-child(even) tr:nth-child(even) {background: #fff3bc;}
|
||||
tbody:nth-child(even) tr:nth-child(odd) {background: #fffbe0;}
|
||||
.org-keyword{font-weight:bold}
|
||||
.org-builtin{font-weight:bold}
|
||||
.org-preprocessor{font-weight:bold}
|
||||
|
|
@ -49,5 +55,7 @@ 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{background:#fff0a6;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}
|
||||
.caveat{background:#ef99c9;padding:0.5ex 1ex 0.5ex 1ex;margin:1ex;border-color:#d70079;border-style:solid none}
|
||||
.caveat:before{background:#d70079;content:"Caveat";padding:.5ex;position:relative;top:0;left:0;font-weight:bold}
|
||||
|
|
|
|||
|
|
@ -6,6 +6,9 @@
|
|||
This example demonstrates how to create an automaton and then print it.
|
||||
|
||||
* C++
|
||||
:PROPERTIES:
|
||||
:CUSTOM_ID: cpp
|
||||
:END:
|
||||
|
||||
#+BEGIN_SRC C++ :results verbatim :exports both :wrap SRC hoa
|
||||
#include <iostream>
|
||||
|
|
|
|||
647
doc/org/upgrade2.org
Normal file
647
doc/org/upgrade2.org
Normal file
|
|
@ -0,0 +1,647 @@
|
|||
# -*- coding: utf-8 -*-
|
||||
#+TITLE: Upgrading from Spot 1.2.6
|
||||
#+SETUPFILE: setup.org
|
||||
#+HTML_LINK_UP: index.html
|
||||
|
||||
This page is for people who have code written for Spot 1.2.6, and
|
||||
would like to upgrade to Spot 2.0. The changes listed here will
|
||||
probably also apply to code written using older Spot 1.x versions.
|
||||
|
||||
This page is in no way exhaustive. The main intent is just to list
|
||||
the major changes that have occurred in the library since version
|
||||
1.2.6, so that one can more easily update existing code. The focus is
|
||||
based on features that appear to be commonly used, based on our the
|
||||
experience of updating a couple of projects that are using Spot.
|
||||
|
||||
* Overview of the changes
|
||||
|
||||
Let's begin by just trying to summarize what has changed between
|
||||
Spot 1.2.6 and Spot 2.0, just to get an idea of what will need to be
|
||||
updated.
|
||||
|
||||
1. [[#cpp11][Spot now compiles using the C++11 standard]]. Compliant compiler
|
||||
are sufficiently widespread now that this should not be an issue.
|
||||
|
||||
2. The layout of the source-tree and the layout of the installed
|
||||
header files have been completely overhauled, and several header
|
||||
files have been renamed. An early step of upgrading existing
|
||||
code dependent on Spot will therefore be to [[#includes][update all the
|
||||
=#include=]].
|
||||
|
||||
3. [[#buddy][The customized version of BuDDy distributed with Spot has been
|
||||
renamed]] to not clash with any regular version installed on the
|
||||
system.
|
||||
|
||||
4. [[#formulas][The implementation of LTL formulas has been rewritten]].
|
||||
|
||||
They are no longer pointers but plain objects that performs their
|
||||
own reference counting, freeing the programmer from this tedious
|
||||
and error-prone task. They could be handled as if they were
|
||||
shared pointer, with the small difference that they are not using
|
||||
C++'s standard shared pointers.
|
||||
|
||||
All operators are now implemented using a single type of node,
|
||||
with a field that can be used to make a switch instead of what
|
||||
used to require visitors.
|
||||
|
||||
5. Allocated object that are large or expected to have a long life
|
||||
(such as automata, BDD dictionnaries, accepting runs) are now
|
||||
[[#shared_ptr][returned using shared pointers]].
|
||||
|
||||
6. Spot used to be centered around the concept of TGBA
|
||||
(Transition-based Generalized Büchi Automata), i.e.,
|
||||
\omega-automata in which a run is accepting if it visits
|
||||
infinitely often one transition in each defined accepting set of
|
||||
transitions. This was implemented as a =tgba= class.
|
||||
|
||||
In Spot 2.0, each automaton can have a different acceptance
|
||||
condition: this includes well known acceptance conditions such as
|
||||
Büchi, co-Büchi, Rabin, Streett, or parity, but it could also be
|
||||
an arbitrarily complex Boolean combination of those. [[#tgba-twa][The central
|
||||
automaton concept is now called T\omega{}A]] (for Transition-based
|
||||
\omega-Automata), and implemented as a =twa= class. The =tgba=
|
||||
class does not exist anymore: a TGBA is just a T\omega{}A in
|
||||
which the acceptance condition has been set to "generalized
|
||||
Büchi".
|
||||
|
||||
While the gained generality on acceptance conditions allows us to
|
||||
write algorithms that may work on any acceptance condition, Spot
|
||||
still contains algorithms that work only on a particular
|
||||
acceptance condition. Those restrictions have to be ensured
|
||||
using preconditions: the acceptance condition does not appear in
|
||||
the type of the C++ object representing the automaton.
|
||||
|
||||
7. [[*Various renamings][Several class, functions, and methods, have been renamed]]. Some
|
||||
have been completely reimplemented, with different interfaces.
|
||||
In particular the =tgba_explicit_*= familly of classes
|
||||
(=tgba_explicit_formula=, =tgba_explicit_number=,
|
||||
=tgba_explicit_string= used to encode a TGBA using a graph whose
|
||||
state was named using LTL formulas, integers, or strings) are
|
||||
replaced by a =twa_graph= class in which the representation is
|
||||
more complact and efficient, but where states are necessarily
|
||||
numbered. Many algorithms have been rewritten on top of this
|
||||
=twa_graph= class, and this simplified them a lot.
|
||||
|
||||
* Upgrading to C++11
|
||||
:PROPERTIES:
|
||||
:CUSTOM_ID: cpp11
|
||||
:END:
|
||||
|
||||
Because Spot now relies on C++11 features, programs that use Spot
|
||||
should at least be compiled using this version (or a later one) of
|
||||
the language.
|
||||
|
||||
Before the =g++= 6.0, the default C++ standard used was C++98, and
|
||||
enabling C++11 is usually done by passing the option =-std=c++11=.
|
||||
In =g++= 6.0 the default C++ standard used is C++14, so passing
|
||||
=-std=c++11= is only necessary in projects that are incompatible
|
||||
with C++14.
|
||||
|
||||
Upgrading from C++98 or C++03 to C++11 should be relatively smooth
|
||||
as the language is /mostly/ backward compatible.
|
||||
|
||||
* Upgrading =#include= directives
|
||||
:PROPERTIES:
|
||||
:CUSTOM_ID: include
|
||||
:END:
|
||||
|
||||
** Adjusting the search path
|
||||
:PROPERTIES:
|
||||
:CUSTOM_ID: include-search
|
||||
:END:
|
||||
|
||||
|
||||
If Spot 1.2.6 was installed in =/usr/local=, its headers are
|
||||
in =/usr/local/include/spot=. One would to write include statements
|
||||
such as
|
||||
#+BEGIN_SRC c++
|
||||
#include <tgba/tgba.hh>
|
||||
#include <ltl/formula.hh>
|
||||
#+END_SRC
|
||||
and then compile with =-I /usr/local/include/spot/= to make sure that
|
||||
the Spot headers were found. Headers in Spot would also include other
|
||||
header in Spot by using names relative to the =/usr/local/include/spot/=
|
||||
directory.
|
||||
|
||||
If Spot 2.0 is installed in =/usr/local=, its headers are still in
|
||||
=/usr/local/include/spot= however the =spot/= directory is and should
|
||||
always be used to refer to the header:
|
||||
#+BEGIN_SRC c++
|
||||
#include <spot/twa/twa.hh> // the new name of tgba/tgba.hh
|
||||
#include <spot/tl/formula.hh> // the new name of ltl/formula.hh
|
||||
#+END_SRC
|
||||
Now compilation should only be done with option =-I
|
||||
/usr/local/include=, which is usually already included by default.
|
||||
|
||||
** Renaming headers files
|
||||
:PROPERTIES:
|
||||
:CUSTOM_ID: includes
|
||||
:END:
|
||||
|
||||
The following table shows all the headers installed by Spot 1.2.6, and
|
||||
the corresponding name to include in Spot 2.0. Some of the new names
|
||||
do not exactly correspond to a renaming, but instead correspond to headers
|
||||
that provide a function with a similar service.
|
||||
|
||||
|
||||
|------------------------------------+------------------------------------+--------------------------------------------------|
|
||||
| old name | new name or suggested replacement | comment |
|
||||
|------------------------------------+------------------------------------+--------------------------------------------------|
|
||||
| ~bdd.h~ | ~bddx.h~ | customized version of BuDDy |
|
||||
| ~bvec.h~ | ~bvecx.h~ | customized version of BuDDy |
|
||||
| ~fdd.h~ | ~fddx.h~ | customized version of BuDDy |
|
||||
|------------------------------------+------------------------------------+--------------------------------------------------|
|
||||
| ~dstarparse/public.hh~ | ~spot/parseaut/public.hh~ | single parser for all automata |
|
||||
| ~eltlparse/public.hh~ | | not supported anymore |
|
||||
| ~iface/dve2/dve2.hh~ | ~spot/ltsmin/ltsmin.hh~ | |
|
||||
| ~kripke/fairkripke.hh~ | ~spot/kripke/fairkripke.hh~ | |
|
||||
| ~kripke/kripkeexplicit.hh~ | ~spot/kripke/kripkegraph.hh~ | new implementation |
|
||||
| ~kripke/kripke.hh~ | ~spot/kripke/kripke.hh~ | |
|
||||
| ~kripke/kripkeprint.hh~ | ~spot/twaalgos/hoa.hh~ | adhoc output format replaced by HOA |
|
||||
| ~kripkeparse/public.hh~ | ~spot/parseaut/public.hh~ | single parser for all automata |
|
||||
|------------------------------------+------------------------------------+--------------------------------------------------|
|
||||
| ~ltlast/allnodes.hh~ | ~spot/tl/formula.hh~ | new implementation of formulas |
|
||||
| ~ltlast/atomic_prop.hh~ | ~spot/tl/formula.hh~ | new implementation of formulas |
|
||||
| ~ltlast/automatop.hh~ | ~spot/tl/formula.hh~ | new implementation of formulas |
|
||||
| ~ltlast/binop.hh~ | ~spot/tl/formula.hh~ | new implementation of formulas |
|
||||
| ~ltlast/bunop.hh~ | ~spot/tl/formula.hh~ | new implementation of formulas |
|
||||
| ~ltlast/constant.hh~ | ~spot/tl/formula.hh~ | new implementation of formulas |
|
||||
| ~ltlast/formula.hh~ | ~spot/tl/formula.hh~ | new implementation of formulas |
|
||||
| ~ltlast/multop.hh~ | ~spot/tl/formula.hh~ | new implementation of formulas |
|
||||
| ~ltlast/nfa.hh~ | | not supported anymore |
|
||||
| ~ltlast/predecl.hh~ | | not needed anymore |
|
||||
| ~ltlast/refformula.hh~ | | not needed anymore |
|
||||
| ~ltlast/unop.hh~ | ~spot/tl/formula.hh~ | new implementation of formulas |
|
||||
| ~ltlast/visitor.hh~ | | not supported anymore |
|
||||
| ~ltlenv/declenv.hh~ | ~spot/tl/declenv.hh~ | |
|
||||
| ~ltlenv/defaultenv.hh~ | ~spot/tl/defaultenv.hh~ | |
|
||||
| ~ltlenv/environment.hh~ | ~spot/tl/environment.hh~ | |
|
||||
| ~ltlparse/ltlfile.hh~ | | not supported anymore |
|
||||
| ~ltlparse/public.hh~ | ~spot/tl/parse.hh~ | |
|
||||
| ~ltlvisit/apcollect.hh~ | ~spot/tl/apcollect.hh~ | |
|
||||
| ~ltlvisit/clone.hh~ | | not needed anymore |
|
||||
| ~ltlvisit/contain.hh~ | ~spot/tl/contain.hh~ | |
|
||||
| ~ltlvisit/destroy.hh~ | | not needed anymore |
|
||||
| ~ltlvisit/dotty.hh~ | ~spot/tl/dot.hh~ | |
|
||||
| ~ltlvisit/dump.hh~ | ~spot/tl/formula.hh~ | member of the formula class |
|
||||
| ~ltlvisit/lbt.hh~ | ~spot/tl/print.hh~ | |
|
||||
| ~ltlvisit/length.hh~ | ~spot/tl/length.hh~ | |
|
||||
| ~ltlvisit/lunabbrev.hh~ | ~spot/tl/unabbrev.hh~ | generalized |
|
||||
| ~ltlvisit/nenoform.hh~ | ~spot/tl/nenoform.hh~ | |
|
||||
| ~ltlvisit/postfix.hh~ | | not supported anymore |
|
||||
| ~ltlvisit/randomltl.hh~ | ~spot/tl/randomltl.hh~ | |
|
||||
| ~ltlvisit/reduce.hh~ | ~spot/tl/simplify.hh~ | was already deprecated |
|
||||
| ~ltlvisit/relabel.hh~ | ~spot/tl/relabel.hh~ | |
|
||||
| ~ltlvisit/remove_x.hh~ | ~spot/tl/remove_x.hh~ | |
|
||||
| ~ltlvisit/simpfg.hh~ | ~spot/tl/unabbrev.hh~ | generalized |
|
||||
| ~ltlvisit/simplify.hh~ | ~spot/tl/simplify.hh~ | |
|
||||
| ~ltlvisit/snf.hh~ | ~spot/tl/snf.hh~ | |
|
||||
| ~ltlvisit/tostring.hh~ | ~spot/tl/print.hh~ | |
|
||||
| ~ltlvisit/tunabbrev.hh~ | ~spot/tl/unabbrev.hh~ | generalized |
|
||||
| ~ltlvisit/wmunabbrev.hh~ | ~spot/lt/wmunabbrev.hh~ | generalized |
|
||||
|------------------------------------+------------------------------------+--------------------------------------------------|
|
||||
| ~misc/bareword.hh~ | ~spot/misc/bareword.hh~ | |
|
||||
| ~misc/bddlt.hh~ | ~spot/misc/bddlt.hh~ | |
|
||||
| ~misc/bddop.hh~ | | not needed anymore |
|
||||
| ~misc/bitvect.hh~ | ~spot/misc/bitvect.hh~ | |
|
||||
| ~misc/casts.hh~ | ~spot/misc/casts.hh~ | |
|
||||
| ~misc/common.hh~ | ~spot/misc/common.hh~ | |
|
||||
| ~misc/_config.h~ | ~spot/misc/_config.h~ | |
|
||||
| ~misc/escape.hh~ | ~spot/misc/escape.hh~ | |
|
||||
| ~misc/fixpool.hh~ | ~spot/misc/fixpool.hh~ | |
|
||||
| ~misc/formater.hh~ | ~spot/misc/formater.hh~ | |
|
||||
| ~misc/hashfunc.hh~ | ~spot/misc/hashfunc.hh~ | |
|
||||
| ~misc/hash.hh~ | ~spot/misc/hash.hh~ | |
|
||||
| ~misc/intvcmp2.hh~ | ~spot/misc/intvcmp2.hh~ | |
|
||||
| ~misc/intvcomp.hh~ | ~spot/misc/intvcomp.hh~ | |
|
||||
| ~misc/location.hh~ | ~spot/misc/location.hh~ | |
|
||||
| ~misc/ltstr.hh~ | ~spot/misc/ltstr.hh~ | |
|
||||
| ~misc/memusage.hh~ | ~spot/misc/memusage.hh~ | |
|
||||
| ~misc/minato.hh~ | ~spot/misc/minato.hh~ | |
|
||||
| ~misc/mspool.hh~ | ~spot/misc/mspool.hh~ | |
|
||||
| ~misc/optionmap.hh~ | ~spot/misc/optionmap.hh~ | |
|
||||
| ~misc/position.hh~ | ~spot/misc/position.hh~ | |
|
||||
| ~misc/random.hh~ | ~spot/misc/random.hh~ | |
|
||||
| ~misc/satsolver.hh~ | ~spot/misc/satsolver.hh~ | |
|
||||
| ~misc/timer.hh~ | ~spot/misc/timer.hh~ | |
|
||||
| ~misc/tmpfile.hh~ | ~spot/misc/tmpfile.hh~ | |
|
||||
| ~misc/unique_ptr.hh~ | ~memory~ | use =std::unique_ptr= from C++11 |
|
||||
| ~misc/version.hh~ | ~spot/misc/version.hh~ | |
|
||||
|------------------------------------+------------------------------------+--------------------------------------------------|
|
||||
| ~neverparse/public.hh~ | ~spot/parseaut/public.hh~ | single parser for all automata |
|
||||
| ~sabaalgos/sabadotty.hh~ | | not supported anymore |
|
||||
| ~sabaalgos/sabareachiter.hh~ | | not supported anymore |
|
||||
| ~saba/explicitstateconjunction.hh~ | | not supported anymore |
|
||||
| ~saba/sabacomplementtgba.hh~ | | not supported anymore |
|
||||
| ~saba/saba.hh~ | | not supported anymore |
|
||||
| ~saba/sabastate.hh~ | | not supported anymore |
|
||||
| ~saba/sabasucciter.hh~ | | not supported anymore |
|
||||
|------------------------------------+------------------------------------+--------------------------------------------------|
|
||||
| ~taalgos/dotty.hh~ | ~spot/taalgos/dot.hh~ | |
|
||||
| ~taalgos/emptinessta.hh~ | ~spot/taalgos/emptinessta.hh~ | |
|
||||
| ~taalgos/minimize.hh~ | ~spot/taalgos/minimize.hh~ | |
|
||||
| ~taalgos/reachiter.hh~ | ~spot/taalgos/reachiter.hh~ | |
|
||||
| ~taalgos/statessetbuilder.hh~ | ~spot/taalgos/statesetbuilder.hh~ | |
|
||||
| ~taalgos/stats.hh~ | ~spot/taalgos/stats.hh~ | |
|
||||
| ~taalgos/tgba2ta.hh~ | ~spot/taalgos/tgba2ta.hh~ | |
|
||||
| ~ta/taexplicit.hh~ | ~spot/ta/taexplicit.hh~ | old implementation (ought to be changed) |
|
||||
| ~ta/ta.hh~ | ~spot/ta/ta.hh~ | |
|
||||
| ~ta/taproduct.hh~ | ~spot/ta/taproduct.hh~ | |
|
||||
| ~ta/tgtaexplicit.hh~ | ~spot/ta/tgtaexplicit.hh~ | old implementation (ought to be changed) |
|
||||
| ~ta/tgta.hh~ | ~spot/ta/tgta.hh~ | |
|
||||
| ~ta/tgtaproduct.hh~ | ~spot/ta/tgtaproduct.hh~ | |
|
||||
|------------------------------------+------------------------------------+--------------------------------------------------|
|
||||
| ~tgbaalgos/bfssteps.hh~ | ~spot/twaalgos/bfssteps.hh~ | |
|
||||
| ~tgbaalgos/complete.hh~ | ~spot/twaalgos/complete.hh~ | |
|
||||
| ~tgbaalgos/compsusp.hh~ | ~spot/twaalgos/compsusp.hh~ | |
|
||||
| ~tgbaalgos/cutscc.hh~ | | not supported anymore |
|
||||
| ~tgbaalgos/cycles.hh~ | ~spot/twaalgos/cycles.hh~ | |
|
||||
| ~tgbaalgos/degen.hh~ | ~spot/twaalgos/degen.hh~ | |
|
||||
| ~tgbaalgos/dottydec.hh~ | | not supported anymore |
|
||||
| ~tgbaalgos/dotty.hh~ | ~spot/twaalgos/dot.hh~ | |
|
||||
| ~tgbaalgos/dtbasat.hh~ | ~spot/twaalgos/dtbasat.hh~ | |
|
||||
| ~tgbaalgos/dtgbacomp.hh~ | ~spot/twaalgos/complement.hh~ | |
|
||||
| ~tgbaalgos/dtgbasat.hh~ | ~spot/twaalgos/dtwasat.hh~ | |
|
||||
| ~tgbaalgos/dupexp.hh~ | ~spot/twaalgos/copy.hh~ | also a copy constructor of twa |
|
||||
| ~tgbaalgos/eltl2tgba_lacim.hh~ | | not supported anymore |
|
||||
| ~tgbaalgos/emptiness.hh~ | ~spot/twaalgos/emptiness.hh~ | |
|
||||
| ~tgbaalgos/emptiness_stats.hh~ | ~spot/twaalgos/emptiness_stats.hh~ | |
|
||||
| ~tgbaalgos/gtec/ce.hh~ | ~spot/twaalgos/gtec/ce.hh~ | |
|
||||
| ~tgbaalgos/gtec/explscc.hh~ | | not supported anymore |
|
||||
| ~tgbaalgos/gtec/gtec.hh~ | ~spot/twaalgos/gtec/gtec.hh~ | |
|
||||
| ~tgbaalgos/gtec/nsheap.hh~ | | not supported anymore |
|
||||
| ~tgbaalgos/gtec/sccstack.hh~ | ~spot/twaalgos/gtec/sccstack.hh~ | |
|
||||
| ~tgbaalgos/gtec/status.hh~ | ~spot/twaalgos/gtec/status.hh~ | |
|
||||
| ~tgbaalgos/gv04.hh~ | ~spot/twaalgos/gv04.hh~ | |
|
||||
| ~tgbaalgos/hoaf.hh~ | ~spot/twaalgos/hoa.hh~ | |
|
||||
| ~tgbaalgos/isdet.hh~ | ~spot/twaalgos/isdet.hh~ | |
|
||||
| ~tgbaalgos/isweakscc.hh~ | ~spot/twaalgos/isweakscc.hh~ | |
|
||||
| ~tgbaalgos/lbtt.hh~ | ~spot/twaalgos/lbtt.hh~ | |
|
||||
| ~tgbaalgos/ltl2taa.hh~ | ~spot/twaalgos/ltl2taa.hh~ | |
|
||||
| ~tgbaalgos/ltl2tgba_fm.hh~ | ~spot/twaalgos/ltl2tgba_fm.hh~ | |
|
||||
| ~tgbaalgos/ltl2tgba_lacim.hh~ | | not supported anymore |
|
||||
| ~tgbaalgos/magic.hh~ | ~spot/twaalgos/magic.hh~ | |
|
||||
| ~tgbaalgos/minimize.hh~ | ~spot/twaalgos/minimize.hh~ | |
|
||||
| ~tgbaalgos/neverclaim.hh~ | ~spot/twaalgos/neverclaim.hh~ | |
|
||||
| ~tgbaalgos/postproc.hh~ | ~spot/twaalgos/postproc.hh~ | |
|
||||
| ~tgbaalgos/powerset.hh~ | ~spot/twaalgos/powerset.hh~ | |
|
||||
| ~tgbaalgos/projrun.hh~ | ~spot/twaalgos/projrun.hh~ | |
|
||||
| ~tgbaalgos/randomgraph.hh~ | ~spot/twaalgos/randomgraph.hh~ | |
|
||||
| ~tgbaalgos/reachiter.hh~ | ~spot/twaalgos/reachiter.hh~ | |
|
||||
| ~tgbaalgos/reducerun.hh~ | ~spot/twaalgos/emptiness.hh~ | now =twa_run::reduce()= |
|
||||
| ~tgbaalgos/reductgba_sim.hh~ | ~spot/twaalgos/simulation.hh~ | was already deprecated |
|
||||
| ~tgbaalgos/replayrun.hh~ | ~spot/twaalgos/emptiness.hh~ | now =twa_run::replay()= |
|
||||
| ~tgbaalgos/rundotdec.hh~ | ~spot/twaalgos/emptiness.hh~ | now =twa_run::highlight()= |
|
||||
| ~tgbaalgos/safety.hh~ | ~spot/twaalgos/strength.hh~ | |
|
||||
| ~tgbaalgos/save.hh~ | ~spot/twaalgos/hoa.hh~ | adhoc output format replaced by HOA |
|
||||
| ~tgbaalgos/sccfilter.hh~ | ~spot/twaalgos/sccfilter.hh~ | |
|
||||
| ~tgbaalgos/scc.hh~ | ~spot/twaalgos/sccinfo.hh~ | new implementation restricted to ~twa_graph~ |
|
||||
| ~tgbaalgos/se05.hh~ | ~spot/twaalgos/se05.hh~ | |
|
||||
| ~tgbaalgos/simulation.hh~ | ~spot/twaalgos/simulation.hh~ | |
|
||||
| ~tgbaalgos/stats.hh~ | ~spot/twaalgos/stats.hh~ | |
|
||||
| ~tgbaalgos/stripacc.hh~ | ~spot/twaalgos/stripacc.hh~ | |
|
||||
| ~tgbaalgos/tau03.hh~ | ~spot/twaalgos/tau03.hh~ | |
|
||||
| ~tgbaalgos/tau03opt.hh~ | ~spot/twaalgos/tau03opt.hh~ | |
|
||||
| ~tgbaalgos/translate.hh~ | ~spot/twaalgos/translate.hh~ | |
|
||||
| ~tgbaalgos/word.hh~ | ~spot/twaalgos/word.hh~ | |
|
||||
|------------------------------------+------------------------------------+--------------------------------------------------|
|
||||
| ~tgba/bdddict.hh~ | ~spot/twa/bdddict.hh~ | |
|
||||
| ~tgba/bddprint.hh~ | ~spot/twa/bddprint.hh~ | |
|
||||
| ~tgba/formula2bdd.hh~ | ~spot/twa/formula2bdd.hh~ | |
|
||||
| ~tgba/futurecondcol.hh~ | | not supported anymore |
|
||||
| ~tgba/public.hh~ | ~spot/twa/twa.hh~ | |
|
||||
| ~tgba/sba.hh~ | | replaced by a flag in =twa= |
|
||||
| ~tgba/statebdd.hh~ | | not supported anymore |
|
||||
| ~tgba/state.hh~ | ~spot/twa/twa.hh~ | |
|
||||
| ~tgba/succiterconcrete.hh~ | | not supported anymore |
|
||||
| ~tgba/succiter.hh~ | ~spot/twa/twa.hh~ | |
|
||||
| ~tgba/taatgba.hh~ | ~spot/twa/taatgba.hh~ | |
|
||||
| ~tgba/tgbabddconcretefactory.hh~ | | not supported anymore |
|
||||
| ~tgba/tgbabddconcrete.hh~ | | not supported anymore |
|
||||
| ~tgba/tgbabddconcreteproduct.hh~ | | not supported anymore |
|
||||
| ~tgba/tgbabddcoredata.hh~ | | not supported anymore |
|
||||
| ~tgba/tgbabddfactory.hh~ | | not supported anymore |
|
||||
| ~tgba/tgbaexplicit.hh~ | ~spot/twa/twagraph.hh~ | |
|
||||
| ~tgba/tgba.hh~ | ~spot/twa/twa.hh~ | |
|
||||
| ~tgba/tgbakvcomplement.hh~ | | use ~tgba_determinize()~ and ~dtwa_complement()~ |
|
||||
| ~tgba/tgbamask.hh~ | ~spot/twa/tgbamask.hh~ | |
|
||||
| ~tgba/tgbaproduct.hh~ | ~spot/twa/tgbaproduct.hh~ | |
|
||||
| ~tgba/tgbaproxy.hh~ | | not supported anymore |
|
||||
| ~tgba/tgbasafracomplement.hh~ | ~spot/twaalgos/determinize.hh~ | |
|
||||
| ~tgba/tgbascc.hh~ | ~spot/twaalgos/mask.hh~ | |
|
||||
| ~tgba/tgbasgba.hh~ | ~spot/twaalgos/sbacc.hh~ | |
|
||||
| ~tgba/tgbatba.hh~ | ~spot/twaalgos/degen.hh~ | |
|
||||
| ~tgba/tgbaunion.hh~ | | not yet reimplemented |
|
||||
| ~tgba/wdbacomp.hh~ | ~spot/twaalgos/complement.hh~ | use ~dtwa_complement()~ instead |
|
||||
|------------------------------------+------------------------------------+--------------------------------------------------|
|
||||
| ~tgbaparse/public.hh~ | ~spot/parseaut/public.hh~ | single parser for all automata |
|
||||
|
||||
* BuDDy was renamed
|
||||
:PROPERTIES:
|
||||
:CUSTOM_ID: buddy
|
||||
:END:
|
||||
|
||||
Spot install a customized version of the BDD library BuDDy.
|
||||
|
||||
As shown in [[#includes][the table of renamed header files]], the header files for
|
||||
this library were all renamed: they have an =x= appended (=bddx.h=,
|
||||
=bvecx.h=, =fddx.h=). The name of the library was renamed as well:
|
||||
=libbdd.so= and =libbdd.a= are now respectively =libbddx.so= and
|
||||
=libbddx.a=. This means one should now pass =-lspot -lbddx= to the
|
||||
linker (instead of =-lspot -lbdd=) when linking against Spot.
|
||||
|
||||
* New implementation for temporal logic formulas
|
||||
:PROPERTIES:
|
||||
:CUSTOM_ID: formulas
|
||||
:END:
|
||||
|
||||
As can be guessed from the [[#includes][the table of renamed header files]], the
|
||||
class hierarchy for temporal formulas has been entirely
|
||||
rewritten. This change is actually quite massive (~13200 lines
|
||||
removed, ~8200 lines added), and brings some nice benefits:
|
||||
- LTL/PSL formulas are now represented by lightweight formula
|
||||
objects (instead of pointers to children of an abstract
|
||||
formula class) that perform reference counting automatically.
|
||||
- There is no hierachy anymore: all operators are represented by
|
||||
a single type of node in the syntax tree, and an enumerator is
|
||||
used to distinguish between operators.
|
||||
- Visitors have been replaced by member functions such as =map()=
|
||||
or =traverse()=, that take a function (usually written as a
|
||||
lambda function) and apply it to the nodes of the tree.
|
||||
- As a consequence, writing algorithms that manipulate formula is more
|
||||
friendly, and several algorithms that spanned a few pages have been
|
||||
reduced to a few lines. [[file:tut03.org][This page]] illustrates the new interface.
|
||||
|
||||
Also the =spot::ltl= namespace has been removed: everything is
|
||||
directly in =spot= now.
|
||||
|
||||
In code where formulas are just parsed from input string, and then
|
||||
passed on to other algorithms (e.g., translation to automata): it will
|
||||
suffice to change all occurrences of =const spot::ltl::formula*= into
|
||||
a plain =spot::formula=, and remove all calls to =->destroy()= or
|
||||
=->clone()= (that were used to perform explicit reference counting).
|
||||
|
||||
* Many objects are now returned as =std::shared_ptr=
|
||||
:PROPERTIES:
|
||||
:CUSTOM_ID: shared_ptr
|
||||
:END:
|
||||
|
||||
By convention =foo_ptr= is a =typedef= for =std::share_ptr<foo>=. The
|
||||
following typedefs are provided:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports results
|
||||
find ../../spot -name '[^.]*.hh' | xargs grep -h 'typedef.*_ptr;' | sed 's/^[ \t]*//' | sort -u
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
typedef std::shared_ptr<bdd_dict> bdd_dict_ptr;
|
||||
typedef std::shared_ptr<const fair_kripke> const_fair_kripke_ptr;
|
||||
typedef std::shared_ptr<const kripke> const_kripke_ptr;
|
||||
typedef std::shared_ptr<const kripke_explicit> const_kripke_explicit_ptr;
|
||||
typedef std::shared_ptr<const parsed_aut> const_parsed_aut_ptr;
|
||||
typedef std::shared_ptr<const taa_tgba_formula> const_taa_tgba_formula_ptr;
|
||||
typedef std::shared_ptr<const taa_tgba_string> const_taa_tgba_string_ptr;
|
||||
typedef std::shared_ptr<const ta> const_ta_ptr;
|
||||
typedef std::shared_ptr<const ta_explicit> const_ta_explicit_ptr;
|
||||
typedef std::shared_ptr<const ta_product> const_ta_product_ptr;
|
||||
typedef std::shared_ptr<const tgta> const_tgta_ptr;
|
||||
typedef std::shared_ptr<const tgta_explicit> const_tgta_explicit_ptr;
|
||||
typedef std::shared_ptr<const twa> const_twa_ptr;
|
||||
typedef std::shared_ptr<const twa_graph> const_twa_graph_ptr;
|
||||
typedef std::shared_ptr<const twa_product> const_twa_product_ptr;
|
||||
typedef std::shared_ptr<const twa_run> const_twa_run_ptr;
|
||||
typedef std::shared_ptr<emptiness_check> emptiness_check_ptr;
|
||||
typedef std::shared_ptr<emptiness_check_result> emptiness_check_result_ptr;
|
||||
typedef std::shared_ptr<fair_kripke> fair_kripke_ptr;
|
||||
typedef std::shared_ptr<kripke_explicit> kripke_explicit_ptr;
|
||||
typedef std::shared_ptr<kripke_graph> kripke_graph_ptr;
|
||||
typedef std::shared_ptr<kripke> kripke_ptr;
|
||||
typedef std::shared_ptr<parsed_aut> parsed_aut_ptr;
|
||||
typedef std::shared_ptr<taa_tgba_formula> taa_tgba_formula_ptr;
|
||||
typedef std::shared_ptr<taa_tgba_string> taa_tgba_string_ptr;
|
||||
typedef std::shared_ptr<ta_explicit> ta_explicit_ptr;
|
||||
typedef std::shared_ptr<ta_product> ta_product_ptr;
|
||||
typedef std::shared_ptr<ta> ta_ptr;
|
||||
typedef std::shared_ptr<tgta_explicit> tgta_explicit_ptr;
|
||||
typedef std::shared_ptr<tgta> tgta_ptr;
|
||||
typedef std::shared_ptr<twa_graph> twa_graph_ptr;
|
||||
typedef std::shared_ptr<twa_product> twa_product_ptr;
|
||||
typedef std::shared_ptr<twa_run> twa_run_ptr;
|
||||
typedef std::shared_ptr<twa> twa_ptr;
|
||||
#+end_example
|
||||
|
||||
You should update any =foo*= to =foo_ptr= if it appears in this list,
|
||||
and remove any explicit call to =delete=. Additionally, if =foo= is a
|
||||
class, there is usually a =make_foo(...)= function that calls
|
||||
=std::make_shared<foo>(...)=.
|
||||
|
||||
As an example of usage, see [[file:tut22.org::#cpp][this example of creating an automaton
|
||||
explicitly]] where =spot::make_bdd_dict()= is used to create a BDD
|
||||
dictionary that is then passed to =spot::make_twa_graph()=.
|
||||
|
||||
* The =twa= class replaces =tgba=
|
||||
:PROPERTIES:
|
||||
:CUSTOM_ID: tgba-twa
|
||||
:END:
|
||||
|
||||
The change has several implications besides just the changing the
|
||||
name:
|
||||
|
||||
- =twa= can represent a larger class of automata than =tgba= could,
|
||||
since [[file:concepts.org::#acceptance-condition][the acceptance condition can be arbitrarily complex]].
|
||||
Algorithm that used to input =tgba= can be either generalized to
|
||||
handle those larger acceptance conditions, or restricted to
|
||||
generalized Büchi acceptance. The typical way to ensure
|
||||
that an =input= automaton has generalized Büchi acceptance is
|
||||
#+BEGIN_SRC c++
|
||||
if (!input->acc().is_generalized_buchi())
|
||||
throw std::runtime_error
|
||||
("myalgorithm() can only works with generalized Büchi acceptance");
|
||||
#+END_SRC
|
||||
|
||||
- Some methods of the =tgba= class have been removed. If you
|
||||
wrote a subclass, you may simply remove the following methods:
|
||||
- =compute_support_conditions()=,
|
||||
- =compute_support_variables()=,
|
||||
- =transition_annotation()=,
|
||||
- =neg_acceptance_conditions()=.
|
||||
|
||||
- The =succ_iter()= method lost its last two (optional) arguments.
|
||||
|
||||
- The badly named =number_of_acceptance_conditions()= has been renamed
|
||||
to =num_sets()=.
|
||||
|
||||
- The =tgba_succ_iterator= class was renamed to =twa_succ_iterator=, and
|
||||
its interface was changed:
|
||||
- =current_state()=, =current_condition()=, and
|
||||
=current_acceptance_conditions()= are now named respectively
|
||||
=dst()=, =cond()=, =acc()=.
|
||||
- the =first()= and =next()= method now return a Boolean that
|
||||
indicates whether we moved to a new successor (=true=), or reached
|
||||
the end of the list of successors (=false=). This return value
|
||||
should be the same as what =!done()= would return, and can be used
|
||||
to avoid some costly calls to the =done()= virtual function.
|
||||
|
||||
- The =twa::release_iter()= method allow iterators to be recycled.
|
||||
Each =twa= now contains a mutable field =iter_cache_= where
|
||||
=release_iter()= stores the last returned iterator. If this field
|
||||
is not equal to =nullptr=, then =succ_iter()= can use it to allocate
|
||||
a new iterator more efficiently.
|
||||
|
||||
In the code for =succ_iter()=, instead of:
|
||||
#+BEGIN_SRC C++
|
||||
// ...
|
||||
return new my_iterator(arg1, arg2, arg3);
|
||||
#+END_SRC
|
||||
we can now have
|
||||
#+BEGIN_SRC C++
|
||||
// ...
|
||||
if (iter_cache_)
|
||||
{
|
||||
my_iterator* it = down_cast<my_iterator*>(iter_cache_);
|
||||
iter_cache_ = nullptr;
|
||||
// Some method to change the member that need changing.
|
||||
// (Here we assume that arg2 is the same for all iterators
|
||||
// built on this automaton.)
|
||||
it->recycle(arg1, arg3);
|
||||
return it;
|
||||
}
|
||||
return new my_iterator(arg1, arg2, arg3);
|
||||
#+END_SRC
|
||||
|
||||
So not only do we save the calls to =new= and =delete=, but we also
|
||||
save the time it takes to construct the objects (including setting
|
||||
up the virtual table), and via a =recycle()= method that has to be
|
||||
added to the iterator, we update only the attributes that needs to
|
||||
be updated (for instance if the iterator contains a pointer back to
|
||||
the automaton, this pointer requires no update when the iterator is
|
||||
recycled).
|
||||
|
||||
#+BEGIN_caveat
|
||||
The iterator stored in =twa::iter_cache_= is destroyed by
|
||||
=twa::~twa()=. In some case, this is too late. For instance the
|
||||
class =twa_product= uses a custom memory pool to allocate new
|
||||
iterators more efficiently, and this memory pool is destroyed in
|
||||
=twa_product::~twa_product()=. In this case, referencing
|
||||
=twa::iter_cache_= for its deletion in =twa::~tgba()= would be
|
||||
incorrect: it has to be done in =twa_product::~twa_product()=
|
||||
before destroying the pool.
|
||||
#+END_caveat
|
||||
|
||||
|
||||
For a TGBA =aut=, and a state =s=, the original way to loop over the
|
||||
successors of =s= was:
|
||||
#+BEGIN_SRC C++
|
||||
tgba_succ_iterator* i = aut->succ_iter(s);
|
||||
for (i->first(); !i->done(); i->next())
|
||||
{
|
||||
// use i->current_state()
|
||||
// i->current_condition()
|
||||
// i->current_acceptance_conditions()
|
||||
}
|
||||
delete i;
|
||||
#+END_SRC
|
||||
|
||||
While the above would still run after a few renamings, it can now be
|
||||
written more efficiently as:
|
||||
|
||||
#+BEGIN_SRC C++
|
||||
twa_succ_iterator* i = aut->succ_iter(s);
|
||||
if (i->first())
|
||||
do
|
||||
{
|
||||
// use i->dst()
|
||||
// i->cond()
|
||||
// i->acc()
|
||||
}
|
||||
while (i->next());
|
||||
aut->release_iter(i);
|
||||
#+END_SRC
|
||||
|
||||
If the original code did $1$ virtual call to =first()=, $n+1$ virtual
|
||||
calls to =done()=, and $n$ virtual calls to =next()=, the new version
|
||||
do as many calls to =first()= and =done()= while avoiding all the
|
||||
calls to =done()=. Furthermore the call =release_iter()= makes it
|
||||
possible for the next call to =succ_iter()= to reuse the same
|
||||
iterator.
|
||||
|
||||
Because the the above loop is quite common we also have some syntactic
|
||||
sugar via the new =succ()= method that returns a fake container with
|
||||
=begin()= and =end()= methods so that this works:
|
||||
|
||||
#+BEGIN_SRC C++
|
||||
for (auto i: aut->succ(s))
|
||||
{
|
||||
// use i->dst()
|
||||
// i->cond()
|
||||
// i->acc()
|
||||
}
|
||||
#+END_SRC
|
||||
|
||||
- There should now be very few cases where it is necessary to call
|
||||
methods of the BDD dictionary attached to a =twa=. Registering
|
||||
the atomic proposition used by a =twa= should now be done via the
|
||||
=register_ap()= or =copy_ap_of()= methods. Accessing all
|
||||
registered propositions is achievable with =ap()= or =ap_vars()=.
|
||||
All propositions registered by an automaton are automatically
|
||||
unregistered when the automaton is destroyed.
|
||||
|
||||
* Various renamings
|
||||
|
||||
:PROPERTIES:
|
||||
:CUSTOM_ID: renamings
|
||||
:END:
|
||||
|
||||
The following is a non-exhaustive list of functions or classes that
|
||||
have been renamed.
|
||||
|
||||
| old name | new name | comment |
|
||||
|-------------------------------------------------------+---------------------------------------------+----------------------------------------------|
|
||||
| ~dstar_parse()~ | ~parse_aut()~ | single parser for all automata |
|
||||
| ~dtgba_complement()~ | ~dtwa_complement()~ | |
|
||||
| ~dupexp_bfs()~ | | deleted |
|
||||
| ~dupexp_dfs()~ | ~copy()~ | |
|
||||
| ~format_parse_aut_errors()~ | ~parsed_aut::format_errors()~ | |
|
||||
| ~hoaf_reachable()~ | ~print_hoa()~ | |
|
||||
| ~is_guarantee_automaton()~ | ~is_terminal_automaton()~ | |
|
||||
| ~kripke_parse()~ | ~parse_aut()~ | single parser for all automata |
|
||||
| ~kripke_save_reachable()~ | ~print_hoa()~ | adhoc output format replaced by HOA |
|
||||
| ~kripke_save_reachable_renumbered()~ | ~print_hoa()~ | adhoc output format replaced by HOA |
|
||||
| ~lbtt_parse()~ | ~parse_aut()~ | single parser for all automata |
|
||||
| ~lbtt_reachable()~ | ~print_lbtt()~ | |
|
||||
| ~ltl::formula::is_X_free()~ | ~formula::is_syntactic_stutter_invariant()~ | |
|
||||
| ~ltl::ltl_simplifier~ | ~tl_simplifier~ | |
|
||||
| ~ltl::parse_boolean()~ | ~parse_infix_boolean()~ | |
|
||||
| ~ltl::parse_lbt()~ | ~parse_prefix_ltl()~ | |
|
||||
| ~ltl::parse()~ | ~parse_infix_psl()~ | |
|
||||
| ~ltl::parse_sere()~ | ~parse_infix_sere()~ | |
|
||||
| ~ltl::to_latex_string()~ | ~print_latex_psl()~ | also ~str_latex_psl()~ |
|
||||
| ~ltl::to_lbt_string()~ | ~print_lbt_ltl()~ | also ~str_lbt_ltl()~ |
|
||||
| ~ltl::to_sclatex_string()~ | ~print_sclatex_psl()~ | also ~str_sclatex_psl()~ |
|
||||
| ~ltl::to_spin_string()~ | ~print_spin_ltl()~ | also ~str_spin_ltl()~ |
|
||||
| ~ltl::to_string()~ | ~print_psl()~, ~print_sere()~ | also ~str_psl()~ or ~str_sere()~ |
|
||||
| ~ltl::to_ut8_string()~ | ~print_utg8_psl()~, ~print_utf8_sere()~ | also ~str_utf8_psl()~ or ~str_utf8_sere()~ |
|
||||
| ~ltl::to_wring_string()~ | ~print_wring_ltl()~ | also ~str_wring_ltl()~ |
|
||||
| ~neverclaim_parse()~ | ~parse_aut()~ | single parser for all automata |
|
||||
| ~never_claim_reachable()~ | ~print_never_claim()~ | |
|
||||
| ~print_tgba_run()~ | ~tgba_run::operator<<()~ | |
|
||||
| ~reduce_run()~ | ~twa_run::reduce()~ | |
|
||||
| ~replay_tgba_run()~ | ~twa_run::replay()~ | |
|
||||
| ~scc_map~ | ~scc_info~ | new implementation restricted to ~twa_graph~ |
|
||||
| ~ta_succ_iterator::current_acceptance_conditions()~ | ~ta_succ_iterator::acc()~ | |
|
||||
| ~ta_succ_iterator::current_condition()~ | ~ta_succ_iterator::cond()~ | |
|
||||
| ~ta_succ_iterator::current_state()~ | ~ta_succ_iterator::dst()~ | |
|
||||
| ~tgba~ | ~twa~ | |
|
||||
| ~tgba_explicit_formula~ | | deleted |
|
||||
| ~tgba_explicit_number~ | ~twa_graph~ | new implementation |
|
||||
| ~tgba_explicit_string~ | | deleted |
|
||||
| ~tgba_parse()~ | ~parse_aut()~ | single parser for all automata |
|
||||
| ~tgba_run_to_tgba()~ | ~twa_run::as_twa()~ | |
|
||||
| ~tgba_run~ | ~twa_run~ | |
|
||||
| ~tgba_save_reachable()~ | ~print_hoa()~ | adhoc output format replaced by HOA |
|
||||
| ~tgba_statistics::transitions()~ | ~twa_statistics::edges()~ | |
|
||||
| ~tgba_sub_statistics::sub_transitions()~ | ~twa_sub_statistics::transitions()~ | |
|
||||
| ~tgba_succ_iterator::current_acceptance_conditions()~ | ~twa_succ_iterator::acc()~ | |
|
||||
| ~tgba_succ_iterator::current_condition()~ | ~twa_succ_iterator::cond()~ | |
|
||||
| ~tgba_succ_iterator::current_state()~ | ~twa_succ_iterator::dst()~ | |
|
||||
Loading…
Add table
Add a link
Reference in a new issue