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

Minor fixes.

Browse source 
* src/misc/bddop.hh, src/tgba/taa.hh, src/tgbaalgos/ltl2taa.hh:
Fix sanity (incorrect include guard).
* src/tgba/tgbacomplement.cc, src/tgba/tgbacomplement.hh:
Copyright 2009.
* src/tgbaalgos/eltl2tgba_lacim.cc: Use abbreviations.
* src/tgbatest/taa.cc: Fix it.
This commit is contained in:
Damien Lefortier 2009-10-16 17:00:46 +02:00
parent 627b667712
commit 84060b49e5
8 changed files with 70 additions and 36 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/tgbatest/taa.cc
View file

@ -24,29 +24,9 @@
#include "misc/hash.hh"
#include "ltlenv/defaultenv.hh"
#include "ltlast/allnodes.hh"
#include "tgbaalgos/dotty.hh"
#include "tgba/taa.hh"
typedef Sgi::hash_set<
const spot::state*, spot::state_ptr_hash, spot::state_ptr_equal
> mset;
void
dfs(spot::taa* a, const spot::state* s, mset& m)
{
if (m.find(s) != m.end())
return;
m.insert(s);
spot::tgba_succ_iterator* i = a->succ_iter(s);
assert(i);
for (i->first(); !i->done(); i->next())
{
std::cout << a->format_state(i->current_state()) << std::endl;
dfs(a, i->current_state(), m);
}
delete i;
}
int
main()
{
@ -70,11 +50,12 @@ main()
a->add_condition(t2, e.require("b"));
a->add_condition(t3, e.require("c"));
mset m;
spot::state* init = a->get_init_state();
dfs(a, init, m);
spot::dotty_reachable(std::cout, a);
delete init;
delete a;
delete dict;
assert(spot::ltl::atomic_prop::instance_count() == 0);
assert(spot::ltl::unop::instance_count() == 0);
assert(spot::ltl::binop::instance_count() == 0);
assert(spot::ltl::multop::instance_count() == 0);
}