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

tgbaexplicit: execute the test

Browse source 
* src/tgbatest/explicit2.test: New file.
* src/tgbatest/Makefile.am: Add it.
* src/tgbatest/explicit2.cc: Print the LTL formula as text.
This commit is contained in:
Alexandre Duret-Lutz 2012-04-12 17:54:20 +02:00
parent 37a6b601c1
commit 8269ae9cee
3 changed files with 51 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tgbatest/explicit2.cc
View file

@ -23,6 +23,7 @@
#include "ltlenv/defaultenv.hh"
#include "ltlast/allnodes.hh"
#include "ltlvisit/tostring.hh"
#include "tgba/tgbaexplicit.hh"
@ -60,7 +61,6 @@ create_tgba_explicit_number(bdd_dict* d)
state_explicit_number* s1 = tgba->add_state(51);
state_explicit_number* s2 = tgba->add_state(69);
state_explicit_number::transition* t =
tgba->create_transition(s1, s2);
(void) t;
@ -96,7 +96,7 @@ create_tgba_explicit_formula(bdd_dict* d, spot::ltl::default_environment& e)
for (it->first(); !it->done(); it->next())
{
state_explicit_formula* s = it->current_state();
std::cout << s->label() << std::endl;
to_string(s->label(), std::cout) << std::endl;
s->destroy();
}