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

extend HOA I/O to preserve the state-player property

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2020-09-08 16:25:36 +02:00
parent 25c75c55b1
commit ea9384dd4b
8 changed files with 209 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

9
NEWS
View file

@ -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:

20
bin/ltlsynt.cc
View file

@ -49,6 +49,7 @@
#include <spot/twaalgos/simulation.hh>
#include <spot/twaalgos/split.hh>
#include <spot/twaalgos/toparity.hh>
#include <spot/twaalgos/hoa.hh>
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<std::string> 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;

66
doc/org/hoa.org
View file

@ -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" <<EOF | tr -d '\n'
$t
EOF
#+END_SRC

34
spot/parseaut/parseaut.yy
View file

@ -1,5 +1,5 @@
/* -*- coding: utf-8 -*-
** Copyright (C) 2014-2019 Laboratoire de Recherche et Développement
** Copyright (C) 2014-2020 Laboratoire de Recherche et Développement
** de l'Epita (LRDE).
**
** This file is part of Spot, a model checking library.
@ -138,6 +138,8 @@ extern "C" int strverscmp(const char *s1, const char *s2);
std::map<unsigned, unsigned>* highlight_edges = nullptr;
std::map<unsigned, unsigned>* highlight_states = nullptr;
std::map<unsigned, unsigned> states_map;
std::vector<bool>* state_player = nullptr;
spot::location state_player_loc;
std::set<int> 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 <str> IDENTIFIER "identifier"; // also used by neverclaim
%token <str> HEADERNAME "header name";
%token <str> ANAME "alias name";
@ -822,6 +825,15 @@ header-item: "States:" INT
| "spot.highlight.states:"
{ res.highlight_states = new std::map<unsigned, unsigned>; }
highlight-states
| "spot.state-player:"
{ auto p = new std::vector<bool>;
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);

3
spot/parseaut/scanaut.ll
View file

@ -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;

20
spot/twaalgos/hoa.cc
View file

@ -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<std::vector<bool>>("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.

1
tests/Makefile.am
View file

@ -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 \

61
tests/core/gamehoa.test Executable file
View file

@ -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 <http://www.gnu.org/licenses/>.
. ./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 <<EOF >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 <<EOF >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