From f1af8f96bf446af8af5b2d072c418944ae5f1a18 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 25 Jun 2003 09:44:29 +0000 Subject: [PATCH] * src/tgbatest/ltl2tgba.cc: Support -v. --- ChangeLog | 4 ++++ src/tgbatest/ltl2tgba.cc | 11 ++++++++++- 2 files changed, 14 insertions(+), 1 deletion(-) diff --git a/ChangeLog b/ChangeLog index b20d83e86..e3b27eb93 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,7 @@ +2003-06-25 Alexandre Duret-Lutz + + * src/tgbatest/ltl2tgba.cc: Support -v. + 2003-06-24 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc (syntax): Fix usage message. diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 5b0dfb6a4..8176cd367 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -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"); }