Alexandre Duret-Lutz committed Mar 02, 2016 1 2 # -*- coding: utf-8 -*- #+TITLE: Upgrading from Spot 1.2.6  Alexandre Duret-Lutz committed May 10, 2016 3 #+DESCRIPTION: Help for upgrading code to Spot 2.0  Alexandre Duret-Lutz committed Mar 02, 2016 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 #+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.  Alexandre Duret-Lutz committed Aug 22, 2017 23  1. [[#cpp14][Spot now compiles using the C++14 standard]]. Compliant compiler  Alexandre Duret-Lutz committed Mar 02, 2016 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48  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  Alexandre Duret-Lutz committed Mar 08, 2017 49  (such as automata, BDD dictionaries, accepting runs) are now  Alexandre Duret-Lutz committed Mar 02, 2016 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76  [[#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.  Alexandre Duret-Lutz committed Apr 23, 2017 77  In particular the =tgba_explicit_*= family of classes  Alexandre Duret-Lutz committed Mar 02, 2016 78 79 80 81 82 83 84 85  (=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.  Alexandre Duret-Lutz committed Aug 22, 2017 86 * Upgrading to C++14  Alexandre Duret-Lutz committed Mar 02, 2016 87 88 89 90  :PROPERTIES: :CUSTOM_ID: cpp11 :END:  Alexandre Duret-Lutz committed Aug 22, 2017 91  Because Spot now relies on C++14 features, programs that use Spot  Alexandre Duret-Lutz committed Mar 02, 2016 92 93 94 95  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  Alexandre Duret-Lutz committed Aug 22, 2017 96  enabling C++14 is usually done by passing the option =-std=c++14=.  Alexandre Duret-Lutz committed Mar 02, 2016 97  In =g++= 6.0 the default C++ standard used is C++14, so passing  Alexandre Duret-Lutz committed Aug 22, 2017 98  =-std=c++14= is not necessary.  Alexandre Duret-Lutz committed Mar 02, 2016 99   Alexandre Duret-Lutz committed Aug 22, 2017 100 101  Upgrading from C++98, C++03 or C++11 to C++14 should be relatively smooth as the language is /mostly/ backward compatible.  Alexandre Duret-Lutz committed Mar 02, 2016 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264  * 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~ | |  Alexandre Duret-Lutz committed Jul 25, 2017 265 | ~tgbaalgos/dupexp.hh~ | ~spot/twaalgos/twagraph.hh~ | constructor of twa_graph |  Alexandre Duret-Lutz committed Mar 02, 2016 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 | ~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~ | |  Alexandre Duret-Lutz committed Jul 18, 2016 288 | ~tgbaalgos/projrun.hh~ | ~spot/twaalgos/emptiness.hh~ | use =twa_run::project()= since Spot 2.1 |  Alexandre Duret-Lutz committed Mar 02, 2016 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 | ~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~ | |  Thomas Medioni committed Apr 07, 2017 326 | ~tgba/tgbakvcomplement.hh~ | | use ~tgba_determinize()~ and ~dualize()~ |  Alexandre Duret-Lutz committed Mar 02, 2016 327 328 329 330 331 332 333 334 | ~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 |  Thomas Medioni committed Apr 07, 2017 335 | ~tgba/wdbacomp.hh~ | ~spot/twaalgos/dualize.hh~ | use ~dualize()~ instead |  Alexandre Duret-Lutz committed Mar 02, 2016 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 |------------------------------------+------------------------------------+--------------------------------------------------| | ~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  Alexandre Duret-Lutz committed Mar 03, 2016 463 464 465 - Some methods of the =tgba= class have been removed, include some pure virtual methods. If you wrote a subclass, you may simply remove the following methods:  Alexandre Duret-Lutz committed Mar 02, 2016 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486  - =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.  Alexandre Duret-Lutz committed Mar 03, 2016 487 488 489 490 491 492 - Membership to acceptance sets is now represented using a bit set (instead of BDDs). An T\omega{}A =aut= uses =aut->num_sets()= acceptance sets numbered from =0= to =aut->num_sets()-1=. The bit sets are implemented as instances of =spot::acc_cond::mark_t=, so they are also called "acceptance marks".  Alexandre Duret-Lutz committed Mar 02, 2016 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 - 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_) {  Alexandre Duret-Lutz committed Mar 03, 2016 509  my_iterator* it = static_cast(iter_cache_);  Alexandre Duret-Lutz committed Mar 02, 2016 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570  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  Alexandre Duret-Lutz committed Mar 03, 2016 571 does as many calls to =first()= and =done()= while avoiding all the  Alexandre Duret-Lutz committed Mar 02, 2016 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 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  Alexandre Duret-Lutz committed Mar 08, 2017 589 - Each =twa= now has a BDD dictionary, so the =get_dict()= method is  Alexandre Duret-Lutz committed Mar 03, 2016 590 591 592 593 594 595 596 597 598 599 600 601  implemented once for all in =twa=, and should not be implemented anymore in sub-classes. - 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 =twa::register_ap()= or =twa::copy_ap_of()= methods. Accessing all registered propositions is achievable with =twa::ap()= or =twa::ap_vars()=. All propositions registered by an automaton are automatically unregistered when the automaton is destroyed.  Alexandre Duret-Lutz committed Mar 02, 2016 602 603 604 605 606 607 608 609 610 * Various renamings :PROPERTIES: :CUSTOM_ID: renamings :END: The following is a non-exhaustive list of functions or classes that have been renamed.  Alexandre Duret-Lutz committed Mar 03, 2016 611 612 613 614 615 | old name | new name | comment | |-------------------------------------------------------------+---------------------------------------------+-----------------------------------------------------------| | ~dstar_parse()~ | ~parse_aut()~ | single parser for all automata | | ~dtgba_complement()~ | ~dtwa_complement()~ | | | ~dupexp_bfs()~ | | deleted |  Alexandre Duret-Lutz committed Jul 25, 2017 616 | ~dupexp_dfs()~ | ~make_twa_graph()~ | |  Alexandre Duret-Lutz committed Mar 03, 2016 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 | ~format_parse_aut_errors()~ | ~parsed_aut::format_errors()~ | | | ~emptiness_check_instantiator::construct()~ | ~make_emptiness_check_instantiator()~ | | | ~emptiness_check_instantiator::max_acceptance_conditions()~ | ~emptiness_check_instantiator::max_sets()~ | | | ~emptiness_check_instantiator::min_acceptance_conditions()~ | ~emptiness_check_instantiator::min_sets()~ | | | ~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::all_acceptance_conditions()~ | | use ~tgba::acc().accepting()~ or ~tgba::acc().all_sets()~ | | ~tgba::neg_acceptance_conditions()~ | | deleted | | ~tgba::number_of_acceptance_conditions()~ | ~tgba::num_sets()~ | | | ~tgba::support_conditions()~ | | deleted | | ~tgba::support_variables()~ | | deleted | | ~tgba_explicit_formula~ | | deleted | | ~tgba_explicit_number~ | ~twa_graph~ | new implementation | | ~tgba_explicit_string~ | | deleted | | ~tgba_parse()~ | ~parse_aut()~ | single parser for all automata |  Alexandre Duret-Lutz committed Mar 06, 2016 660 661 662 | ~tgba_reachable_iterator~ | ~twa_reachable_iterator~ | | | ~tgba_reachable_iterator_breadth_first~ | ~twa_reachable_iterator_breadth_first~ | | | ~tgba_reachable_iterator_depth_first~ | ~twa_reachable_iterator_depth_first~ | |  Alexandre Duret-Lutz committed Mar 03, 2016 663 664 665 666 667 668 669 670 | ~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()~ | |