diff --git a/ChangeLog b/ChangeLog index 23e1a90d7..eee80c294 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,15 @@ 2003-10-23 Alexandre Duret-Lutz + Merge emptinesscheckexplicit into ltl2tgba. + * src/tgbatest/Makefile.am (check_PROGRAMS): Remove + emptinesscheckexplicit. + (emptinesscheckexplicit_SOURCES): Remove. + (TESTS): Replace emptinesscheckexplicit.test by emptchke.test. + * src/tgbatest/emptinesscheckexplicit.cc, + src/tgbatest/emptinesscheckexplicit.test: Delete. + * src/tgbatest/empchke.test: New file. + * src/tgbatest/ltl2tgba.cc: Add support for -X. + Merge emptiness-checks tests into ltl2tgba. * src/tgbatest/Makefile (check_PRORGRAMS): Remove emptinesscheck and ltlmagic. diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 6dc63a52b..22631fac2 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -6,7 +6,6 @@ check_SCRIPTS = defs check_PROGRAMS = \ bddprod \ explicit \ - emptinesscheckexplicit \ explprod \ ltl2tgba \ ltlprod \ @@ -18,7 +17,6 @@ check_PROGRAMS = \ # Keep this sorted alphabetically. bddprod_SOURCES = ltlprod.cc bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT -emptinesscheckexplicit_SOURCES = emptinesscheckexplicit.cc explicit_SOURCES = explicit.cc explprod_SOURCES = explprod.cc ltl2tgba_SOURCES = ltl2tgba.cc @@ -43,7 +41,7 @@ TESTS = \ tripprod.test \ mixprod.test \ emptchk.test \ - emptinesscheckexplicit.test \ + emptchke.test \ spotlbtt.test EXTRA_DIST = $(TESTS) diff --git a/src/tgbatest/emptinesscheckexplicit.test b/src/tgbatest/emptchke.test similarity index 72% rename from src/tgbatest/emptinesscheckexplicit.test rename to src/tgbatest/emptchke.test index 29555f314..b9a6591ba 100755 --- a/src/tgbatest/emptinesscheckexplicit.test +++ b/src/tgbatest/emptchke.test @@ -11,4 +11,5 @@ s1, "s2", a!b, c d; "state 3", s1,,; EOF -./emptinesscheckexplicit input > stdout +./ltl2tgba -e -X input +./ltl2tgba -m -X input diff --git a/src/tgbatest/emptinesscheckexplicit.cc b/src/tgbatest/emptinesscheckexplicit.cc deleted file mode 100644 index 90f77bbd9..000000000 --- a/src/tgbatest/emptinesscheckexplicit.cc +++ /dev/null @@ -1,46 +0,0 @@ -#include -#include "tgbaparse/public.hh" -#include "tgba/tgbaexplicit.hh" -#include "tgbaalgos/dotty.hh" -#include "tgbaalgos/emptinesscheck.hh" - -void -syntax(char* prog) -{ - std::cerr << prog << " [-d] filename" << std::endl; - exit(2); -} - -int -main(int argc, char** argv) -{ - int exit_code = 0; - - if (argc < 2) - syntax(argv[0]); - - bool debug = false; - int filename_index = 1; - - if (!strcmp(argv[1], "-d")) - { - debug = true; - if (argc < 3) - syntax(argv[0]); - filename_index = 2; - } - - spot::ltl::environment& env(spot::ltl::default_environment::instance()); - spot::tgba_parse_error_list pel; - spot::bdd_dict* dict = new spot::bdd_dict(); - spot::tgba_explicit* a = spot::tgba_parse(argv[filename_index], - pel, dict, env, debug); - spot::emptiness_check empty_check; - - if (spot::format_tgba_parse_errors(std::cerr, pel)) - return 2; -bool emptiness = empty_check.tgba_emptiness_check(a); - empty_check.counter_example(a); - delete a; - return 0; -} diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 5c8e447cc..bc2e6abbf 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -13,12 +13,14 @@ #include "tgba/tgbatba.hh" #include "tgbaalgos/magic.hh" #include "tgbaalgos/emptinesscheck.hh" +#include "tgbaparse/public.hh" void syntax(char* prog) { std::cerr << "Usage: "<< prog << " [OPTIONS...] formula" << std::endl << " "<< prog << " -F [OPTIONS...] file" << std::endl + << " "<< prog << " -X [OPTIONS...] file" << std::endl << std::endl << "Options:" << std::endl << " -a display the accepting_conditions BDD, not the " @@ -45,6 +47,8 @@ syntax(char* prog) << " -R same as -r, but as a set" << std::endl << " -t display reachable states in LBTT's format" << std::endl << " -v display the BDD variables used by the automaton" + << std::endl + << " -X do compute an automaton, read it from a file" << std::endl; exit(2); } @@ -63,6 +67,7 @@ main(int argc, char** argv) enum { None, Couvreur, MagicSearch } echeck = None; bool magic_many = false; bool expect_counter_example = false; + bool from_file = false; for (;;) { @@ -145,6 +150,10 @@ main(int argc, char** argv) { output = 5; } + else if (!strcmp(argv[formula_index], "-X")) + { + from_file = true; + } else { break; @@ -174,24 +183,36 @@ main(int argc, char** argv) } spot::ltl::environment& env(spot::ltl::default_environment::instance()); - spot::ltl::parse_error_list pel; - spot::ltl::formula* f = spot::ltl::parse(input, pel, env, debug_opt); - - exit_code = spot::ltl::format_parse_errors(std::cerr, input, pel); - spot::bdd_dict* dict = new spot::bdd_dict(); - if (f) + + spot::ltl::formula* f = 0; + if (!from_file) + { + spot::ltl::parse_error_list pel; + f = spot::ltl::parse(input, pel, env, debug_opt); + exit_code = spot::ltl::format_parse_errors(std::cerr, input, pel); + } + if (f || from_file) { spot::tgba_bdd_concrete* concrete = 0; spot::tgba* to_free = 0; spot::tgba* a = 0; - if (fm_opt) - to_free = a = spot::ltl_to_tgba_fm(f, dict); + if (from_file) + { + spot::tgba_parse_error_list pel; + to_free = a = spot::tgba_parse(input, pel, dict, env, debug_opt); + if (spot::format_tgba_parse_errors(std::cerr, pel)) + return 2; + } else - to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict); - - spot::ltl::destroy(f); + { + if (fm_opt) + to_free = a = spot::ltl_to_tgba_fm(f, dict); + else + to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict); + spot::ltl::destroy(f); + } spot::tgba_tba_proxy* degeneralized = 0; if (degeneralize_opt)