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

Add a verbose option to ltlsynt

Browse source 
* bin/ltlsynt.cc: implement it
This commit is contained in:
Maximilien Colange 2018-01-02 09:24:31 +01:00
parent bc2fa1a2a3
commit 5d80cc556c
1 changed files with 17 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

19
bin/ltlsynt.cc
View file

@ -53,7 +53,8 @@ enum
OPT_OUTPUT, OPT_OUTPUT,
OPT_PRINT, OPT_PRINT,
OPT_PRINT_AIGER, OPT_PRINT_AIGER,
OPT_REAL OPT_REAL,
OPT_VERBOSE
}; };
static const argp_option options[] = static const argp_option options[] =
@ -80,6 +81,8 @@ static const argp_option options[] =
"realizability only, do not compute a winning strategy", 0}, "realizability only, do not compute a winning strategy", 0},
{ "aiger", OPT_PRINT_AIGER, nullptr, 0, { "aiger", OPT_PRINT_AIGER, nullptr, 0,
"prints the winning strategy as an AIGER circuit", 0}, "prints the winning strategy as an AIGER circuit", 0},
{ "verbose", OPT_VERBOSE, nullptr, 0,
"verbose mode", -1 },
/**************************************************/ /**************************************************/
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
{ nullptr, 0, nullptr, 0, nullptr, 0 }, { nullptr, 0, nullptr, 0, nullptr, 0 },
@ -129,6 +132,7 @@ static solver const solver_types[] =
ARGMATCH_VERIFY(solver_args, solver_types); ARGMATCH_VERIFY(solver_args, solver_types);
static solver opt_solver = REC; static solver opt_solver = REC;
static bool verbose = false;
namespace namespace
{ {
@ -276,7 +280,6 @@ namespace
return aut; return aut;
} }
class ltl_processor final : public job_processor class ltl_processor final : public job_processor
{ {
private: private:
@ -300,6 +303,8 @@ namespace
timer.start(); timer.start();
auto aut = trans_.run(&f); auto aut = trans_.run(&f);
if (verbose)
std::cerr << "translating formula done" << std::endl;
bdd all_inputs = bddtrue; bdd all_inputs = bddtrue;
bdd all_outputs = bddtrue; bdd all_outputs = bddtrue;
for (unsigned i = 0; i < input_aps_.size(); ++i) for (unsigned i = 0; i < input_aps_.size(); ++i)
@ -318,10 +323,17 @@ namespace
unsigned v = aut->register_ap(spot::formula::ap(lowercase.str())); unsigned v = aut->register_ap(spot::formula::ap(lowercase.str()));
all_outputs &= bdd_ithvar(v); all_outputs &= bdd_ithvar(v);
} }
auto split = split_automaton(aut, all_inputs); auto split = split_automaton(aut, all_inputs);
if (verbose)
std::cerr << "split inputs and outputs done" << std::endl;
auto dpa = to_dpa(split); auto dpa = to_dpa(split);
if (verbose)
std::cerr << "determinization done" << std::endl;
auto owner = make_alternating_owner(dpa); auto owner = make_alternating_owner(dpa);
auto pg = spot::parity_game(dpa, owner); auto pg = spot::parity_game(dpa, owner);
if (verbose)
std::cerr << "parity game built" << std::endl;
timer.stop(); timer.stop();
if (opt_print_pg) if (opt_print_pg)
@ -425,6 +437,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_PRINT_AIGER: case OPT_PRINT_AIGER:
opt_print_aiger = true; opt_print_aiger = true;
break; break;
case OPT_VERBOSE:
verbose = true;
break;
} }
return 0; return 0;
} }