diff --git a/NEWS b/NEWS index 9e9755f1f..a855ed55f 100644 --- a/NEWS +++ b/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: diff --git a/doc/Makefile.am b/doc/Makefile.am index f03c24110..2c8e97eb2 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -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 \ diff --git a/doc/org/index.org b/doc/org/index.org index 51725fb4b..d79945db9 100644 --- a/doc/org/index.org +++ b/doc/org/index.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 diff --git a/doc/org/spot.css b/doc/org/spot.css index 12c526e38..49ca7598d 100644 --- a/doc/org/spot.css +++ b/doc/org/spot.css @@ -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} diff --git a/doc/org/tut22.org b/doc/org/tut22.org index ac529d7aa..da6ca6d7f 100644 --- a/doc/org/tut22.org +++ b/doc/org/tut22.org @@ -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 diff --git a/doc/org/upgrade2.org b/doc/org/upgrade2.org new file mode 100644 index 000000000..e7e07754d --- /dev/null +++ b/doc/org/upgrade2.org @@ -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 + #include +#+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 // the new name of tgba/tgba.hh + #include // 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=. 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_ptr; +typedef std::shared_ptr const_fair_kripke_ptr; +typedef std::shared_ptr const_kripke_ptr; +typedef std::shared_ptr const_kripke_explicit_ptr; +typedef std::shared_ptr const_parsed_aut_ptr; +typedef std::shared_ptr const_taa_tgba_formula_ptr; +typedef std::shared_ptr const_taa_tgba_string_ptr; +typedef std::shared_ptr const_ta_ptr; +typedef std::shared_ptr const_ta_explicit_ptr; +typedef std::shared_ptr const_ta_product_ptr; +typedef std::shared_ptr const_tgta_ptr; +typedef std::shared_ptr const_tgta_explicit_ptr; +typedef std::shared_ptr const_twa_ptr; +typedef std::shared_ptr const_twa_graph_ptr; +typedef std::shared_ptr const_twa_product_ptr; +typedef std::shared_ptr const_twa_run_ptr; +typedef std::shared_ptr emptiness_check_ptr; +typedef std::shared_ptr emptiness_check_result_ptr; +typedef std::shared_ptr fair_kripke_ptr; +typedef std::shared_ptr kripke_explicit_ptr; +typedef std::shared_ptr kripke_graph_ptr; +typedef std::shared_ptr kripke_ptr; +typedef std::shared_ptr parsed_aut_ptr; +typedef std::shared_ptr taa_tgba_formula_ptr; +typedef std::shared_ptr taa_tgba_string_ptr; +typedef std::shared_ptr ta_explicit_ptr; +typedef std::shared_ptr ta_product_ptr; +typedef std::shared_ptr ta_ptr; +typedef std::shared_ptr tgta_explicit_ptr; +typedef std::shared_ptr tgta_ptr; +typedef std::shared_ptr twa_graph_ptr; +typedef std::shared_ptr twa_product_ptr; +typedef std::shared_ptr twa_run_ptr; +typedef std::shared_ptr 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(...)=. + +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(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()~ | |