From 8080813303fff30bfb3b95822f55d208f338eaeb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 14 May 2015 17:24:28 +0200 Subject: [PATCH] =?UTF-8?q?simulation:=20work=20on=20T=CF=89A?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * src/twaalgos/simulation.cc, src/twaalgos/simulation.hh: Adjust to work on TωA. This only require separate acceptance sets. * src/tests/sim3.test: New test. * src/tests/Makefile.am: Add it. --- src/tests/Makefile.am | 1 + src/tests/sim3.test | 49 ++++++++++++++++++++++++++++++++++++++ src/twaalgos/simulation.cc | 26 +++++++++++--------- src/twaalgos/simulation.hh | 4 ++-- 4 files changed, 67 insertions(+), 13 deletions(-) create mode 100755 src/tests/sim3.test diff --git a/src/tests/Makefile.am b/src/tests/Makefile.am index 543fe6548..b87aaa435 100644 --- a/src/tests/Makefile.am +++ b/src/tests/Makefile.am @@ -183,6 +183,7 @@ TESTS_twa = \ maskkeep.test \ simdet.test \ sim2.test \ + sim3.test \ ltl2tgba.test \ ltl2neverclaim.test \ ltl2neverclaim-lbtt.test \ diff --git a/src/tests/sim3.test b/src/tests/sim3.test new file mode 100755 index 000000000..fd6bf3397 --- /dev/null +++ b/src/tests/sim3.test @@ -0,0 +1,49 @@ +#! /bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2015 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 >input < map_bdd_bdd; int acc_vars; + acc_cond::mark_t all_inf_; public: bdd mark_to_bdd(acc_cond::mark_t m) @@ -188,9 +190,9 @@ namespace spot all_class_var_(bddtrue), original_(in) { - if (in->acc().uses_fin_acceptance()) + if (!has_separate_sets(in)) throw std::runtime_error - ("direct_simulation() does not yet support Fin acceptance"); + ("direct_simulation() requires separate Inf and Fin sets"); // Call get_init_state_number() before anything else as it // might add a state. @@ -201,6 +203,9 @@ namespace spot assert(ns > 0); size_a_ = ns; + auto all_inf = in->get_acceptance().used_inf_fin_sets().first; + all_inf_ = all_inf; + // Replace all the acceptance conditions by their complements. // (In the case of Cosimulation, we also flip the transitions.) if (Cosimulation) @@ -209,7 +214,6 @@ namespace spot a_->copy_ap_of(in); a_->copy_acceptance_of(in); a_->new_states(ns); - auto& acccond = in->acc(); for (unsigned s = 0; s < ns; ++s) { @@ -227,13 +231,13 @@ namespace spot acc = 0U; for (auto& td: in->out(t.dst)) { - acc = acccond.comp(td.acc); + acc = td.acc ^ all_inf; break; } } else { - acc = acccond.comp(t.acc); + acc = t.acc ^ all_inf; } a_->new_transition(t.dst, s, t.cond, acc); } @@ -243,9 +247,8 @@ namespace spot else { a_ = make_twa_graph(in, twa::prop_set::all()); - auto& acccond = a_->acc(); for (auto& t: a_->transitions()) - t.acc = acccond.comp(t.acc); + t.acc ^= all_inf; } assert(a_->num_states() == size_a_); @@ -515,6 +518,7 @@ namespace spot unsigned nb_satoneset = 0; unsigned nb_minato = 0; + auto all_inf = all_inf_; // For each class, we will create // all the transitions between the states. for (auto& p: bdd_lstate_) @@ -580,10 +584,10 @@ namespace spot bdd cond = bdd_existcomp(cond_acc_dest, sup_all_atomic_prop); - // Because we have complemented all the acceptance - // conditions on the input automaton, we must - // revert them to create a new transition. - acc = res->acc().comp(acc); + // Because we have complemented all the Inf + // acceptance conditions on the input automaton, + // we must revert them to create a new transition. + acc ^= all_inf; if (Cosimulation) { diff --git a/src/twaalgos/simulation.hh b/src/twaalgos/simulation.hh index 6480e302f..1f23b2bca 100644 --- a/src/twaalgos/simulation.hh +++ b/src/twaalgos/simulation.hh @@ -33,7 +33,7 @@ namespace spot /// When the suffixes (letter and acceptance conditions) reachable /// from one state are included in the suffixes seen by another one, /// the former state can be merged into the latter. The algorithm is - /// based on the following paper, but generalized to handle TGBA + /// based on the following paper, but generalized to handle TωA /// directly. /// /** \verbatim @@ -81,7 +81,7 @@ namespace spot /// state can be merged into the latter. /// /// Reverse simulation is discussed in the following paper, - /// but generalized to handle TGBA directly. + /// but generalized to handle TωA directly. /** \verbatim @InProceedings{ somenzi.00.cav, author = {Fabio Somenzi and Roderick Bloem},