From 8ce39e09b2c985fd607c5aacbab055e6bc265ff8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 6 Mar 2011 10:50:26 +0100 Subject: [PATCH] Augment dve2check to perform LTL model checking. * iface/dve2/dve2check.cc: Add many option to perform emptiness check and other debugging tasks. --- ChangeLog | 7 + iface/dve2/dve2check.cc | 291 ++++++++++++++++++++++++++++++++++++---- 2 files changed, 272 insertions(+), 26 deletions(-) diff --git a/ChangeLog b/ChangeLog index ee08a02e6..36d2c33e8 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2011-03-06 Alexandre Duret-Lutz + + Augment dve2check to perform LTL model checking. + + * iface/dve2/dve2check.cc: Add many option to perform + emptiness check and other debugging tasks. + 2011-03-05 Alexandre Duret-Lutz Teach the DVE2 interface about enumerated types. diff --git a/iface/dve2/dve2check.cc b/iface/dve2/dve2check.cc index 9f6bb330f..2985aae6f 100644 --- a/iface/dve2/dve2check.cc +++ b/iface/dve2/dve2check.cc @@ -22,45 +22,284 @@ #include "tgbaalgos/dotty.hh" #include "ltlenv/defaultenv.hh" #include "ltlast/allnodes.hh" +#include "ltlparse/public.hh" +#include "tgbaalgos/ltl2tgba_fm.hh" +#include "tgbaalgos/sccfilter.hh" +#include "tgbaalgos/emptiness.hh" +#include "tgbaalgos/reducerun.hh" +#include "tgba/tgbaproduct.hh" +#include "misc/timer.hh" +#include + +void +syntax(char* prog) +{ + // Display the supplied name unless it appears to be a libtool wrapper. + char* slash = strrchr(prog, '/'); + if (slash && (strncmp(slash + 1, "lt-", 3) == 0)) + prog = slash + 4; + + std::cerr << "usage: " << prog << " [options] model formula" << std::endl + << std::endl + << "Options:" << std::endl + << " -e[ALGO] run emptiness check, expect an accepting run" + << std::endl + << " -E[ALGO] run emptiness check, expect no accepting run" + << std::endl + << " -C compute an accepting run (Counterexample) if it exists" + << std::endl + << " -gf output the automaton of the formula in dot format" + << std::endl + << " -gm output the model state-space in dot format" + << std::endl + << " -gp output the product state-space in dot format" + << std::endl + << " -T time the different phases of the execution" + << std::endl; + + exit(1); +} int main(int argc, char **argv) { + spot::timer_map tm; + + bool use_timer = false; + + enum { DotFormula, DotModel, DotProduct, EmptinessCheck } + output = EmptinessCheck; + bool accepting_run = false; + bool expect_counter_example = false; + + const char* echeck_algo = "Cou99"; + + int dest = 1; + int n = argc; + for (int i = 1; i < n; ++i) + { + char* opt = argv[i]; + if (*opt == '-') + { + switch (*++opt) + { + case 'C': + accepting_run = true; + break; + case 'e': + case 'E': + { + echeck_algo = opt + 1; + if (!*echeck_algo) + echeck_algo = "Cou99"; + + expect_counter_example = (*opt == 'E'); + output = EmptinessCheck; + break; + } + case 'g': + switch (opt[1]) + { + case 'm': output = DotModel; break; + case 'p': output = DotProduct; break; + case 'f': output = DotFormula; break; + default: + goto error; + } + break; + case 'T': + use_timer = true; + break; + default: + error: + std::cerr << "Unknown option `" << argv[i] << "'." << std::endl; + exit(1); + } + --argc; + } + else + { + argv[dest++] = argv[i]; + } + } + + if (argc != 3) + syntax(argv[0]); + spot::ltl::default_environment& env = spot::ltl::default_environment::instance(); spot::ltl::atomic_prop_set ap; - - if (argc <= 1) - { - std::cerr << "usage: " << argv[0] << " model" << std::endl; - exit(1); - } - - while (argc > 2) - { - ap.insert(static_cast - (env.require(argv[argc - 1]))); - --argc; - } - spot::bdd_dict* dict = new spot::bdd_dict(); - spot::kripke* a = spot::load_dve2(argv[1], dict, &ap, true); + spot::kripke* model = 0; + spot::tgba* prop = 0; + spot::tgba* product = 0; + spot::emptiness_check_instantiator* echeck_inst = 0; + int exit_code = 0; + spot::ltl::formula* f = 0; - for (spot::ltl::atomic_prop_set::const_iterator it = ap.begin(); - it != ap.end(); ++it) - (*it)->destroy(); - ap.clear(); - - if (!a) + if (output == EmptinessCheck) { - delete dict; - exit(1); + const char* err; + echeck_inst = + spot::emptiness_check_instantiator::construct(echeck_algo, &err); + if (!echeck_inst) + { + std::cerr << "Failed to parse argument of -e/-E near `" + << err << "'" << std::endl; + exit_code = 1; + goto safe_exit; + } } - spot::dotty_reachable(std::cout, a); + tm.start("parsing formula"); + { + spot::ltl::parse_error_list pel; + f = spot::ltl::parse(argv[2], pel, env, false); + exit_code = spot::ltl::format_parse_errors(std::cerr, argv[2], pel); + } + tm.stop("parsing formula"); - delete a; + if (exit_code) + goto safe_exit; + + atomic_prop_collect(f, &ap); + + + if (output != DotFormula) + { + tm.start("loading dve2"); + model = spot::load_dve2(argv[1], dict, &ap, true); + tm.stop("loading dve2"); + + if (!model) + { + exit_code = 1; + goto safe_exit; + } + + if (output == DotModel) + { + tm.start("dotty output"); + spot::dotty_reachable(std::cout, model); + tm.stop("dotty output"); + goto safe_exit; + } + } + + + tm.start("translating formula"); + prop = spot::ltl_to_tgba_fm(f, dict); + tm.stop("translating formula"); + + tm.start("reducing A_f w/ SCC"); + { + spot::tgba* aut_scc = spot::scc_filter(prop, true); + delete prop; + prop = aut_scc; + } + tm.stop("reducing A_f w/ SCC"); + + if (output == DotFormula) + { + tm.start("dotty output"); + spot::dotty_reachable(std::cout, prop); + tm.stop("dotty output"); + goto safe_exit; + } + + product = new spot::tgba_product(model, prop); + + if (output == DotProduct) + { + tm.start("dotty output"); + spot::dotty_reachable(std::cout, product); + tm.stop("dotty output"); + goto safe_exit; + } + + + assert(echeck_inst); + + { + spot::emptiness_check* ec = echeck_inst->instantiate(product); + bool search_many = echeck_inst->options().get("repeated"); + assert(ec); + do + { + tm.start("running emptiness check"); + spot::emptiness_check_result* res = ec->check(); + tm.stop("running emptiness check"); + + ec->print_stats(std::cout); + + if (expect_counter_example == !res && + (!expect_counter_example || ec->safe())) + exit_code = 1; + + if (!res) + { + std::cout << "no accepting run found"; + if (!ec->safe() && expect_counter_example) + { + std::cout << " even if expected" << std::endl; + std::cout << "this may be due to the use of the bit" + << " state hashing technique" << std::endl; + std::cout << "you can try to increase the heap size " + << "or use an explicit storage" + << std::endl; + } + std::cout << std::endl; + break; + } + else if (accepting_run) + { + + tm.start("computing accepting run"); + spot::tgba_run* run = res->accepting_run(); + tm.stop("computing accepting run"); + + if (!run) + { + std::cout << "an accepting run exists" << std::endl; + } + else + { + tm.start("reducing accepting run"); + spot::tgba_run* redrun = + spot::reduce_run(res->automaton(), run); + tm.stop("reducing accepting run"); + delete run; + run = redrun; + + tm.start("printing accepting run"); + spot::print_tgba_run(std::cout, product, run); + tm.stop("printing accepting run"); + } + delete run; + } + else + { + std::cout << "an accepting run exists " + << "(use -C to print it)" << std::endl; + } + delete res; + } + while (search_many); + delete ec; + } + + safe_exit: + delete echeck_inst; + delete product; + delete prop; + delete model; + if (f) + f->destroy(); + delete dict; + + if (use_timer) + tm.print(std::cout); spot::ltl::atomic_prop::dump_instances(std::cerr); spot::ltl::unop::dump_instances(std::cerr); @@ -73,5 +312,5 @@ main(int argc, char **argv) assert(spot::ltl::multop::instance_count() == 0); assert(spot::ltl::automatop::instance_count() == 0); - delete dict; + exit(exit_code); }