From c87c13db67efee4a7f816086d9fdd616d61c5a6f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 24 May 2018 13:36:17 +0200 Subject: [PATCH] autfilt: better handling of chain of products with -B Fixes #348, reported by Jeroen Meijer. * bin/autfilt.cc: If -B is used with many --product, degeneralize intermediate products as needed. * NEWS: Mention the change. * tests/core/prodchain.test: New file. * tests/Makefile.am: Add it. * spot/twa/acc.cc, spot/twa/acc.hh: Fix reporting of overflow. * tests/core/acc.cc: Adjust. --- NEWS | 7 ++++++ bin/autfilt.cc | 47 ++++++++++++++++++++++++++++++++----- spot/twa/acc.cc | 8 +++++++ spot/twa/acc.hh | 47 +++++++++++++++++++++++++++++++------ tests/Makefile.am | 1 + tests/core/acc.cc | 9 +++---- tests/core/prodchain.test | 49 +++++++++++++++++++++++++++++++++++++++ 7 files changed, 149 insertions(+), 19 deletions(-) create mode 100755 tests/core/prodchain.test diff --git a/NEWS b/NEWS index cee198016..7728469e8 100644 --- a/NEWS +++ b/NEWS @@ -15,6 +15,13 @@ New in spot 2.5.3.dev (not yet released) - ltlcross, ltldo, and autcross learned shorthands to call delag, ltl2dra, ltl2dgra, and nba2dpa. + - When autfilt is asked to build a Büchi automaton from + of a chain of many products, as in + "autfilt -B --product 1.hoa ... --product n.hoa in.hoa" + then it will automatically degeneralize the intermediate + product to avoid exceeding the number of supported + acceptance sets. + Library: - You can now specify to Spot the number of acceptance marks you diff --git a/bin/autfilt.cc b/bin/autfilt.cc index e51450cbb..9890bd579 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -50,6 +50,7 @@ #include #include #include +#include #include #include #include @@ -634,6 +635,40 @@ ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false) return p.run(aut); } +static spot::twa_graph_ptr ensure_tba(spot::twa_graph_ptr aut) +{ + spot::postprocessor p; + p.set_type(spot::postprocessor::TGBA); + p.set_pref(spot::postprocessor::Any); + p.set_level(spot::postprocessor::Low); + return spot::degeneralize_tba(p.run(aut)); + +} + +static spot::twa_graph_ptr +product(spot::twa_graph_ptr left, spot::twa_graph_ptr right) +{ + if ((type == spot::postprocessor::BA) + && (left->num_sets() + right->num_sets() > SPOT_NB_ACC)) + { + left = ensure_tba(left); + right = ensure_tba(right); + } + return spot::product(left, right); +} + +static spot::twa_graph_ptr +product_or(spot::twa_graph_ptr left, spot::twa_graph_ptr right) +{ + if ((type == spot::postprocessor::BA) + && (left->num_sets() + right->num_sets() > SPOT_NB_ACC)) + { + left = ensure_tba(left); + right = ensure_tba(right); + } + return spot::product_or(left, right); +} + static int parse_opt(int key, char* arg, struct argp_state*) { @@ -947,8 +982,8 @@ parse_opt(int key, char* arg, struct argp_state*) if (!opt->product_and) opt->product_and = std::move(a); else - opt->product_and = spot::product(std::move(opt->product_and), - std::move(a)); + opt->product_and = ::product(std::move(opt->product_and), + std::move(a)); } break; case OPT_PRODUCT_OR: @@ -957,8 +992,8 @@ parse_opt(int key, char* arg, struct argp_state*) if (!opt->product_or) opt->product_or = std::move(a); else - opt->product_or = spot::product_or(std::move(opt->product_or), - std::move(a)); + opt->product_or = ::product_or(std::move(opt->product_or), + std::move(a)); } break; case OPT_RANDOMIZE: @@ -1410,9 +1445,9 @@ namespace aut->purge_unreachable_states(); if (opt->product_and) - aut = spot::product(std::move(aut), opt->product_and); + aut = ::product(std::move(aut), opt->product_and); if (opt->product_or) - aut = spot::product_or(std::move(aut), opt->product_or); + aut = ::product_or(std::move(aut), opt->product_or); if (opt->sum_or) aut = spot::sum(std::move(aut), opt->sum_or); diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 4286c06bc..87aab2f83 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -32,6 +32,14 @@ namespace spot { + void acc_cond::report_too_many_sets() + { +#define STR(x) #x +#define VALUESTR(x) STR(x) + throw std::runtime_error("Too many acceptance sets used. " + "The limit is " VALUESTR(SPOT_NB_ACC) "."); + } + std::ostream& operator<<(std::ostream& os, spot::acc_cond::mark_t m) { auto a = m; diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 253cd608b..921c06a86 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -46,6 +46,11 @@ namespace spot class SPOT_API acc_cond { + +#ifndef SWIG + private: + [[noreturn]] static void report_too_many_sets(); +#endif public: struct mark_t : public internal::_32acc { @@ -214,24 +219,52 @@ namespace spot mark_t operator<<(unsigned i) const { - return id << i; + try + { + return id << i; + } + catch (const std::runtime_error& e) + { + report_too_many_sets(); + } } mark_t& operator<<=(unsigned i) { - id <<= i; - return *this; + try + { + id <<= i; + return *this; + } + catch (const std::runtime_error& e) + { + report_too_many_sets(); + } } mark_t operator>>(unsigned i) const { - return id >> i; + try + { + return id >> i; + } + catch (const std::runtime_error& e) + { + report_too_many_sets(); + } } mark_t& operator>>=(unsigned i) { - id >>= i; - return *this; + try + { + id >>= i; + return *this; + } + catch (const std::runtime_error& e) + { + report_too_many_sets(); + } } mark_t strip(mark_t y) const @@ -1229,7 +1262,7 @@ namespace spot unsigned j = num_; num_ += num; if (num_ > SPOT_NB_ACC) - throw std::runtime_error("Too many acceptance sets used."); + report_too_many_sets(); all_ = all_sets_(); return j; } diff --git a/tests/Makefile.am b/tests/Makefile.am index bba62bffa..bf3eaefd4 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -229,6 +229,7 @@ TESTS_twa = \ core/ltldo2.test \ core/maskacc.test \ core/maskkeep.test \ + core/prodchain.test \ core/prodor.test \ core/simdet.test \ core/sim2.test \ diff --git a/tests/core/acc.cc b/tests/core/acc.cc index 7ac6e5aeb..24443a1dd 100644 --- a/tests/core/acc.cc +++ b/tests/core/acc.cc @@ -189,8 +189,7 @@ int main() } catch (const std::runtime_error& e) { - if (std::strcmp(e.what(), "Too many acceptance sets used.")) - return 1; + assert(!std::strncmp(e.what(), "Too many acceptance sets used.", 30)); } try @@ -200,8 +199,7 @@ int main() } catch (const std::runtime_error& e) { - if (std::strcmp(e.what(), "bit shift overflow is undefined behavior")) - return 1; + assert(!std::strncmp(e.what(), "Too many acceptance sets used.", 30)); } try @@ -211,8 +209,7 @@ int main() } catch (const std::runtime_error& e) { - if (std::strcmp(e.what(), "bit shift overflow is undefined behavior")) - return 1; + assert(!std::strncmp(e.what(), "Too many acceptance sets used.", 30)); } return 0; diff --git a/tests/core/prodchain.test b/tests/core/prodchain.test new file mode 100755 index 000000000..b5037782f --- /dev/null +++ b/tests/core/prodchain.test @@ -0,0 +1,49 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2018 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 + +set x +shift +for i in `seq 1 42`; do + ltl2tgba "{a[*$i]}[]->GFb" > $i.hoa +done +for i in *.hoa; do + set x "$@" --product $i + shift +done +shift +autfilt "$@" 2> error && exit 1 +grep 'Too many acceptance sets used' error +autfilt -B "$@" > result +test "127,253,508,1" = `autfilt --stats=%s,%e,%t,%a result` + +set x +shift +for i in *.hoa; do + set x "$@" --product-or $i + shift +done +shift +autfilt "$@" 2> error && exit 1 +grep 'Too many acceptance sets used' error +autfilt -B "$@" > result +test "45,89,180,1" = `autfilt --stats=%s,%e,%t,%a result`