From 8c33f959a334238bc3273bbff28e7c6a116b9c78 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 3 Jan 2022 18:04:29 +0100 Subject: [PATCH] hoa: add support for controllable-AP * doc/spot.bib (perez.19.hoa): New entry. * spot/parseaut/public.hh: Mention it. * spot/parseaut/parseaut.yy, spot/parseaut/scanaut.ll: Learn to parse the controllable-AP header. * spot/twaalgos/hoa.cc: Print it. * tests/core/ltlsynt.test, tests/core/parseaut.test, tests/core/readsave.test, tests/python/_synthesis.ipynb, tests/python/except.py, tests/python/games.ipynb, tests/python/mealy.py, tests/python/synthesis.py: Adjust or augment test cases. --- NEWS | 4 +++ doc/spot.bib | 9 +++++++ spot/parseaut/parseaut.yy | 50 ++++++++++++++++++++++++++++++++++- spot/parseaut/public.hh | 8 +++++- spot/parseaut/scanaut.ll | 3 ++- spot/twaalgos/hoa.cc | 18 ++++++++++++- tests/core/ltlsynt.test | 5 +++- tests/core/parseaut.test | 15 ++++++++--- tests/core/readsave.test | 5 +++- tests/python/_synthesis.ipynb | 9 +++++++ tests/python/except.py | 13 ++++++++- tests/python/games.ipynb | 1 + tests/python/mealy.py | 6 ++--- tests/python/synthesis.py | 3 ++- 14 files changed, 134 insertions(+), 15 deletions(-) diff --git a/NEWS b/NEWS index d76130a12..993a2dbfd 100644 --- a/NEWS +++ b/NEWS @@ -18,6 +18,10 @@ New in spot 2.10.2.dev (not yet released) - sbacc() learned to take the "original-classes" property into account and preserve it. + - The HOA parser and printer learned to map the synthesis-outputs + property of Spot to the controllable-AP header for the Extended + HOA format used in SyntComp. https://arxiv.org/abs/1912.05793 + Bugs fixed: - On automata where the absence of color is not rejecting diff --git a/doc/spot.bib b/doc/spot.bib index 6092de0a5..5405a2322 100644 --- a/doc/spot.bib +++ b/doc/spot.bib @@ -726,6 +726,15 @@ doi = {10.1007/978-3-540-73370-6_17} } +@Misc{ perez.19.hoa, + author = {Guillermo A. P{\'{e}}rez}, + title = {The Extended {HOA} Format for Synthesis}, + howpublished = {ArXiv}, + month = {dec}, + year = {2019}, + url = {http://arxiv.org/abs/1912.05793} +} + @InProceedings{ piterman.06.vmcai, author = {Nir Piterman and Amir Pnueli and Yaniv Sa'ar}, editor = {E. Allen Emerson and Kedar S. Namjoshi"}, diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index c71636bde..5328c576b 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -1,5 +1,5 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2014-2021 Laboratoire de Recherche et Développement +** Copyright (C) 2014-2022 Laboratoire de Recherche et Développement ** de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. @@ -97,6 +97,10 @@ extern "C" int strverscmp(const char *s1, const char *s2); named_tgba_t* namer = nullptr; spot::acc_mapper_int* acc_mapper = nullptr; std::vector ap; + std::vector controllable_ap; + bool has_controllable_ap = false; + std::vector controllable_ap_loc; + spot::location controllable_aps_loc; std::vector guards; std::vector::const_iterator cur_guard; // If "Alias: ..." occurs before "AP: ..." in the HOA format we @@ -233,6 +237,7 @@ extern "C" int strverscmp(const char *s1, const char *s2); %token ALIAS "Alias:" %token ACCEPTANCE "Acceptance:" %token ACCNAME "acc-name:" +%token CONTROLLABLE_AP "controllable-AP:" %token TOOL "tool:" %token NAME "name:" %token PROPERTIES "properties:" @@ -404,6 +409,37 @@ header: format-version header-items for (auto& p: res.alias) p.second = bddtrue; } + if (res.has_controllable_ap) + { + if (!res.ignore_more_ap && !res.controllable_ap.empty()) + { + error(res.controllable_aps_loc, + "controllable-AP without AP declaration"); + } + else + { + bdd cont = bddtrue; + unsigned n = res.controllable_ap.size(); + unsigned maxap = res.ap.size(); + for (unsigned i = 0; i < n; ++i) + { + unsigned c = res.controllable_ap[i]; + if (c >= maxap) + { + error(res.controllable_ap_loc[i], + "controllable AP number is larger than" + " the number of APs..."); + error(res.ap_loc, "... declared here."); + } + else + { + cont &= bdd_ithvar(res.ap[c]); + } + } + res.aut_or_ks->set_named_prop("synthesis-outputs", + new bdd(cont)); + } + } // Process properties. { auto explicit_labels = res.prop_is_true("explicit-labels"); @@ -683,6 +719,13 @@ version: IDENTIFIER format-version: "HOA:" { res.h->loc = @1; } version +controllable-aps: %empty + | controllable-aps INT + { + res.controllable_ap.push_back($2); + res.controllable_ap_loc.push_back(@2); + } + aps: "AP:" INT { if (res.ignore_more_ap) @@ -766,6 +809,11 @@ header-item: "States:" INT res.start.emplace_back(@$, std::vector{$2}); } | aps + | "controllable-AP:" controllable-aps + { + res.controllable_aps_loc = @1; + res.has_controllable_ap = true; + } | "Alias:" ANAME { res.in_alias=true; } label-expr { res.in_alias = false; diff --git a/spot/parseaut/public.hh b/spot/parseaut/public.hh index 342057407..d1c1793be 100644 --- a/spot/parseaut/public.hh +++ b/spot/parseaut/public.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche et +// Copyright (C) 2013, 2014, 2015, 2016, 2017, 2022 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -117,6 +117,12 @@ namespace spot /// tool that produce Büchi automata in the form of a neverclaim, /// but is not understood by this parser, please report it to /// spot@lrde.epita.fr. + /// + /// The parser for HOA recognize a few extensions. It maps the + /// `controlled-AP:` header \cite perez.19.hoa to the + /// `synthesis-output` property of Spot. It also maps + /// `spot.highlight.edges:`, `spot.highlight.states:`, and + /// `spot.state-player:` to the associated automata properties. class SPOT_API automaton_stream_parser final { spot::location last_loc; diff --git a/spot/parseaut/scanaut.ll b/spot/parseaut/scanaut.ll index c1c4fb44f..4b4d03c37 100644 --- a/spot/parseaut/scanaut.ll +++ b/spot/parseaut/scanaut.ll @@ -1,5 +1,5 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2014-2018, 2020, 2021 Laboratoire de Recherche et Développement +** Copyright (C) 2014-2018, 2020, 2021, 2022 Laboratoire de Recherche et Développement ** de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. @@ -145,6 +145,7 @@ identifier [[:alpha:]_][[:alnum:]_.-]* "Alias:" return token::ALIAS; "Acceptance:" return token::ACCEPTANCE; "acc-name:" return token::ACCNAME; + "controllable-AP:" return token::CONTROLLABLE_AP; "tool:" return token::TOOL; "name:" return token::NAME; "properties:" return token::PROPERTIES; diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index 6c474fb2a..eb5cd3431 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2021 Laboratoire de Recherche et +// Copyright (C) 2014-2022 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -627,6 +627,22 @@ namespace spot } os << nl; } + if (auto synout = aut->get_named_prop("synthesis-outputs")) + { + bdd vars = bdd_support(*synout); + os << "controllable-AP:"; + while (vars != bddtrue) + { + int v = bdd_var(vars); + vars = bdd_high(vars); + if (auto p = md.ap.find(v); p != md.ap.end()) + os << ' ' << p->second; + else + throw std::runtime_error("print_hoa(): synthesis-outputs has " + "unregistered proposition"); + } + os << nl; + } // If we want to output implicit labels, we have to // fill a vector with all destinations in order. diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 4d318dbae..24a53556a 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017, 2019-2021 Laboratoire de Recherche et +# Copyright (C) 2017, 2019-2022 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -373,6 +373,7 @@ AP: 1 "p0" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic +controllable-AP: 0 --BODY-- State: 0 [t] 1 @@ -394,6 +395,7 @@ AP: 1 "p0" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic +controllable-AP: 0 --BODY-- State: 0 [!0] 0 @@ -529,6 +531,7 @@ AP: 3 "a" "b" "c" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic +controllable-AP: 2 --BODY-- State: 0 [!0&!2 | !1&!2] 0 diff --git a/tests/core/parseaut.test b/tests/core/parseaut.test index c882b4093..530047a01 100755 --- a/tests/core/parseaut.test +++ b/tests/core/parseaut.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014-2018, 2020-2021 Laboratoire de Recherche et +# Copyright (C) 2014-2018, 2020-2022 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -165,6 +165,7 @@ HOA: v1 AP: 1 "a" States: 0 AP: 2 "a" "b" +controllable-AP: 3 2 Acceptance: 0 t --BODY-- --END-- @@ -184,7 +185,11 @@ EOF expecterr input <input <input <input <