parseaut: Add support for PGSolver's format
* spot/parseaut/parseaut.yy, spot/parseaut/scanaut.ll: Add rules for PGSolver's format. * spot/parseaut/public.hh: PGAME is a new type of output. * tests/core/pgsolver.test: New file. * tests/Makefile.am: Add it. * tests/python/games.ipynb: More exemples. * NEWS: Mention the new feature.
This commit is contained in:
Alexandre Duret-Lutz
parent
d6b3c757d0
commit
444e2b5b89
7 changed files with 1144 additions and 342 deletions
6
NEWS
6
NEWS
|
|
@ -65,6 +65,10 @@ New in spot 2.10.6.dev (not yet released)
|
|||
property of Spot to the controllable-AP header for the Extended
|
||||
HOA format used in SyntComp. https://arxiv.org/abs/1912.05793
|
||||
|
||||
- The automaton parser learned to parse games in the PGSolver format.
|
||||
See the bottom of https://spot.lrde.epita.fr/ipynb/games.html for
|
||||
an example.
|
||||
|
||||
- "aliases" is a new named property that is filled by the HOA parser
|
||||
using the list of aliases declared in the HOA file, and then used
|
||||
by the HOA printer on a best-effort basis. Aliases can be used to
|
||||
|
|
@ -105,7 +109,7 @@ New in spot 2.10.6.dev (not yet released)
|
|||
|
||||
- The zielonka_tree construction was optimized using the same
|
||||
memoization trick that is used in ACD. Additionally it can now be
|
||||
run with additional option to abort when the tree as an unwanted
|
||||
run with additional options to abort when the tree as an unwanted
|
||||
shape, or to turn the tree into a DAG.
|
||||
|
||||
- contains() can now take a twa as a second argument, not just a
|
||||
|
|
|
|||
|
|
@ -44,6 +44,7 @@
|
|||
#include "spot/priv/accmap.hh"
|
||||
#include <spot/tl/parse.hh>
|
||||
#include <spot/twaalgos/alternation.hh>
|
||||
#include <spot/twaalgos/game.hh>
|
||||
|
||||
using namespace std::string_literals;
|
||||
|
||||
|
|
@ -256,6 +257,11 @@ extern "C" int strverscmp(const char *s1, const char *s2);
|
|||
%token ENDOFFILE 0 "end of file"
|
||||
%token <str> '['
|
||||
|
||||
%token <str> LINEDIRECTIVE "#line"
|
||||
%token <b> BDD
|
||||
|
||||
/**** DSTAR tokens ****/
|
||||
%token ENDDSTAR "end of DSTAR automaton"
|
||||
%token DRA "DRA"
|
||||
%token DSA "DSA"
|
||||
%token V2 "v2"
|
||||
|
|
@ -263,14 +269,12 @@ extern "C" int strverscmp(const char *s1, const char *s2);
|
|||
%token ACCPAIRS "Acceptance-Pairs:"
|
||||
%token ACCSIG "Acc-Sig:"
|
||||
%token ENDOFHEADER "---"
|
||||
%token <str> LINEDIRECTIVE "#line"
|
||||
%token <b> BDD
|
||||
|
||||
%left '|'
|
||||
%left '&'
|
||||
%precedence '!'
|
||||
|
||||
%type <states> init-state-conj-2 state-conj-2 state-conj-checked
|
||||
%type <states> init-state-conj-2 state-conj-2 state-conj-checked pgame_succs
|
||||
%type <num> checked-state-num state-num acc-set sign
|
||||
%type <b> label-expr
|
||||
%type <mark> acc-sig acc-sets trans-acc_opt state-acc_opt
|
||||
|
|
@ -299,10 +303,14 @@ extern "C" int strverscmp(const char *s1, const char *s2);
|
|||
%type <str> nc-one-ident nc-ident-list
|
||||
%type <code> acceptance-cond
|
||||
|
||||
/**** PGAME tokens ****/
|
||||
// Also using INT, STRING
|
||||
%token PGAME "start of PGSolver game"
|
||||
%token ENDPGAME "end of PGSolver game"
|
||||
|
||||
/**** LBTT tokens *****/
|
||||
// Also using INT, STRING
|
||||
// Also using INT, STRING
|
||||
%token ENDAUT "-1"
|
||||
%token ENDDSTAR "end of DSTAR automaton"
|
||||
%token <num> LBTT "LBTT header"
|
||||
%token <num> INT_S "state acceptance"
|
||||
%token <num> LBTT_EMPTY "acceptance sets for empty automaton"
|
||||
|
|
@ -364,6 +372,7 @@ aut-1: hoa { res.h->type = spot::parsed_aut_type::HOA; }
|
|||
| never { res.h->type = spot::parsed_aut_type::NeverClaim; }
|
||||
| lbtt { res.h->type = spot::parsed_aut_type::LBTT; }
|
||||
| dstar /* will set type as DSA or DRA while parsing first line */
|
||||
| pgame { res.h->type = spot::parsed_aut_type::PGAME; }
|
||||
|
||||
/**********************************************************************/
|
||||
/* Rules for HOA */
|
||||
|
|
@ -1765,7 +1774,7 @@ dstar_header: dstar_sizes
|
|||
|
||||
if (res.states > 0)
|
||||
{
|
||||
res.h->aut->new_states(res.states);;
|
||||
res.h->aut->new_states(res.states);
|
||||
res.info_states.resize(res.states);
|
||||
}
|
||||
res.acc_style = State_Acc;
|
||||
|
|
@ -1908,6 +1917,93 @@ dstar_states: %empty
|
|||
res.h->aut->new_edge(res.cur_state, i.first, i.second, $3);
|
||||
}
|
||||
|
||||
/**********************************************************************/
|
||||
/* Rules for PGSolver games */
|
||||
/**********************************************************************/
|
||||
|
||||
pgamestart: PGAME
|
||||
{
|
||||
if (res.opts.want_kripke)
|
||||
{
|
||||
error(@$,
|
||||
"cannot read a Kripke structure out of a PGSolver game.");
|
||||
YYABORT;
|
||||
}
|
||||
}
|
||||
|
||||
pgame: pgamestart pgame_nodes ENDPGAME
|
||||
{
|
||||
unsigned n = res.accset;
|
||||
auto p = spot::acc_cond::acc_code::parity_max_odd(n);
|
||||
res.h->aut->set_acceptance(n, p);
|
||||
res.acc_style = State_Acc;
|
||||
// Pretend that we have declared all states.
|
||||
n = res.h->aut->num_states();
|
||||
res.info_states.resize(n);
|
||||
for (auto& p: res.info_states)
|
||||
p.declared = true;
|
||||
}
|
||||
| pgamestart error ENDPGAME
|
||||
{
|
||||
error(@$, "failed to parse this as a PGSolver game");
|
||||
}
|
||||
|
||||
pgame_nodes: pgame_node ';'
|
||||
| pgame_nodes pgame_node ';'
|
||||
|
||||
pgame_succs: INT
|
||||
{ $$ = new std::vector<unsigned>{$1}; }
|
||||
| pgame_succs ',' INT
|
||||
{
|
||||
$$ = $1;
|
||||
$$->emplace_back($3);
|
||||
}
|
||||
|
||||
pgame_node: INT INT INT pgame_succs string_opt
|
||||
{
|
||||
unsigned state = $1;
|
||||
unsigned owner = $3;
|
||||
if (owner > 1)
|
||||
{
|
||||
error(@3, "node owner should be 0 or 1");
|
||||
owner = 0;
|
||||
}
|
||||
// Create any missing state
|
||||
unsigned max_state = state;
|
||||
for (unsigned s: *$4)
|
||||
max_state = std::max(max_state, s);
|
||||
unsigned n = res.h->aut->num_states();
|
||||
if (n <= max_state)
|
||||
res.h->aut->new_states(max_state + 1 - n);
|
||||
|
||||
// assume the source of the first edge is initial
|
||||
if (res.start.empty())
|
||||
res.start.emplace_back(@$, std::vector<unsigned>{state});
|
||||
|
||||
// Create all edges with priority $2
|
||||
spot::acc_cond::mark_t m({$2});
|
||||
for (unsigned s: *$4)
|
||||
res.h->aut->new_edge(state, s, bddtrue, m);
|
||||
res.accset = std::max(res.accset, 1 + (int) $2);
|
||||
|
||||
n = res.h->aut->num_states();
|
||||
if (!res.state_player)
|
||||
res.state_player = new std::vector<bool>(n);
|
||||
else if (res.state_player->size() < n)
|
||||
res.state_player->resize(n);
|
||||
(*res.state_player)[state] = owner;
|
||||
|
||||
if (std::string* name = $5)
|
||||
{
|
||||
if (!res.state_names)
|
||||
res.state_names = new std::vector<std::string>(n);
|
||||
else if (res.state_names->size() < n)
|
||||
res.state_names->resize(n);
|
||||
(*res.state_names)[state] = std::move(*name);
|
||||
delete name;
|
||||
}
|
||||
}
|
||||
|
||||
/**********************************************************************/
|
||||
/* Rules for neverclaims */
|
||||
/**********************************************************************/
|
||||
|
|
|
|||
|
|
@ -44,7 +44,14 @@ namespace spot
|
|||
struct parse_aut_error_list {};
|
||||
#endif
|
||||
|
||||
enum class parsed_aut_type { HOA, NeverClaim, LBTT, DRA, DSA, Unknown };
|
||||
enum class parsed_aut_type {
|
||||
HOA,
|
||||
NeverClaim,
|
||||
LBTT,
|
||||
DRA, /* DSTAR format for Rabin */
|
||||
DSA, /* DSTAR format for Streett */
|
||||
PGAME, /* PG Solver Game */
|
||||
Unknown };
|
||||
|
||||
/// \brief Result of the automaton parser
|
||||
struct SPOT_API parsed_aut final
|
||||
|
|
|
|||
|
|
@ -65,12 +65,18 @@ eol \n+|\r+
|
|||
eol2 (\n\r)+|(\r\n)+
|
||||
eols ({eol}|{eol2})*
|
||||
identifier [[:alpha:]_][[:alnum:]_.-]*
|
||||
pgameinit "parity"[ \t]+[0-9]+[ \t]*;
|
||||
oldpgameinit [0-9]+[ \t]+[0-9]+[ \t]+[01]+[ \t]+[0-9,]+([ \t]+".*")?[ \t]*;
|
||||
/* A pattern than match the start of an automaton, in order
|
||||
to detect the end of the previous one. We do not try to match
|
||||
LBTT automata here. */
|
||||
startaut {eols}("HOA:"|"never"|"DSA"|"DRA"|{pgameinit})
|
||||
|
||||
%x in_COMMENT in_STRING in_NEVER_PAR
|
||||
%s in_HOA in_NEVER in_LBTT_HEADER
|
||||
%s in_LBTT_STATE in_LBTT_INIT in_LBTT_TRANS
|
||||
%s in_LBTT_T_ACC in_LBTT_S_ACC in_LBTT_GUARD
|
||||
%s in_DSTAR
|
||||
%s in_DSTAR in_PGAME
|
||||
%%
|
||||
|
||||
%{
|
||||
|
|
@ -127,7 +133,20 @@ identifier [[:alpha:]_][[:alnum:]_.-]*
|
|||
<INITIAL>"never" BEGIN(in_NEVER); return token::NEVER;
|
||||
<INITIAL>"DSA" BEGIN(in_DSTAR); return token::DSA;
|
||||
<INITIAL>"DRA" BEGIN(in_DSTAR); return token::DRA;
|
||||
|
||||
<INITIAL>{pgameinit} {
|
||||
BEGIN(in_PGAME);
|
||||
char* end = nullptr;
|
||||
errno = 0;
|
||||
unsigned long n = strtoul(yytext + 7, &end, 10);
|
||||
yylval->num = n;
|
||||
return token::PGAME;
|
||||
}
|
||||
<INITIAL>{oldpgameinit} {
|
||||
BEGIN(in_PGAME);
|
||||
yylval->num = 0;
|
||||
yyless(0);
|
||||
return token::PGAME;
|
||||
}
|
||||
<INITIAL>[0-9]+[ \t][0-9]+[ts]? {
|
||||
BEGIN(in_LBTT_HEADER);
|
||||
char* end = nullptr;
|
||||
|
|
@ -229,10 +248,8 @@ identifier [[:alpha:]_][[:alnum:]_.-]*
|
|||
return token::INT;
|
||||
}
|
||||
[0-9]+ parse_int(); return token::INT;
|
||||
/* The start of any automaton is the end of this one.
|
||||
We do not try to detect LBTT automata, as that would
|
||||
be too hard to distinguish from state numbers. */
|
||||
{eols}("HOA:"|"never"|"DSA"|"DRA") {
|
||||
/* The start of any automaton is the end of this one. */
|
||||
{startaut} {
|
||||
yylloc->end = yylloc->begin;
|
||||
yyless(0);
|
||||
BEGIN(INITIAL);
|
||||
|
|
@ -270,6 +287,24 @@ identifier [[:alpha:]_][[:alnum:]_.-]*
|
|||
}
|
||||
}
|
||||
|
||||
<in_PGAME>{
|
||||
/* Handle short numbers without going through parse_int() for efficiency. */
|
||||
[0-9] yylval->num = *yytext - '0'; return token::INT;
|
||||
[0-9][0-9] {
|
||||
yylval->num = (yytext[0] * 10) + yytext[1] - '0' * 11;
|
||||
return token::INT;
|
||||
}
|
||||
[0-9]+ parse_int(); return token::INT;
|
||||
/* The start of any automaton is the end of this one. */
|
||||
{startaut} {
|
||||
yylloc->end = yylloc->begin;
|
||||
yyless(0);
|
||||
BEGIN(INITIAL);
|
||||
return token::ENDPGAME;
|
||||
}
|
||||
<<EOF>> return token::ENDPGAME;
|
||||
}
|
||||
|
||||
/* Note: the LBTT format is scanf friendly, but not Bison-friendly.
|
||||
If we only tokenize it as a stream of INTs, the parser will have
|
||||
a very hard time recognizing what is a state from what is a
|
||||
|
|
|
|||
|
|
@ -341,6 +341,7 @@ TESTS_twa = \
|
|||
core/dnfstreett.test \
|
||||
core/parity.test \
|
||||
core/parity2.test \
|
||||
core/pgsolver.test \
|
||||
core/ltlsynt.test \
|
||||
core/ltlsynt-pgame.test \
|
||||
core/syfco.test \
|
||||
|
|
|
|||
265
tests/core/pgsolver.test
Executable file
265
tests/core/pgsolver.test
Executable file
|
|
@ -0,0 +1,265 @@
|
|||
#!/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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./defs
|
||||
|
||||
set -e
|
||||
|
||||
# This is example 6 is the manual of pgsolver 4.1
|
||||
cat >example1.pg <<EOF
|
||||
parity 4;
|
||||
0 6 1 4,2 "Africa";
|
||||
4 5 1 0 "Antarctica";
|
||||
1 8 1 2,4,3 "America";
|
||||
3 6 0 4,2 "Australia";
|
||||
2 7 0 3,1,0,4 "Asia";
|
||||
EOF
|
||||
autfilt example1.pg >out
|
||||
|
||||
rest='(Fin(6) & (Inf(5) | (Fin(4) & (Inf(3) | (Fin(2) & (Inf(1) | Fin(0)))))))'
|
||||
cat >example1.hoa <<EOF
|
||||
HOA: v1
|
||||
States: 5
|
||||
Start: 0
|
||||
AP: 0
|
||||
acc-name: parity max odd 9
|
||||
Acceptance: 9 Fin(8) & (Inf(7) | $rest)
|
||||
properties: trans-labels explicit-labels state-acc colored complete
|
||||
spot-state-player: 1 1 0 0 1
|
||||
--BODY--
|
||||
State: 0 "Africa" {6}
|
||||
[t] 4
|
||||
[t] 2
|
||||
State: 1 "America" {8}
|
||||
[t] 2
|
||||
[t] 4
|
||||
[t] 3
|
||||
State: 2 "Asia" {7}
|
||||
[t] 3
|
||||
[t] 1
|
||||
[t] 0
|
||||
[t] 4
|
||||
State: 3 "Australia" {6}
|
||||
[t] 4
|
||||
[t] 2
|
||||
State: 4 "Antarctica" {5}
|
||||
[t] 0
|
||||
--END--
|
||||
EOF
|
||||
|
||||
diff out example1.hoa
|
||||
|
||||
# The first line should be optional
|
||||
sed 1d example1.pg | autfilt example1.pg >out
|
||||
diff out example1.hoa
|
||||
|
||||
|
||||
# Test streaming.
|
||||
cat >example2.pg <<EOF
|
||||
parity 10;
|
||||
0 0 1 4,9;
|
||||
1 2 1 5,2;
|
||||
2 4 0 6,1;
|
||||
3 5 0 0,2;
|
||||
4 6 0 6,3;
|
||||
5 8 1 7,8;
|
||||
6 10 1 0,8;
|
||||
7 11 1 5,1;
|
||||
8 13 0 1,3;
|
||||
9 14 1 5,6;
|
||||
parity 20;
|
||||
0 0 0 6,5;
|
||||
1 2 1 13,0;
|
||||
2 4 0 7,18;
|
||||
3 5 0 8,4;
|
||||
4 6 0 0,19;
|
||||
5 8 0 12,18;
|
||||
6 9 0 16,17;
|
||||
7 11 1 14,2;
|
||||
8 13 1 15,1;
|
||||
9 15 0 11,10;
|
||||
10 16 1 14,9;
|
||||
11 17 1 16,14;
|
||||
12 19 1 9,1;
|
||||
13 21 0 11,17;
|
||||
14 22 1 12,8;
|
||||
15 24 1 5,1;
|
||||
16 26 1 13,7;
|
||||
17 28 1 10,1;
|
||||
18 29 1 12,6;
|
||||
19 30 1 13,10;
|
||||
never { /* false */
|
||||
accept_init:
|
||||
T0_init:
|
||||
do
|
||||
:: atomic { (false) -> assert(!(false)) }
|
||||
od;
|
||||
accept_all:
|
||||
skip
|
||||
}
|
||||
EOF
|
||||
autfilt example2.pg >out
|
||||
parity15=`randaut -A'parity max odd 15' -Q1 0 | grep Acceptance`
|
||||
parity31=`randaut -A'parity max odd 31' -Q1 0 | grep Acceptance`
|
||||
cat > example2.hoa <<EOF
|
||||
HOA: v1
|
||||
States: 10
|
||||
Start: 0
|
||||
AP: 0
|
||||
acc-name: parity max odd 15
|
||||
$parity15
|
||||
properties: trans-labels explicit-labels state-acc colored complete
|
||||
spot-state-player: 1 1 0 0 0 1 1 1 0 1
|
||||
--BODY--
|
||||
State: 0 {0}
|
||||
[t] 4
|
||||
[t] 9
|
||||
State: 1 {2}
|
||||
[t] 5
|
||||
[t] 2
|
||||
State: 2 {4}
|
||||
[t] 6
|
||||
[t] 1
|
||||
State: 3 {5}
|
||||
[t] 0
|
||||
[t] 2
|
||||
State: 4 {6}
|
||||
[t] 6
|
||||
[t] 3
|
||||
State: 5 {8}
|
||||
[t] 7
|
||||
[t] 8
|
||||
State: 6 {10}
|
||||
[t] 0
|
||||
[t] 8
|
||||
State: 7 {11}
|
||||
[t] 5
|
||||
[t] 1
|
||||
State: 8 {13}
|
||||
[t] 1
|
||||
[t] 3
|
||||
State: 9 {14}
|
||||
[t] 5
|
||||
[t] 6
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 20
|
||||
Start: 0
|
||||
AP: 0
|
||||
acc-name: parity max odd 31
|
||||
$parity31
|
||||
properties: trans-labels explicit-labels state-acc colored complete
|
||||
spot-state-player: 0 1 0 0 0 0 0 1 1 0 1 1 1 0 1 1 1 1 1 1
|
||||
--BODY--
|
||||
State: 0 {0}
|
||||
[t] 6
|
||||
[t] 5
|
||||
State: 1 {2}
|
||||
[t] 13
|
||||
[t] 0
|
||||
State: 2 {4}
|
||||
[t] 7
|
||||
[t] 18
|
||||
State: 3 {5}
|
||||
[t] 8
|
||||
[t] 4
|
||||
State: 4 {6}
|
||||
[t] 0
|
||||
[t] 19
|
||||
State: 5 {8}
|
||||
[t] 12
|
||||
[t] 18
|
||||
State: 6 {9}
|
||||
[t] 16
|
||||
[t] 17
|
||||
State: 7 {11}
|
||||
[t] 14
|
||||
[t] 2
|
||||
State: 8 {13}
|
||||
[t] 15
|
||||
[t] 1
|
||||
State: 9 {15}
|
||||
[t] 11
|
||||
[t] 10
|
||||
State: 10 {16}
|
||||
[t] 14
|
||||
[t] 9
|
||||
State: 11 {17}
|
||||
[t] 16
|
||||
[t] 14
|
||||
State: 12 {19}
|
||||
[t] 9
|
||||
[t] 1
|
||||
State: 13 {21}
|
||||
[t] 11
|
||||
[t] 17
|
||||
State: 14 {22}
|
||||
[t] 12
|
||||
[t] 8
|
||||
State: 15 {24}
|
||||
[t] 5
|
||||
[t] 1
|
||||
State: 16 {26}
|
||||
[t] 13
|
||||
[t] 7
|
||||
State: 17 {28}
|
||||
[t] 10
|
||||
[t] 1
|
||||
State: 18 {29}
|
||||
[t] 12
|
||||
[t] 6
|
||||
State: 19 {30}
|
||||
[t] 13
|
||||
[t] 10
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 2
|
||||
Start: 0
|
||||
AP: 0
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc colored
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
State: 0 {0}
|
||||
[f] 1
|
||||
State: 1 {0}
|
||||
[t] 1
|
||||
--END--
|
||||
EOF
|
||||
diff out example2.hoa
|
||||
|
||||
|
||||
cat >example3.pg <<EOF
|
||||
parity 4;
|
||||
0 6 1 4,2;
|
||||
4 5 1 0;
|
||||
1 8 1 2,4,3;
|
||||
3 6 20 4,2;
|
||||
2 7 3 3,1,0,4;
|
||||
EOF
|
||||
autfilt example3.pg >stdout 2>stderr && exit 1
|
||||
cat >expected.err<<EOF
|
||||
example3.pg:5.5-6: node owner should be 0 or 1
|
||||
example3.pg:6.5: node owner should be 0 or 1
|
||||
EOF
|
||||
diff stderr expected.err
|
||||
sed 's/ ".*"//g' example1.hoa > example3.hoa
|
||||
diff stdout example3.hoa
|
||||
File diff suppressed because it is too large
Load diff
Loading…
Add table
Add a link
Reference in a new issue