From ea9384dd4b04019c575f6bf92dbf6030da4cd4aa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 8 Sep 2020 16:25:36 +0200 Subject: [PATCH] extend HOA I/O to preserve the state-player property * spot/parseaut/parseaut.yy, spot/parseaut/scanaut.ll, spot/twaalgos/hoa.cc: Add input and output support. * doc/org/hoa.org: Document the HOA extension. * bin/ltlsynt.cc: Add a --print-game-hoa option to produce such format. * tests/core/gamehoa.test: New file to test this. * tests/Makefile.am: Add it. * NEWS: Mention this new feature. --- NEWS | 9 ++++++ bin/ltlsynt.cc | 20 ++++++++++-- doc/org/hoa.org | 66 +++++++++++++++++++++++++++++++++++++++ spot/parseaut/parseaut.yy | 34 +++++++++++++++++++- spot/parseaut/scanaut.ll | 3 +- spot/twaalgos/hoa.cc | 20 +++++++++++- tests/Makefile.am | 1 + tests/core/gamehoa.test | 61 ++++++++++++++++++++++++++++++++++++ 8 files changed, 209 insertions(+), 5 deletions(-) create mode 100755 tests/core/gamehoa.test diff --git a/NEWS b/NEWS index c9ab0bd98..ca378ed45 100644 --- a/NEWS +++ b/NEWS @@ -8,6 +8,11 @@ New in spot 2.9.4.dev (not yet released) problem. There is also an --enable-c++20 option to configure in case you want to force a build of Spot in C++20 mode. + Command-line tools: + + - ltlsynt learned --print-game-hoa to output its internal parity + game in the HOA format (with an extension described below). + Library: - Historically, Spot labels automata by Boolean formulas over @@ -67,6 +72,10 @@ New in spot 2.9.4.dev (not yet released) has a parity max odd acceptance and a "state-player" property is considered to be a parity game. + - the "state-player" property is output by the HOA printer, and read + back by the automaton parser, which means that games can be saved + and loaded. + New in spot 2.9.4 (2020-09-07) Bugs fixed: diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 92485c5ff..78571fe50 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -49,6 +49,7 @@ #include #include #include +#include enum { @@ -58,6 +59,7 @@ enum OPT_OUTPUT, OPT_PRINT, OPT_PRINT_AIGER, + OPT_PRINT_HOA, OPT_REAL, OPT_VERBOSE }; @@ -87,6 +89,8 @@ static const argp_option options[] = { nullptr, 0, nullptr, 0, "Output options:", 20 }, { "print-pg", OPT_PRINT, nullptr, 0, "print the parity game in the pgsolver format, do not solve it", 0}, + { "print-game-hoa", OPT_PRINT_HOA, "options", OPTION_ARG_OPTIONAL, + "print the parity game in the HOA format, do not solve it", 0}, { "realizability", OPT_REAL, nullptr, 0, "realizability only, do not compute a winning strategy", 0}, { "aiger", OPT_PRINT_AIGER, nullptr, 0, @@ -125,6 +129,8 @@ static std::vector output_aps; static const char* opt_csv = nullptr; static bool opt_print_pg = false; +static bool opt_print_hoa = false; +static const char* opt_print_hoa_args = nullptr; static bool opt_real = false; static bool opt_print_aiger = false; static spot::option_map extra_options; @@ -315,7 +321,7 @@ namespace { out << ("\"formula\",\"algo\",\"trans_time\"," "\"split_time\",\"todpa_time\",\"build_game_time\""); - if (!opt_print_pg) + if (!opt_print_pg && !opt_print_hoa) { out << ",\"solve_time\""; if (!opt_real) @@ -333,7 +339,7 @@ namespace << ',' << split_time << ',' << paritize_time << ',' << bgame_time; - if (!opt_print_pg) + if (!opt_print_pg && !opt_print_hoa) { out << ',' << solve_time; if (!opt_real) @@ -555,6 +561,12 @@ namespace pg_print(std::cout, dpa); return 0; } + if (opt_print_hoa) + { + timer.stop(); + spot::print_hoa(std::cout, dpa, opt_print_hoa_args) << '\n'; + return 0; + } spot::strategy_t strategy[2]; spot::region_t winning_region[2]; @@ -646,6 +658,10 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_PRINT: opt_print_pg = true; break; + case OPT_PRINT_HOA: + opt_print_hoa = true; + opt_print_hoa_args = arg; + break; case OPT_PRINT_AIGER: opt_print_aiger = true; break; diff --git a/doc/org/hoa.org b/doc/org/hoa.org index a404eae34..d3ae178b3 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -1154,3 +1154,69 @@ rm -f stvstracc.hoa sba.hoa stvstrlab.hoa decorate.hoa # LocalWords: bitsets randaut stvstrlab aut Hv hw bigwedge mathsf # LocalWords: genltl gf GFp Fp parser's rankdir br labelloc ffffa # LocalWords: fillcolor fontname svg txt Xa +** Arenas for two-player games + +An automaton can be seen as a two-player game by simply annotating +states with number representing the player that should play in this +state. We use an extension to the HOA format to transmit this +information: the =spot-state-player:= head (or =spot.state-player:= when +using the HOA 1.1 version) is followed by a string of =0= or +=1=, one per state of the automaton, representing the player's number +associated to each state. + +For instance in the following output of =ltlsynt=, the sequence +call_player() indicates the players owning each of the +call_player(h="States")[:results raw] states. + +#+NAME: exgame +#+begin_src sh :wrap SRC hoa +ltlsynt --ins=a --outs=b -f 'Ga <-> Gb' --print-game-hoa +#+end_src + +#+RESULTS: exgame +#+begin_SRC hoa +HOA: v1 +States: 11 +Start: 3 +AP: 2 "a" "b" +acc-name: Streett 1 +Acceptance: 2 Fin(0) | Inf(1) +properties: trans-labels explicit-labels trans-acc colored complete +properties: deterministic +spot-state-player: 0 0 0 0 1 1 1 1 1 1 0 +--BODY-- +State: 0 +[t] 4 {0} +State: 1 +[t] 5 {0} +State: 2 +[0] 6 {0} +[!0] 7 {0} +State: 3 +[0] 8 {0} +[!0] 5 {0} +State: 4 +[t] 0 {1} +State: 5 +[!1] 0 {0} +[1] 1 {0} +State: 6 +[t] 2 {0} +State: 7 +[t] 0 {0} +State: 8 +[!1] 2 {0} +[1] 3 {1} +State: 9 +[t] 10 {0} +State: 10 +[t] 9 {0} +--END-- +#+end_SRC + +#+NAME: player +#+BEGIN_SRC sh :exports none :var t=exgame h="spot-state-player" +sed -n "s/^$h: \(.*\)\$/\\1/p" <* highlight_edges = nullptr; std::map* highlight_states = nullptr; std::map states_map; + std::vector* state_player = nullptr; + spot::location state_player_loc; std::set ap_set; unsigned cur_state; int states = -1; @@ -238,6 +240,7 @@ extern "C" int strverscmp(const char *s1, const char *s2); %token STATE "State:"; %token SPOT_HIGHLIGHT_EDGES "spot.highlight.edges:"; %token SPOT_HIGHLIGHT_STATES "spot.highlight.states:"; +%token SPOT_STATE_PLAYER "spot.state-player:"; %token IDENTIFIER "identifier"; // also used by neverclaim %token HEADERNAME "header name"; %token ANAME "alias name"; @@ -822,6 +825,15 @@ header-item: "States:" INT | "spot.highlight.states:" { res.highlight_states = new std::map; } highlight-states + | "spot.state-player:" + { auto p = new std::vector; + if (res.states >= 0) + p->reserve(res.states); + res.state_player = p; + } state-player + { + res.state_player_loc = @$; + } | HEADERNAME header-spec { char c = (*$1)[0]; @@ -918,6 +930,14 @@ highlight-states: %empty res.highlight_states->emplace($2, $3); } +state-player: %empty + | state-player INT + { + if ($2 != 0 && $2 != 1) + error(@2, "player should be 0 or 1"); + res.state_player->emplace_back($2); + } + header-spec: %empty | header-spec BOOLEAN | header-spec INT @@ -1196,6 +1216,16 @@ body: states "environment variable."); det_warned = true; } + if (res.state_player) + if (unsigned spsz = res.state_player->size(); spsz != n) + { + error(res.state_player_loc, + "ignoring state-player header because it has "s + + std::to_string(spsz) + " entries while automaton has " + + std::to_string(n) + " states"); + delete res.state_player; + res.state_player = nullptr; + } } state-num: INT { @@ -2621,6 +2651,8 @@ namespace spot r.aut_or_ks->set_named_prop("highlight-edges", r.highlight_edges); if (r.highlight_states) r.aut_or_ks->set_named_prop("highlight-states", r.highlight_states); + if (r.state_player) + r.aut_or_ks->set_named_prop("state-player", r.state_player); fix_acceptance(r); fix_initial_state(r); fix_properties(r); diff --git a/spot/parseaut/scanaut.ll b/spot/parseaut/scanaut.ll index 728404c3d..cb54a0af7 100644 --- a/spot/parseaut/scanaut.ll +++ b/spot/parseaut/scanaut.ll @@ -1,5 +1,5 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2014-2018 Laboratoire de Recherche et Développement +** Copyright (C) 2014-2018, 2020 Laboratoire de Recherche et Développement ** de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. @@ -129,6 +129,7 @@ identifier [[:alpha:]_][[:alnum:]_.-]* "properties:" return token::PROPERTIES; "spot.highlight.states:" return token::SPOT_HIGHLIGHT_STATES; "spot.highlight.edges:" return token::SPOT_HIGHLIGHT_EDGES; + "spot"[.-]"state-player:" return token::SPOT_STATE_PLAYER; "--BODY--" return token::BODY; "--END--" BEGIN(INITIAL); return token::END; "State:" return token::STATE; diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index 320053eb5..fe72896ea 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2019 Laboratoire de Recherche et +// Copyright (C) 2014-2020 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -609,6 +609,24 @@ namespace spot os << (v1_1 ? "spot." : "spot-") << "rejected-word: \""; escape_str(os, *word) << '"' << nl; } + if (auto player = aut->get_named_prop>("state-player")) + { + os << (v1_1 ? "spot." : "spot-") << "state-player:"; + if (player->size() != num_states) + throw std::runtime_error("print_hoa(): state-player property has" + " (" + std::to_string(player->size()) + + " states but automaton has " + + std::to_string(num_states)); + unsigned n = 0; + while (n < num_states) + { + os << ' ' << (*player)[n]; + ++n; + if (newline && n < num_states && (n % 30 == 0)) + os << "\n "; + } + os << nl; + } // If we want to output implicit labels, we have to // fill a vector with all destinations in order. diff --git a/tests/Makefile.am b/tests/Makefile.am index e8db7e94b..cd291c7cf 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -222,6 +222,7 @@ TESTS_twa = \ core/bdddict.test \ core/cube.test \ core/alternating.test \ + core/gamehoa.test \ core/ltlcross3.test \ core/ltlcross5.test \ core/taatgba.test \ diff --git a/tests/core/gamehoa.test b/tests/core/gamehoa.test new file mode 100755 index 000000000..e5a6168e5 --- /dev/null +++ b/tests/core/gamehoa.test @@ -0,0 +1,61 @@ +#! /bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2020 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 -x + +ltlsynt --ins=a,c --outs=b -f 'GF(a <-> XXXc) <-> GFb' --print-game-hoa >out +grep spot-state-player: out +autfilt out >out2 +diff out out2 +ltlsynt --ins=a,c --outs=b -f 'GF(a <-> XXXc) <-> GFb' --print-game-hoa=l >out3 +test 1 = `wc -l < out3` +cmp out out3 && exit 1 +autfilt out3 >out2 +diff out out2 + +cat <bug.hoa +HOA: v1 States: 11 Start: 3 AP: 3 "a" "b" "c" +acc-name: Streett 1 Acceptance: 2 Fin(0) | Inf(1) spot-state-player: 0 +0 0 0 1 1 1 1 1 1 --BODY-- State: 0 [t] 4 {0} State: 1 [t] 5 {0} +State: 2 [0] 6 {0} [!0] 7 {0} State: 3 [0] 8 {0} [!0] 5 {0} State: 4 +[t] 0 {1} State: 5 [!1] 0 {0} [1] 1 {0} State: 6 [t] 2 {0} State: 7 +[t] 0 {0} State: 8 [!1] 2 {0} [1] 3 {1} State: 9 [t] 10 {0} State: 10 +[t] 9 {0} --END-- +EOF +autfilt bug.hoa 2> error && exit 1 +cat error +grep 'bug.hoa:2.69-68:.* has 11 states.*state-player has 10 entries' error + +cat <bug2.hoa +HOA: v1 States: 11 Start: 3 AP: 3 "a" "b" "c" +acc-name: Streett 1 Acceptance: 2 Fin(0) | Inf(1) spot-state-player: 0 +0 0 0 1 3 1 1 a 1 0--BODY-- State: 0 [t] 4 {0} State: 1 [t] 5 {0} +State: 2 [0] 6 {0} [!0] 7 {0} State: 3 [0] 8 {0} [!0] 5 {0} State: 4 +[t] 0 {1} State: 5 [!1] 0 {0} [1] 1 {0} State: 6 [t] 2 {0} State: 7 +[t] 0 {0} State: 8 [!1] 2 {0} [1] 3 {1} State: 9 [t] 10 {0} State: 10 +[t] 9 {0} --END-- +EOF +autfilt bug2.hoa 2> error && exit 1 +cat error +grep 'bug2.hoa:3.9: player should be 0 or 1' error +grep 'bug2.hoa:3.15:.*unexpected' error +grep 'bug2.hoa:2.51-3.13: ignoring state-player.* 8 entries.* 11 states' error