lbtt.hh 1.26 KB
 Alexandre Duret-Lutz committed Jul 08, 2003 1 2 3 4 5 6 7 8 9 10 11 12 ``````#ifndef SPOT_TGBAALGOS_LBTT_HH # define SPOT_TGBAALGOS_LBTT_HH #include "tgba/tgba.hh" #include namespace spot { /// \brief Print reachable states in LBTT format. /// /// Note that LBTT expects an automaton with transition /// labeled by propositional formulae, and generalized `````` Alexandre Duret-Lutz committed Jul 09, 2003 13 `````` /// Büchi accepting conditions on \b states. This `````` Alexandre Duret-Lutz committed Jul 08, 2003 14 `````` /// is unlike our spot::tgba automata which put `````` Alexandre Duret-Lutz committed Jul 09, 2003 15 `````` /// both generalized accepting conditions and propositional `````` Alexandre Duret-Lutz committed Jul 09, 2003 16 `````` /// formulae) on \b transitions. `````` Alexandre Duret-Lutz committed Jul 08, 2003 17 `````` /// `````` Alexandre Duret-Lutz committed Jul 09, 2003 18 19 20 21 22 23 24 25 26 27 `````` /// This algorithm will therefore produce an automata where /// accepting conditions have been moved from each transition to /// previous state. In the worst case, doing so will multiply the /// number of states and transitions of the automata by /// 2^|Acc|. where |Acc| is the number of /// accepting conditions used by the automata. (It can be a bit /// more because LBTT allows only for one initial state: /// lbtt_reachable() may also have to create an additional state in /// case the source initial state had to be split.) You have been /// warned. `````` Alexandre Duret-Lutz committed Jul 08, 2003 28 29 30 31 32 33 34 `````` /// /// \param g The automata to print. /// \param os Where to print. std::ostream& lbtt_reachable(std::ostream& os, const tgba& g); } #endif // SPOT_TGBAALGOS_LBTT_HH``````