From be28365db4a9c1290074f6f5a8a1005c70c9fc55 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 22 Jun 2022 19:31:24 +0200 Subject: [PATCH] ltlsynt: add --from-pgame option to read parity games * bin/common_file.cc, bin/common_file.hh (output_file): Add a force_append option. * bin/ltlsynt.cc: Implement the --from-pgame option, and fix suppot for --csv when multiple inputs are processed. * NEWS: Mention the new option. * tests/core/syfco.test: Add a test case. * tests/core/ltlsynt-pgame.test: New file. * tests/Makefile.am: Add it. --- NEWS | 5 +- bin/common_file.cc | 11 ++- bin/common_file.hh | 4 +- bin/ltlsynt.cc | 170 ++++++++++++++++++++++++++++++++-- tests/Makefile.am | 1 + tests/core/ltlsynt-pgame.test | 157 +++++++++++++++++++++++++++++++ tests/core/syfco.test | 4 + 7 files changed, 336 insertions(+), 16 deletions(-) create mode 100755 tests/core/ltlsynt-pgame.test diff --git a/NEWS b/NEWS index b8067d47a..307cc4a3a 100644 --- a/NEWS +++ b/NEWS @@ -29,10 +29,13 @@ New in spot 2.10.6.dev (not yet released) - autcross learned a --language-complemented option to assist in the case one is testing tools that complement automata. (issue #504). - - ltlsynt as a new option --tlsf that takes the filename of a TLSF + - ltlsynt has a new option --tlsf that takes the filename of a TLSF specification and calls syfco (which must be installed) to convert it into an LTL formula. + - ltlsynt has a new option --from-pgame that takes a parity game in + extended HOA format, as used in the Synthesis Competition. + Library: - A global variable, together with its setters and getters to define the diff --git a/bin/common_file.cc b/bin/common_file.cc index ab89fbfe4..005bb5479 100644 --- a/bin/common_file.cc +++ b/bin/common_file.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2015, 2016, 2022 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -22,15 +22,18 @@ #include -output_file::output_file(const char* name) +output_file::output_file(const char* name, bool force_append) { std::ios_base::openmode mode = std::ios_base::trunc; if (name[0] == '>' && name[1] == '>') { - mode = std::ios_base::app; append_ = true; name += 2; } + if (force_append) + append_ = true; + if (append_) + mode = std::ios_base::app; if (name[0] == '-' && name[1] == 0) { os_ = &std::cout; diff --git a/bin/common_file.hh b/bin/common_file.hh index fba62dec0..b8f9842b8 100644 --- a/bin/common_file.hh +++ b/bin/common_file.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de +// Copyright (C) 2015, 2016, 2022 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -33,7 +33,7 @@ public: // Open a file for output. "-" is interpreted as stdout. // Names that start with ">>" are opened for append. // The function calls error() on... error. - output_file(const char* name); + output_file(const char* name, bool force_append = false); void close(const std::string& name); diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index b5d4289f5..e7d6b73d1 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -23,6 +23,7 @@ #include "common_aoutput.hh" #include "common_finput.hh" +#include "common_hoaread.hh" #include "common_setup.hh" #include "common_sys.hh" #include "common_trans.hh" @@ -48,6 +49,7 @@ enum OPT_BYPASS, OPT_CSV, OPT_DECOMPOSE, + OPT_FROM_PGAME, OPT_INPUT, OPT_OUTPUT, OPT_PRINT, @@ -73,6 +75,9 @@ static const argp_option options[] = { "tlsf", OPT_TLSF, "FILENAME", 0, "Read a TLSF specification from FILENAME, and call syfco to " "convert it into LTL", 0 }, + { "from-pgame", OPT_FROM_PGAME, "FILENAME", 0, + "Read a parity game in Extended HOA format instead of building it.", + 0 }, /**************************************************/ { nullptr, 0, nullptr, 0, "Fine tuning:", 10 }, { "algo", OPT_ALGO, "sd|ds|ps|lar|lar.old|acd", 0, @@ -250,7 +255,7 @@ namespace }; static void - print_csv(const spot::formula& f) + print_csv(const spot::formula& f, const char* filename = nullptr) { auto& vs = gi->verbose_stream; auto& bv = gi->bv; @@ -259,7 +264,9 @@ namespace if (vs) *vs << "writing CSV to " << opt_csv << '\n'; - output_file outf(opt_csv); + static bool not_first_time = false; + output_file outf(opt_csv, not_first_time); + not_first_time = true; // force append on next print. std::ostream& out = outf.ostream(); // Do not output the header line if we append to a file. @@ -284,10 +291,15 @@ namespace out << '\n'; } std::ostringstream os; - os << f; - spot::escape_rfc4180(out << '"', os.str()); - out << "\",\"" << algo_names[(int) gi->s] - << "\"," << bv->total_time + if (filename) + os << filename; + else + os << f; + spot::escape_rfc4180(out << '"', os.str()) << "\","; + // if a filename was given, assume the game has been read directly + if (!filename) + out << '"' << algo_names[(int) gi->s] << '"'; + out << ',' << bv->total_time << ',' << bv->trans_time << ',' << bv->split_time << ',' << bv->paritize_time; @@ -319,6 +331,8 @@ namespace const std::vector& input_aps, const std::vector& output_aps) { + if (opt_csv) // reset benchmark data + gi->bv = spot::synthesis_info::bench_var(); spot::stopwatch sw; if (gi->bv) sw.start(); @@ -386,7 +400,7 @@ namespace [](const spot::twa_graph_ptr& game)->void { if (opt_print_pg) - pg_print(std::cout, game); + spot::pg_print(std::cout, game); else spot::print_hoa(std::cout, game, opt_print_hoa_args) << '\n'; } @@ -438,6 +452,8 @@ namespace safe_tot_time(); return 1; } + if (gi->bv) + gi->bv->realizable = true; // Create the (partial) strategy // only if we need it if (!opt_real) @@ -701,6 +717,141 @@ namespace return res; } + int process_pgame(spot::twa_graph_ptr arena, + const std::string& location) + { + if (opt_csv) // reset benchmark data + gi->bv = spot::synthesis_info::bench_var(); + spot::stopwatch sw_global; + spot::stopwatch sw_local; + if (gi->bv) + { + sw_global.start(); + sw_local.start(); + } + if (!arena->get_named_prop("synthesis-outputs")) + { + std::cerr << location << ": controllable-AP is not specified\n"; + return 2; + } + if (!arena->get_named_prop>("state-player")) + arena = spot::split_2step(arena, true); + // FIXME: If we do not split the game, we should check that it is + // alternating. + spot::change_parity_here(arena, + spot::parity_kind_max, + spot::parity_style_odd); + spot::colorize_parity_here(arena, true); + if (gi->bv) + { + gi->bv->split_time += sw_local.stop(); + gi->bv->nb_states_arena += arena->num_states(); + auto spptr = + arena->get_named_prop>("state-player"); + assert(spptr); + gi->bv->nb_states_arena_env += + std::count(spptr->cbegin(), spptr->cend(), false); + } + if (opt_print_pg || opt_print_hoa) + { + if (opt_print_pg) + spot::pg_print(std::cout, arena); + else + spot::print_hoa(std::cout, arena, opt_print_hoa_args) << '\n'; + return 0; + } + auto safe_tot_time = [&]() { + if (gi->bv) + gi->bv->total_time = sw_global.stop(); + }; + if (!spot::solve_game(arena, *gi)) + { + std::cout << "UNREALIZABLE" << std::endl; + safe_tot_time(); + return 1; + } + if (gi->bv) + gi->bv->realizable = true; + std::cout << "REALIZABLE" << std::endl; + if (opt_real) + { + safe_tot_time(); + return 0; + } + sw_local.start(); + spot::twa_graph_ptr mealy_like = + spot::solved_game_to_mealy(arena, *gi); + // Keep the machine split for aiger otherwise, separate it. + spot::simplify_mealy_here(mealy_like, *gi, opt_print_aiger); + + automaton_printer printer; + spot::process_timer timer_printer_dummy; + if (opt_print_aiger) + { + if (gi->bv) + sw_local.start(); + spot::aig_ptr saig = + spot::mealy_machine_to_aig(mealy_like, opt_print_aiger); + if (gi->bv) + { + gi->bv->aig_time = sw_local.stop(); + gi->bv->nb_latches = saig->num_latches(); + gi->bv->nb_gates = saig->num_gates(); + } + if (gi->verbose_stream) + { + *gi->verbose_stream << "AIG circuit was created in " + << gi->bv->aig_time + << " seconds and has " << saig->num_latches() + << " latches and " + << saig->num_gates() << " gates\n"; + } + spot::print_aiger(std::cout, saig) << '\n'; + } + else + { + printer.print(mealy_like, timer_printer_dummy); + } + safe_tot_time(); + return 0; + } + + int + process_aut_file(const char* filename) override + { + spot::automaton_stream_parser hp(filename); + int err = 0; + while (!abort_run) + { + spot::parsed_aut_ptr haut = hp.parse(spot::make_bdd_dict()); + if (!haut->aut && haut->errors.empty()) + break; + if (haut->format_errors(std::cerr)) + err = 2; + if (!haut->aut /*|| (err && abort_on_error_)*/) + { + error(2, 0, "failed to read automaton from %s", + haut->filename.c_str()); + } + else if (haut->aborted) + { + std::cerr << haut->filename << ':' << haut->loc + << ": aborted input automaton\n"; + err = std::max(err, 2); + } + else + { + std::ostringstream os; + os << haut->filename << ':' << haut->loc; + std::string loc = os.str(); + int res = process_pgame(haut->aut, loc); + if (res < 2 && opt_csv) + print_csv(nullptr, loc.c_str()); + err = std::max(err, res); + } + } + return err; + } }; } @@ -719,13 +870,14 @@ parse_opt(int key, char *arg, struct argp_state *) break; case OPT_CSV: opt_csv = arg ? arg : "-"; - if (not gi->bv) - gi->bv = spot::synthesis_info::bench_var(); break; case OPT_DECOMPOSE: opt_decompose_ltl = XARGMATCH("--decompose", arg, decompose_args, decompose_values); break; + case OPT_FROM_PGAME: + jobs.emplace_back(arg, job_type::AUT_FILENAME); + break; case OPT_INPUT: { all_input_aps.emplace(std::vector{}); diff --git a/tests/Makefile.am b/tests/Makefile.am index b4627f3e6..1a3d440c3 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -342,6 +342,7 @@ TESTS_twa = \ core/parity.test \ core/parity2.test \ core/ltlsynt.test \ + core/ltlsynt-pgame.test \ core/syfco.test \ core/rabin2parity.test \ core/twacube.test diff --git a/tests/core/ltlsynt-pgame.test b/tests/core/ltlsynt-pgame.test new file mode 100755 index 000000000..b4bada798 --- /dev/null +++ b/tests/core/ltlsynt-pgame.test @@ -0,0 +1,157 @@ +#! /bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2022 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +. ./defs || exit 1 + +set -e + +# From SYNTCOMP +cat >aut7.hoa < Xa)" +Start: 0 +acc-name: Buchi +Acceptance: 1 Inf(0) +AP: 2 "a" "b" +controllable-AP: 1 +properties: explicit-labels trans-labels +--BODY-- +State: 0 + [t] 1 + [1] 2 + [!1] 3 +State: 1 "GFa" + [0] 1 {0} + [!0] 1 +State: 2 "a & G(b <-> Xa)" {0} + [0&1] 2 + [0&!1] 3 +State: 3 "!a & G(b <-> Xa)" {0} + [!0&1] 2 + [!0&!1] 3 +--END-- +EOF + +test UNREALIZABLE = `ltlsynt --realizability --from-pgame aut7.hoa` + +grep -v controllable-AP aut7.hoa > aut7b.hoa +run 2 ltlsynt --realizability --from-pgame aut7b.hoa 2>stderr +grep 'aut7b.*controllable-AP' stderr + + +# From SYNTCOMP +cat >UnderapproxDemo2.ehoa <starve.ehoa <expect <results +diff expect results + +ltlsynt --realizability --from-pgame starve.ehoa \ + --from-pgame UnderapproxDemo2.ehoa \ + --from-pgame aut7.hoa --csv=out.csv >result || : +cat >expect <result || : +test 4 = `wc -l < out.csv` +cut -d, -f 9,10,11,12,13 right +end='"strat_num_states","strat_num_edges"' +cat >expect < out1 ltlsynt --tlsf test.tlsf --tlsf test.tlsf > out2 cat out1 out1 > out11 diff out11 out2 + +ltlsynt --tlsf test.tlsf --tlsf test.tlsf --print-game > pgame.hoa +ltlsynt --from-pgame pgame.hoa > out3 +diff out2 out3