From 444e2b5b89175e203d880a20e29f607d94bd2323 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 22 Jul 2022 10:49:23 +0200 Subject: [PATCH] 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. --- NEWS | 6 +- spot/parseaut/parseaut.yy | 110 +++- spot/parseaut/public.hh | 19 +- spot/parseaut/scanaut.ll | 47 +- tests/Makefile.am | 1 + tests/core/pgsolver.test | 265 ++++++++++ tests/python/games.ipynb | 1038 +++++++++++++++++++++++++------------ 7 files changed, 1144 insertions(+), 342 deletions(-) create mode 100755 tests/core/pgsolver.test diff --git a/NEWS b/NEWS index d7f3f4923..7e6bd6a40 100644 --- a/NEWS +++ b/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 diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 71ab8aaea..52d448c16 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -44,6 +44,7 @@ #include "spot/priv/accmap.hh" #include #include +#include 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 '[' +%token LINEDIRECTIVE "#line" +%token 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 LINEDIRECTIVE "#line" -%token BDD %left '|' %left '&' %precedence '!' -%type init-state-conj-2 state-conj-2 state-conj-checked +%type init-state-conj-2 state-conj-2 state-conj-checked pgame_succs %type checked-state-num state-num acc-set sign %type label-expr %type 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 nc-one-ident nc-ident-list %type 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 LBTT "LBTT header" %token INT_S "state acceptance" %token 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{$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{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(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(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 */ /**********************************************************************/ @@ -2487,7 +2583,7 @@ static void fix_initial_state(result_& r) start.resize(std::distance(start.begin(), res)); assert(start.size() >= 1); - if (start.size() == 1) + if (start.size() == 1) { if (r.opts.want_kripke) r.h->ks->set_init_state(start.front().front()); diff --git a/spot/parseaut/public.hh b/spot/parseaut/public.hh index d1c1793be..ec16b3ad7 100644 --- a/spot/parseaut/public.hh +++ b/spot/parseaut/public.hh @@ -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 @@ -91,11 +98,11 @@ namespace spot struct automaton_parser_options final { - bool ignore_abort = false; ///< Skip aborted automata - bool debug = false; ///< Run the parser in debug mode? - bool trust_hoa = true; ///< Trust properties in HOA files - bool raise_errors = false; ///< Raise errors as exceptions. - bool want_kripke = false; ///< Parse as a Kripke structure. + bool ignore_abort = false; ///< Skip aborted automata + bool debug = false; ///< Run the parser in debug mode? + bool trust_hoa = true; ///< Trust properties in HOA files + bool raise_errors = false; ///< Raise errors as exceptions. + bool want_kripke = false; ///< Parse as a Kripke structure. }; /// \brief Parse a stream of automata diff --git a/spot/parseaut/scanaut.ll b/spot/parseaut/scanaut.ll index db8ae75c6..c04834975 100644 --- a/spot/parseaut/scanaut.ll +++ b/spot/parseaut/scanaut.ll @@ -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:]_.-]* "never" BEGIN(in_NEVER); return token::NEVER; "DSA" BEGIN(in_DSTAR); return token::DSA; "DRA" BEGIN(in_DSTAR); return token::DRA; - +{pgameinit} { + BEGIN(in_PGAME); + char* end = nullptr; + errno = 0; + unsigned long n = strtoul(yytext + 7, &end, 10); + yylval->num = n; + return token::PGAME; + } +{oldpgameinit} { + BEGIN(in_PGAME); + yylval->num = 0; + yyless(0); + return token::PGAME; + } [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:]_.-]* } } +{ + /* 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; + } + <> 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 diff --git a/tests/Makefile.am b/tests/Makefile.am index a13a495b3..91d3f10ea 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -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 \ diff --git a/tests/core/pgsolver.test b/tests/core/pgsolver.test new file mode 100755 index 000000000..e767e1953 --- /dev/null +++ b/tests/core/pgsolver.test @@ -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 . + +. ./defs + +set -e + +# This is example 6 is the manual of pgsolver 4.1 +cat >example1.pg <out + +rest='(Fin(6) & (Inf(5) | (Fin(4) & (Inf(3) | (Fin(2) & (Inf(1) | Fin(0)))))))' +cat >example1.hoa <out +diff out example1.hoa + + +# Test streaming. +cat >example2.pg < 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 <example3.pg <stdout 2>stderr && exit 1 +cat >expected.err< example3.hoa +diff stdout example3.hoa diff --git a/tests/python/games.ipynb b/tests/python/games.ipynb index f3ffd7502..fcc2bf12c 100644 --- a/tests/python/games.ipynb +++ b/tests/python/games.ipynb @@ -47,153 +47,153 @@ "\n", "\n", - "\n", "\n", "\n", "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "2->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "6->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "7->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -285,153 +285,153 @@ "\n", "\n", - "\n", "\n", "\n", "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "2->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "6->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "7->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -501,153 +501,153 @@ "\n", "\n", - "\n", "\n", "\n", "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", "\n", - "0\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", "\n", - "1\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", "\n", - "3\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", "\n", - "2\n", + "2\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", "\n", - "4\n", + "4\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", "\n", - "6\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", "\n", - "5\n", + "5\n", "\n", "\n", "\n", "2->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7\n", "\n", - "7\n", + "7\n", "\n", "\n", "\n", "6->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", "\n", - "8\n", + "8\n", "\n", "\n", "\n", "7->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -670,7 +670,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "## Input/Output\n", + "## Input/Output in HOA format\n", "\n", "An extension of the HOA format makes it possible to store the `state-player` property. This allows us to read the parity game constructed by `ltlsynt` using `spot.automaton()` like any other automaton." ] @@ -686,218 +686,218 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "⓿\n", - ")\n", - "[co-Büchi]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "0->5\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "0->6\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "5->1\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "5->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "6->2\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "6->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "1->7\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "1->8\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "7->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "8->2\n", - "\n", - "\n", - "1\n", - "⓿\n", + "\n", + "\n", + "1\n", + "⓿\n", "\n", "\n", "\n", "2->7\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "3->9\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "9->3\n", - "\n", - "\n", - "b\n", - "⓿\n", + "\n", + "\n", + "b\n", + "⓿\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "9->4\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "4->10\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "10->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f6be431fbd0> >" + " *' at 0x7f8f1861bd20> >" ] }, "execution_count": 8, @@ -1013,218 +1013,218 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "⓿\n", - ")\n", - "[co-Büchi]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "⓿\n", + ")\n", + "[co-Büchi]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "0->5\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "0->6\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "5->1\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "5->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "6->2\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "6->3\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "1->7\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "1->8\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "7->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "8->2\n", - "\n", - "\n", - "1\n", - "⓿\n", + "\n", + "\n", + "1\n", + "⓿\n", "\n", "\n", "\n", "2->7\n", - "\n", - "\n", - "!a\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", - "a\n", - "⓿\n", + "\n", + "\n", + "a\n", + "⓿\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "3->9\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "9->3\n", - "\n", - "\n", - "b\n", - "⓿\n", + "\n", + "\n", + "b\n", + "⓿\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "9->4\n", - "\n", - "\n", - "!b\n", + "\n", + "\n", + "!b\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "4->10\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "10->4\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f6be431fcf0> >" + " *' at 0x7f8f187f5ef0> >" ] }, "execution_count": 11, @@ -1235,11 +1235,405 @@ "source": [ "spot.highlight_strategy(game)" ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Input in PGSolver format\n", + "\n", + "The automaton parser is also able to parse the [PGSolver](https://github.com/tcsprojects/pgsolver) format. Here are two examples from the manual of PGSolver. The support for C-style comments is not part of the PGSolver format.\n", + "\n", + "Note that we use diamond node for player 1, while PGSolver use those of player 0. Also in Spot the acceptance condition is what Player 1 should satisfy; player 0 has two way to not satisfy it: leading to a rejecting cycle, or to a state without successor. In PGSolver, the graph is assumed to be total (i.e. each state has a successor), so player 0 can only win by reaching a rejecting cycle, which is equivalent to a `parity max even` acceptance." + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "❽\n", + ") & (Inf(\n", + "❼\n", + ") | (Fin(\n", + "❻\n", + ") & (Inf(\n", + "❺\n", + ") | (Fin(\n", + "❹\n", + ") & (Inf(\n", + "❸\n", + ") | (Fin(\n", + "❷\n", + ") & (Inf(\n", + "❶\n", + ") | Fin(\n", + "⓿\n", + "))))))))\n", + "[parity max odd 9]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "Africa\n", + "❻\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "Antarctica\n", + "❺\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "Asia\n", + "❼\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "America\n", + "❽\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "Australia\n", + "❻\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "❶\n", + ") | Fin(\n", + "⓿\n", + ")\n", + "[Streett 1]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "⓿\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "❶\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "⓿\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "❶\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "⓿\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "❶\n", + "\n", + "\n", + "\n", + "3->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "⓿\n", + "\n", + "\n", + "\n", + "4->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "❶\n", + "\n", + "\n", + "\n", + "5->7\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "6->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "6->7\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7->1\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "a,b = spot.automata(\"\"\"\n", + "parity 4; /* Example 6 in the manual for PGSolver 4.1 */\n", + "0 6 1 4,2 \"Africa\";\n", + "4 5 1 0 \"Antarctica\";\n", + "1 8 1 2,4,3 \"America\";\n", + "3 6 0 4,2 \"Australia\";\n", + "2 7 0 3,1,0,4 \"Asia\";\n", + "parity 8; /* Example 7 in the manual for PGSolver 4.1 */\n", + "0 0 0 1,2;\n", + "1 1 1 2,3;\n", + "2 0 0 3,4;\n", + "3 1 1 4,5;\n", + "4 0 0 5,6;\n", + "5 1 1 6,7;\n", + "6 0 0 7,0;\n", + "7 1 1 0,1;\n", + "\"\"\")\n", + "spot.solve_game(a)\n", + "spot.highlight_strategy(a)\n", + "spot.solve_game(b)\n", + "spot.highlight_strategy(b)\n", + "display(a.show('.g'), b.show('.g'))" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, @@ -1253,7 +1647,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.7.3" + "version": "3.10.5" } }, "nbformat": 4,