alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgbaalgos/lbtt.cc: Typos.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2003-07-29 16:15:19 +00:00
parent 48c03b89b8
commit 60ef421dd5
4 changed files with 12 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,5 +1,9 @@
2003-07-29 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgbaalgos/lbtt.cc: Typos.
* lbtt/: Upgrade to lbtt 1.0.2.
* src/tgbatest/Makefile.am (check_PROGRAMS): Add tbalbtt.
(tbalbtt_SOURCES, tbalbtt_CXXFLAGS): New variables.
* src/tgbatest/spotlbtt.cc [TBA]: Build tba proxies conditionally.

10
src/tgbaalgos/lbtt.cc
View file

@ -12,7 +12,7 @@
namespace spot
{
// At some point we'll need to print an accepting set into LBTT's
// forma. LBTT expect numbered accepting sets, so first we'll
// format. LBTT expects numbered accepting sets, so first we'll
// number each accepting condition, and latter when we have to print
// them we'll just have to look up each of them.
class accepting_cond_splitter
@ -106,8 +106,8 @@ namespace spot
// Set of states yet to produce.
typedef std::set<state_acc_pair, state_acc_pair_less_than> todo_set;
// Each *source* car correspond to several state in the produced
// automate. A minmax_pair specify the range of such associated states.
// Each *source* state corresponds to several states in the produced
// automata. A minmax_pair specifies the range of such associated states.
typedef std::pair<unsigned, unsigned> minmax_pair;
typedef std::map<state*, minmax_pair, state_ptr_less_than> seen_map;
@ -145,7 +145,7 @@ namespace spot
acc_seen.insert(si->current_accepting_conditions());
}
// Order the creation of the supplementary initial state of needed.
// Order the creation of the supplementary initial state if needed.
// Use bddtrue as accepting condition because it cannot conflict
// with other (state, accepting cond) pairs in the maps.
if (init && acc_seen.size() > 1)
@ -229,7 +229,7 @@ namespace spot
os << state_number << " " << acs.count() << std::endl;
os << body.str();
// Finally delete all states used as keys in m:
// Finally delete all states used as keys in m.
for (seen_map::iterator i = seen.begin(); i != seen.end(); ++i)
delete i->first;
return os;

2
src/tgbaalgos/magic.cc
View file

@ -128,7 +128,7 @@ namespace spot
tstack_type::const_reverse_iterator ti;
os << "Prefix:" << std::endl;
const bdd_dict* d = a->get_dict();
for (i = stack.rbegin(), ti = tstack.rbegin();
for (i = stack.rbegin(), ti = tstack.rbegin();
i != stack.rend(); ++i, ++ti)
{
if (i->first.s->compare(x) == 0)

4
src/tgbatest/ltlmagic.cc
View file

@ -52,10 +52,10 @@ main(int argc, char** argv)
spot::ltl::destroy(f1);
spot::magic_search ms(a2);
if (ms.check())
{
do
do
ms.print_result (std::cout);
while (all_opt && ms.check());
}