Augment dve2check to perform LTL model checking.
* iface/dve2/dve2check.cc: Add many option to perform emptiness check and other debugging tasks.
This commit is contained in:
Alexandre Duret-Lutz
parent
7b5879d26a
commit
8ce39e09b2
2 changed files with 272 additions and 26 deletions
|
|
@ -1,3 +1,10 @@
|
|||
2011-03-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||
|
||||
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 <adl@lrde.epita.fr>
|
||||
|
||||
Teach the DVE2 interface about enumerated types.
|
||||
|
|
|
|||
|
|
@ -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 <cstring>
|
||||
|
||||
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<spot::ltl::atomic_prop*>
|
||||
(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);
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue