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

* src/tgbatest/ltl2tgba.cc: Support -v.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2003-06-25 09:44:29 +00:00
parent cdb17c5486
commit f1af8f96bf
2 changed files with 14 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,3 +1,7 @@
2003-06-25 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgbatest/ltl2tgba.cc: Support -v.
2003-06-24 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgbatest/ltl2tgba.cc (syntax): Fix usage message.

11
src/tgbatest/ltl2tgba.cc
View file

@ -21,7 +21,9 @@ syntax(char* prog)
<< std::endl
<< " -r display the relation BDD, not the reachability graph"
<< std::endl
<< " -R same as -r, but as a set" << std::endl;
<< " -R same as -r, but as a set" << std::endl
<< " -v display the BDD variables used by the automaton"
<< std::endl;
exit(2);
}
@ -66,6 +68,10 @@ main(int argc, char** argv)
{
output = 3;
}
else if (!strcmp(argv[formula_index], "-v"))
{
output = 5;
}
else
{
break;
@ -108,6 +114,9 @@ main(int argc, char** argv)
spot::bdd_print_set(std::cout, a.get_dict(),
a.get_core_data().accepting_conditions);
break;
case 5:
a.get_dict().dump(std::cout);
break;
default:
assert(!"unknown output option");
}