From 425e8bb37a2105d71c60f6c8b036e732164d25ae Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 27 Mar 2014 18:35:41 +0100 Subject: [PATCH] tgbamask: implement a build_tgba_mask_acc_ignore() function. * src/tgba/tgbamask.hh (build_tgba_mask_acc_ignore): New function. (tgba_mask::wanted): Take an acc argument. * src/tgba/tgbamask.cc: Implement the above. * src/tgbatest/maskacc.cc, src/tgbatest/maskacc.test: New files. * src/tgbatest/Makefile.am: Add them. --- src/tgba/tgbamask.cc | 119 +++++++++++++++++++++++--------------- src/tgba/tgbamask.hh | 20 ++++++- src/tgbatest/.gitignore | 1 + src/tgbatest/Makefile.am | 3 + src/tgbatest/maskacc.cc | 69 ++++++++++++++++++++++ src/tgbatest/maskacc.test | 50 ++++++++++++++++ 6 files changed, 215 insertions(+), 47 deletions(-) create mode 100755 src/tgbatest/maskacc.cc create mode 100755 src/tgbatest/maskacc.test diff --git a/src/tgba/tgbamask.cc b/src/tgba/tgbamask.cc index 1cbdf066e..9fea6a279 100644 --- a/src/tgba/tgbamask.cc +++ b/src/tgba/tgbamask.cc @@ -76,49 +76,8 @@ namespace spot transitions::const_iterator it_; }; - - class tgba_mask_keep: public tgba_mask - { - const state_set& mask_; - public: - tgba_mask_keep(const tgba* masked, - const state_set& mask, - const state* init) - : tgba_mask(masked, init), - mask_(mask) - { - } - - bool wanted(const state* s) const - { - state_set::const_iterator i = mask_.find(s); - return i != mask_.end(); - } - }; - - class tgba_mask_ignore: public tgba_mask - { - const state_set& mask_; - public: - tgba_mask_ignore(const tgba* masked, - const state_set& mask, - const state* init) - : tgba_mask(masked, init), - mask_(mask) - { - } - - bool wanted(const state* s) const - { - state_set::const_iterator i = mask_.find(s); - return i == mask_.end(); - } - }; - - } - tgba_mask::tgba_mask(const tgba* masked, const state* init) : tgba_proxy(masked), @@ -155,19 +114,79 @@ namespace spot for (auto it: original_->succ(state)) { const spot::state* s = it->current_state(); - if (!wanted(s)) + bdd acc = it->current_acceptance_conditions(); + if (!wanted(s, acc)) { s->destroy(); continue; } - transition t = { s, - it->current_condition(), - it->current_acceptance_conditions() }; - res->trans_.push_back(t); + res->trans_.emplace_back(transition {s, it->current_condition(), acc}); } return res; } + namespace + { + + class tgba_mask_keep: public tgba_mask + { + const state_set& mask_; + public: + tgba_mask_keep(const tgba* masked, + const state_set& mask, + const state* init) + : tgba_mask(masked, init), + mask_(mask) + { + } + + bool wanted(const state* s, const bdd&) const + { + state_set::const_iterator i = mask_.find(s); + return i != mask_.end(); + } + }; + + class tgba_mask_ignore: public tgba_mask + { + const state_set& mask_; + public: + tgba_mask_ignore(const tgba* masked, + const state_set& mask, + const state* init) + : tgba_mask(masked, init), + mask_(mask) + { + } + + bool wanted(const state* s, const bdd&) const + { + state_set::const_iterator i = mask_.find(s); + return i == mask_.end(); + } + }; + + class tgba_mask_acc_ignore: public tgba_mask + { + const bdd& mask_; + public: + tgba_mask_acc_ignore(const tgba* masked, + const bdd& mask, + const state* init) + : tgba_mask(masked, init), + mask_(mask) + { + } + + bool wanted(const state*, const bdd& acc) const + { + return (acc & mask_) == bddfalse; + } + }; + + + } + const tgba* build_tgba_mask_keep(const tgba* to_mask, @@ -185,4 +204,12 @@ namespace spot return new tgba_mask_ignore(to_mask, to_ignore, init); } + const tgba* + build_tgba_mask_acc_ignore(const tgba* to_mask, + const bdd to_ignore, + const state* init) + { + return new tgba_mask_acc_ignore(to_mask, to_ignore, init); + } + } diff --git a/src/tgba/tgbamask.hh b/src/tgba/tgbamask.hh index 7c29299da..cd38789da 100644 --- a/src/tgba/tgbamask.hh +++ b/src/tgba/tgbamask.hh @@ -21,6 +21,7 @@ # define SPOT_TGBA_TGBAMASK_HH #include "tgbaproxy.hh" +#include "bdd.h" namespace spot { @@ -50,7 +51,7 @@ namespace spot virtual tgba_succ_iterator* succ_iter(const state* local_state) const; - virtual bool wanted(const state* s) const = 0; + virtual bool wanted(const state* s, const bdd& acc) const = 0; protected: const state* init_; @@ -78,6 +79,23 @@ namespace spot const state_set& to_ignore, const state* init = 0); + + /// \ingroup tgba_on_the_fly_algorithms + /// \brief Mask a TGBA, rejecting some acceptance set of transitions. + /// + /// This will ignore all transitions labeled by the acceptance ACC + /// such that ACC & TO_IGNORE != bddfalse. The initial state can + /// optionally be reset to \a init. + /// + /// Note that the acceptance condition of the automaton (i.e. the + /// set of all acceptance set) is not changed, because so far this + /// function is only needed in graph algorithms that do not call + /// all_acceptance_conditions(). + SPOT_API const tgba* + build_tgba_mask_acc_ignore(const tgba* to_mask, + const bdd to_ignore, + const state* init = 0); + } #endif // SPOT_TGBA_TGBAMASK_HH diff --git a/src/tgbatest/.gitignore b/src/tgbatest/.gitignore index 1b45a65fe..36469b686 100644 --- a/src/tgbatest/.gitignore +++ b/src/tgbatest/.gitignore @@ -19,6 +19,7 @@ ltlmagic ltlprod Makefile Makefile.in +maskacc mixprod output1 output2 diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index ab8edbd56..025752996 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -42,6 +42,7 @@ check_PROGRAMS = \ intvcomp \ intvcmp2 \ ltlprod \ + maskacc \ mixprod \ powerset \ readsat \ @@ -64,6 +65,7 @@ intvcomp_SOURCES = intvcomp.cc intvcmp2_SOURCES = intvcmp2.cc ltl2tgba_SOURCES = ltl2tgba.cc ltlprod_SOURCES = ltlprod.cc +maskacc_SOURCES = maskacc.cc mixprod_SOURCES = mixprod.cc powerset_SOURCES = powerset.cc randtgba_SOURCES = randtgba.cc @@ -89,6 +91,7 @@ TESTS = \ neverclaimread.test \ dstar.test \ readsave.test \ + maskacc.test \ simdet.test \ sim.test \ sim2.test \ diff --git a/src/tgbatest/maskacc.cc b/src/tgbatest/maskacc.cc new file mode 100755 index 000000000..1d392b686 --- /dev/null +++ b/src/tgbatest/maskacc.cc @@ -0,0 +1,69 @@ +// Copyright (C) 2014 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 . + +#include +#include +#include +#include "tgbaparse/public.hh" +#include "tgbaalgos/save.hh" +#include "tgba/tgbamask.hh" +#include "ltlast/allnodes.hh" + +void +syntax(char* prog) +{ + std::cerr << prog << " file" << std::endl; + exit(2); +} + +int +main(int argc, char** argv) +{ + int exit_code = 0; + + if (argc != 2) + syntax(argv[0]); + + spot::bdd_dict* dict = new spot::bdd_dict(); + + spot::ltl::environment& env(spot::ltl::default_environment::instance()); + spot::tgba_parse_error_list pel; + spot::tgba_explicit_string* aut = spot::tgba_parse(argv[1], pel, dict, env); + if (spot::format_tgba_parse_errors(std::cerr, argv[1], pel)) + return 2; + + bdd all = aut->all_acceptance_conditions(); + while (all != bddfalse) + { + bdd one = bdd_satone(all); + all -= one; + + const spot::tgba* masked = spot::build_tgba_mask_acc_ignore(aut, one); + spot::tgba_save_reachable(std::cout, masked); + delete masked; + } + + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); + assert(spot::ltl::atomic_prop::instance_count() != 0); + delete aut; + assert(spot::ltl::atomic_prop::instance_count() == 0); + delete dict; + return exit_code; +} diff --git a/src/tgbatest/maskacc.test b/src/tgbatest/maskacc.test new file mode 100755 index 000000000..0e6bb711e --- /dev/null +++ b/src/tgbatest/maskacc.test @@ -0,0 +1,50 @@ +#!/bin/sh +# Copyright (C) 2014 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 + +cat >input1 <expect1 <