From eca96cdf80cf9ad4bdb8cd83d1738ace2d004c56 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 21 May 2018 10:24:25 +0200 Subject: [PATCH] parseaut: accept Alias: before AP: Fixes #345. * spot/parseaut/parseaut.yy: Deal with this inconvenient order. * tests/core/parseaut.test: Test it. * NEWS: Mention the bug fix. --- NEWS | 3 ++ spot/parseaut/parseaut.yy | 68 ++++++++++++++++++++++++++++++++++--- tests/core/parseaut.test | 71 +++++++++++++++++++++++++++++++++++++-- 3 files changed, 135 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index 4af447368..d1d71071e 100644 --- a/NEWS +++ b/NEWS @@ -96,6 +96,9 @@ New in spot 2.5.3.dev (not yet released) - print_dot() will correctly escape strings containing \n in HTML mode. + - The HOA parser will now accept Alias: declarations that occur + before AP:. + New in spot 2.5.3 (2018-04-20) Bugs fixed: diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index f926d28b6..be7df7ff6 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -95,6 +95,18 @@ extern "C" int strverscmp(const char *s1, const char *s2); std::vector ap; std::vector guards; std::vector::const_iterator cur_guard; + // If "Alias: ..." occurs before "AP: ..." in the HOA format we + // are in trouble because the parser would like to turn each + // alias into a BDD, yet the atomic proposition have not been + // declared yet. We solve that by using arbitrary BDD variables + // numbers (in fact we use the same number given in the Alias: + // definition) and keeping track of the highest variable number + // we have seen (unknown_ap_max). Once AP: is encountered, + // we can remap everything. If AP: is never encountered an + // unknown_ap_max is non-negative, then we can signal an error. + int unknown_ap_max = -1; + spot::location unknown_ap_max_location; + bool in_alias = false; map_t dest_map; std::vector info_states; // States declared and used. std::vector= 0 && !res.ignore_more_ap) + { + error(res.unknown_ap_max_location, + "atomic proposition used in Alias without AP declaration"); + for (auto& p: res.alias) + p.second = bddtrue; + } // Process properties. { auto explicit_labels = res.prop_is_true("explicit-labels"); @@ -678,6 +697,29 @@ aps: "AP:" INT error(@$, out.str()); } res.ignore_more_ap = true; + // If we have seen Alias: before AP: we have some variable + // renaming to perform. + if (res.unknown_ap_max >= 0) + { + int apsize = res.ap.size(); + if (apsize <= res.unknown_ap_max) + { + error(res.unknown_ap_max_location, + "AP number is larger than the number of APs..."); + error(@1, "... declared here"); + } + bddPair* pair = bdd_newpair(); + int max = std::min(res.unknown_ap_max, apsize - 1); + for (int i = 0; i <= max; ++i) + if (i != res.ap[i]) + bdd_setbddpair(pair, i, res.ap[i]); + bdd extra = bddtrue; + for (unsigned i = apsize; i <= res.unknown_ap_max; ++i) + extra &= bdd_ithvar(i); + for (auto& p: res.alias) + p.second = bdd_restrict(bdd_replace(p.second, pair), extra); + bdd_freepair(pair); + } } } @@ -710,16 +752,17 @@ header-item: "States:" INT res.start.emplace_back(@$, std::vector{$2}); } | aps - | "Alias:" ANAME label-expr + | "Alias:" ANAME { res.in_alias=true; } label-expr { - if (!res.alias.emplace(*$2, bdd_from_int($3)).second) + res.in_alias = false; + if (!res.alias.emplace(*$2, bdd_from_int($4)).second) { std::ostringstream o; o << "ignoring redefinition of alias @" << *$2; error(@$, o.str()); } delete $2; - bdd_delref($3); + bdd_delref($4); } | "Acceptance:" INT { @@ -891,7 +934,7 @@ state-conj-2: checked-state-num '&' checked-state-num } // Same as state-conj-2 except we cannot check the state numbers -// against a number of state that may not have been declared yet. +// against a number of states that may not have been declared yet. init-state-conj-2: state-num '&' state-num { $$ = new std::vector{$1, $3}; @@ -912,7 +955,22 @@ label-expr: 't' } | INT { - if ($1 >= res.ap.size()) + if (res.in_alias && !res.ignore_more_ap) + { + // We are reading Alias: before AP: has been given. + // Use $1 as temporary variable number. We will relabel + // everything once AP: is known. + if (res.unknown_ap_max < (int)$1) + { + res.unknown_ap_max = $1; + res.unknown_ap_max_location = @1; + int missing_vars = 1 + bdd_varnum() - $1; + if (missing_vars > 0) + bdd_extvarnum(missing_vars); + } + $$ = bdd_ithvar($1).id(); + } + else if ($1 >= res.ap.size()) { error(@1, "AP number is larger than the number of APs..."); error(res.ap_loc, "... declared here"); diff --git a/tests/core/parseaut.test b/tests/core/parseaut.test index ca915c74d..338eb39c8 100755 --- a/tests/core/parseaut.test +++ b/tests/core/parseaut.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014-2017 Laboratoire de Recherche et Développement de +# Copyright (C) 2014-2018 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -504,6 +504,37 @@ cat >input <input <input <input <