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 <