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

ltlsynt: fix syntax error handling

Browse source 
Fixes #477.

* bin/common_finput.cc (job_processor::process_string): Fix return
value.
* bin/ltlsynt.cc: Fix handling of syntax errors.  While we are here,
make sure game_info is destroyed before Spot's globals.
* tests/core/ltlsynt.test: Add a test case.
This commit is contained in:
Alexandre Duret-Lutz 2021-09-17 13:25:28 +02:00
parent 4710577dfe
commit cb3a833a8d
3 changed files with 80 additions and 69 deletions
Download patch file Download diff file Expand all files Collapse all files

4
bin/common_finput.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012-2017, 2019 Laboratoire de Recherche et // Copyright (C) 2012-2017, 2019, 2021 Laboratoire de Recherche et
// Développement de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -125,7 +125,7 @@ job_processor::process_string(const std::string& input,
if (filename) if (filename)
error_at_line(0, 0, filename, linenum, "parse error:"); error_at_line(0, 0, filename, linenum, "parse error:");
pf.format_errors(std::cerr); pf.format_errors(std::cerr);
return 1; return 2;
} }
return process_formula(pf.f, filename, linenum); return process_formula(pf.f, filename, linenum);
} }

138
bin/ltlsynt.cc
View file

@ -133,7 +133,7 @@ static bool opt_real = false;
static bool opt_do_verify = false; static bool opt_do_verify = false;
static const char* opt_print_aiger = nullptr; static const char* opt_print_aiger = nullptr;
static spot::game_info gi; static spot::game_info* gi;
static char const *const solver_names[] = static char const *const solver_names[] =
{ {
@ -175,8 +175,8 @@ namespace
static void static void
print_csv(const spot::formula& f) print_csv(const spot::formula& f)
{ {
auto& vs = gi.verbose_stream; auto& vs = gi->verbose_stream;
auto& bv = gi.bv; auto& bv = gi->bv;
if (not bv) if (not bv)
throw std::runtime_error("No information available for csv!"); throw std::runtime_error("No information available for csv!");
if (vs) if (vs)
@ -209,7 +209,7 @@ namespace
std::ostringstream os; std::ostringstream os;
os << f; os << f;
spot::escape_rfc4180(out << '"', os.str()); spot::escape_rfc4180(out << '"', os.str());
out << "\",\"" << solver_names[(int) gi.s] out << "\",\"" << solver_names[(int) gi->s]
<< "\"," << bv->total_time << "\"," << bv->total_time
<< ',' << bv->trans_time << ',' << bv->trans_time
<< ',' << bv->split_time << ',' << bv->split_time
@ -243,17 +243,17 @@ namespace
const std::vector<std::string>& output_aps) const std::vector<std::string>& output_aps)
{ {
spot::stopwatch sw; spot::stopwatch sw;
if (gi.bv) if (gi->bv)
sw.start(); sw.start();
auto safe_tot_time = [&]() auto safe_tot_time = [&]()
{ {
if (gi.bv) if (gi->bv)
gi.bv->total_time = sw.stop(); gi->bv->total_time = sw.stop();
}; };
bool opt_decompose_ltl = bool opt_decompose_ltl =
gi.opt.get("specification-decomposition", 0); gi->opt.get("specification-decomposition", 0);
std::vector<spot::formula> sub_form; std::vector<spot::formula> sub_form;
std::vector<std::set<spot::formula>> sub_outs; std::vector<std::set<spot::formula>> sub_outs;
if (opt_decompose_ltl) if (opt_decompose_ltl)
@ -319,7 +319,7 @@ namespace
spot::strategy_like_t strat{0, nullptr, bddfalse}; spot::strategy_like_t strat{0, nullptr, bddfalse};
if (!want_game) if (!want_game)
strat = strat =
spot::try_create_direct_strategy(*sub_f, *sub_o, gi); spot::try_create_direct_strategy(*sub_f, *sub_o, *gi);
switch (strat.success) switch (strat.success)
{ {
@ -331,20 +331,20 @@ namespace
} }
case 0: case 0:
{ {
auto arena = spot::create_game(*sub_f, *sub_o, gi); auto arena = spot::create_game(*sub_f, *sub_o, *gi);
if (gi.bv) if (gi->bv)
{ {
gi.bv->nb_states_arena += arena->num_states(); gi->bv->nb_states_arena += arena->num_states();
auto spptr = auto spptr =
arena->get_named_prop<std::vector<bool>>("state-player"); arena->get_named_prop<std::vector<bool>>("state-player");
assert(spptr); assert(spptr);
gi.bv->nb_states_arena_env += gi->bv->nb_states_arena_env +=
std::count(spptr->cbegin(), spptr->cend(), false); std::count(spptr->cbegin(), spptr->cend(), false);
assert((spptr->at(arena->get_init_state_number()) == false) assert((spptr->at(arena->get_init_state_number()) == false)
&& "Env needs first turn"); && "Env needs first turn");
} }
print_game(arena); print_game(arena);
if (!spot::solve_game(arena, gi)) if (!spot::solve_game(arena, *gi))
{ {
std::cout << "UNREALIZABLE" << std::endl; std::cout << "UNREALIZABLE" << std::endl;
safe_tot_time(); safe_tot_time();
@ -356,7 +356,7 @@ namespace
{ {
spot::strategy_like_t sl; spot::strategy_like_t sl;
sl.success = 1; sl.success = 1;
sl.strat_like = spot::create_strategy(arena, gi); sl.strat_like = spot::create_strategy(arena, *gi);
sl.glob_cond = bddfalse; sl.glob_cond = bddfalse;
strategies.push_back(sl); strategies.push_back(sl);
} }
@ -372,18 +372,18 @@ namespace
{ {
spot::stopwatch sw_min; spot::stopwatch sw_min;
sw_min.start(); sw_min.start();
bool do_split = 3 <= gi.opt.get("minimization-level", 1); bool do_split = 3 <= gi->opt.get("minimization-level", 1);
if (do_split) if (do_split)
split_2step_fast_here(strat.strat_like, split_2step_fast_here(strat.strat_like,
spot::get_synthesis_outputs(strat.strat_like)); spot::get_synthesis_outputs(strat.strat_like));
minimize_strategy_here(strat.strat_like, gi.minimize_lvl); minimize_strategy_here(strat.strat_like, gi->minimize_lvl);
if (do_split) if (do_split)
strat.strat_like = spot::unsplit_2step(strat.strat_like); strat.strat_like = spot::unsplit_2step(strat.strat_like);
auto delta = sw_min.stop(); auto delta = sw_min.stop();
if (gi.bv) if (gi->bv)
gi.bv->strat2aut_time += delta; gi->bv->strat2aut_time += delta;
if (gi.verbose_stream) if (gi->verbose_stream)
*gi.verbose_stream << "final strategy has " *gi->verbose_stream << "final strategy has "
<< strat.strat_like->num_states() << strat.strat_like->num_states()
<< " states and " << " states and "
<< strat.strat_like->num_edges() << strat.strat_like->num_edges()
@ -429,21 +429,21 @@ namespace
if (opt_print_aiger) if (opt_print_aiger)
{ {
spot::stopwatch sw2; spot::stopwatch sw2;
if (gi.bv) if (gi->bv)
sw2.start(); sw2.start();
saig = spot::strategies_to_aig(strategies, opt_print_aiger, saig = spot::strategies_to_aig(strategies, opt_print_aiger,
input_aps, input_aps,
sub_outs_str); sub_outs_str);
if (gi.bv) if (gi->bv)
{ {
gi.bv->aig_time = sw2.stop(); gi->bv->aig_time = sw2.stop();
gi.bv->nb_latches = saig->num_latches(); gi->bv->nb_latches = saig->num_latches();
gi.bv->nb_gates = saig->num_gates(); gi->bv->nb_gates = saig->num_gates();
} }
if (gi.verbose_stream) if (gi->verbose_stream)
{ {
*gi.verbose_stream << "AIG circuit was created in " *gi->verbose_stream << "AIG circuit was created in "
<< gi.bv->aig_time << gi->bv->aig_time
<< " and has " << saig->num_latches() << " and has " << saig->num_latches()
<< " latches and " << " latches and "
<< saig->num_gates() << " gates\n"; << saig->num_gates() << " gates\n";
@ -470,7 +470,7 @@ namespace
// TODO: different options to speed up verification?! // TODO: different options to speed up verification?!
spot::translator trans(gi.dict, &gi.opt); spot::translator trans(gi->dict, &gi->opt);
auto neg_spec = trans.run(spot::formula::Not(f)); auto neg_spec = trans.run(spot::formula::Not(f));
if (saig) if (saig)
{ {
@ -519,20 +519,20 @@ namespace
}; };
} }
static int static int
parse_opt(int key, char *arg, struct argp_state *) parse_opt(int key, char *arg, struct argp_state *)
{ {
// Called from C code, so should not raise any exception. // Called from C code, so should not raise any exception.
BEGIN_EXCEPTION_PROTECT; BEGIN_EXCEPTION_PROTECT;
switch (key) switch (key)
{ {
case OPT_ALGO: case OPT_ALGO:
gi.s = XARGMATCH("--algo", arg, solver_args, solver_types); gi->s = XARGMATCH("--algo", arg, solver_args, solver_types);
break; break;
case OPT_CSV: case OPT_CSV:
opt_csv = arg ? arg : "-"; opt_csv = arg ? arg : "-";
if (not gi.bv) if (not gi->bv)
gi.bv = spot::game_info::bench_var(); gi->bv = spot::game_info::bench_var();
break; break;
case OPT_INPUT: case OPT_INPUT:
{ {
@ -558,7 +558,7 @@ namespace
} }
case OPT_PRINT: case OPT_PRINT:
opt_print_pg = true; opt_print_pg = true;
gi.force_sbacc = true; gi->force_sbacc = true;
break; break;
case OPT_PRINT_HOA: case OPT_PRINT_HOA:
opt_print_hoa = true; opt_print_hoa = true;
@ -571,20 +571,20 @@ namespace
opt_real = true; opt_real = true;
break; break;
case OPT_VERBOSE: case OPT_VERBOSE:
gi.verbose_stream = &std::cerr; gi->verbose_stream = &std::cerr;
if (not gi.bv) if (not gi->bv)
gi.bv = spot::game_info::bench_var(); gi->bv = spot::game_info::bench_var();
break; break;
case OPT_VERIFY: case OPT_VERIFY:
opt_do_verify = true; opt_do_verify = true;
break; break;
case 'x': case 'x':
{ {
const char* opt = gi.opt.parse_options(arg); const char* opt = gi->opt.parse_options(arg);
if (opt) if (opt)
error(2, 0, "failed to parse --options near '%s'", opt); error(2, 0, "failed to parse --options near '%s'", opt);
// Dispatch the options to the gi structure // Dispatch the options to the gi structure
gi.minimize_lvl = gi.opt.get("minimization-level", 1); gi->minimize_lvl = gi->opt.get("minimization-level", 1);
} }
break; break;
} }
@ -596,31 +596,37 @@ int
main(int argc, char **argv) main(int argc, char **argv)
{ {
return protected_main(argv, [&] { return protected_main(argv, [&] {
//gi.opt.set("simul", 0); // no simulation, except... // Create gi_ as a local variable, so make sure it is destroyed
//gi.opt.set("dpa-simul", 1); // ... after determinization // before all global variables.
gi.opt.set("tls-impl", 1); // no automata-based implication check spot::game_info gi_;
gi.opt.set("wdba-minimize", 2); // minimize only syntactic oblig gi = &gi_;
const argp ap = { options, parse_opt, nullptr, //gi_.opt.set("simul", 0); // no simulation, except...
argp_program_doc, children, nullptr, nullptr }; //gi_.opt.set("dpa-simul", 1); // ... after determinization
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) gi_.opt.set("tls-impl", 1); // no automata-based implication check
exit(err); gi_.opt.set("wdba-minimize", 2); // minimize only syntactic oblig
check_no_formula(); const argp ap = { options, parse_opt, nullptr,
argp_program_doc, children, nullptr, nullptr };
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
exit(err);
check_no_formula();
// Check if inputs and outputs are distinct // Check if inputs and outputs are distinct
// Inputs can be empty, outputs not // Inputs can be empty, outputs not
if (not all_input_aps.empty()) if (not all_input_aps.empty())
{ {
for (const auto& ai : all_input_aps) for (const auto& ai : all_input_aps)
if (std::count(all_output_aps.begin(), all_output_aps.end(), ai)) if (std::count(all_output_aps.begin(), all_output_aps.end(), ai))
throw std::runtime_error("ltlsynt(): " + ai + throw std::runtime_error("ltlsynt(): " + ai +
" appears in the input AND output APs."); " appears in the input AND output APs.");
} }
ltl_processor processor(all_input_aps, all_output_aps); ltl_processor processor(all_input_aps, all_output_aps);
if (int res = processor.run(); res == 0 || res == 1)
auto res = processor.run(); {
// Diagnose unused -x options // Diagnose unused -x options
gi.opt.report_unused_options(); gi_.opt.report_unused_options();
return res; return res;
}); }
return 2;
});
} }

7
tests/core/ltlsynt.test
View file

@ -509,4 +509,9 @@ o1 o1
EOF EOF
ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\ ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\
--aiger=isop --algo=lar -x"specification-decomposition=1" >out --aiger=isop --algo=lar -x"specification-decomposition=1" >out
diff out exp diff out exp
# Issue #477
ltlsynt -f 'a U (b' 2>err && exit 1
test $? -eq 2
test `wc -l <err` -eq 4