From 62f5b9769bc811c5c652966fd39292aec22110da Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 20 Aug 2015 21:31:07 +0200 Subject: [PATCH] remove algorithms that where only used by dstar's dra2ba conversion Since we just removed that conversion, those can go as well. Yay! * src/tests/kv.test, src/twa/twamask.cc, src/twa/twamask.hh, src/twa/twaproxy.cc, src/twa/twaproxy.hh, src/twaalgos/scc.cc, src/twaalgos/scc.hh: Delete. * src/twaalgos/Makefile.am, src/twa/Makefile.am, src/tests/Makefile.am, src/tests/ikwiad.cc: adjust. --- src/tests/Makefile.am | 1 - src/tests/ikwiad.cc | 26 +-- src/tests/kv.test | 55 ----- src/twa/Makefile.am | 4 - src/twa/twamask.cc | 231 -------------------- src/twa/twamask.hh | 66 ------ src/twa/twaproxy.cc | 75 ------- src/twa/twaproxy.hh | 59 ----- src/twaalgos/Makefile.am | 2 - src/twaalgos/scc.cc | 453 --------------------------------------- src/twaalgos/scc.hh | 210 ------------------ 11 files changed, 1 insertion(+), 1181 deletions(-) delete mode 100755 src/tests/kv.test delete mode 100644 src/twa/twamask.cc delete mode 100644 src/twa/twamask.hh delete mode 100644 src/twa/twaproxy.cc delete mode 100644 src/twa/twaproxy.hh delete mode 100644 src/twaalgos/scc.cc delete mode 100644 src/twaalgos/scc.hh diff --git a/src/tests/Makefile.am b/src/tests/Makefile.am index c89713b08..47958b188 100644 --- a/src/tests/Makefile.am +++ b/src/tests/Makefile.am @@ -199,7 +199,6 @@ TESTS_twa = \ degendet.test \ degenid.test \ degenlskip.test \ - kv.test \ randomize.test \ lbttparse.test \ scc.test \ diff --git a/src/tests/ikwiad.cc b/src/tests/ikwiad.cc index 271b2b88b..9d94fc996 100644 --- a/src/tests/ikwiad.cc +++ b/src/tests/ikwiad.cc @@ -53,7 +53,6 @@ #include "twaalgos/stats.hh" #include "twaalgos/sccinfo.hh" #include "twaalgos/emptiness_stats.hh" -#include "twaalgos/scc.hh" #include "twaalgos/sccinfo.hh" #include "twaalgos/isdet.hh" #include "twaalgos/cycles.hh" @@ -268,8 +267,6 @@ syntax(char* prog) << "subtransitions)" << std::endl << " -K dump the graph of SCCs in dot format" << std::endl - << " -KV verbosely dump the graph of SCCs in dot format" - << std::endl << " -KC list cycles in automaton" << std::endl << " -KW list weak SCCs" << std::endl << " -N output the never clain for Spin (implies -DS)" @@ -556,10 +553,6 @@ checked_main(int argc, char** argv) return 2; tm.stop("reading -KP's argument"); } - else if (!strcmp(argv[formula_index], "-KV")) - { - output = 11; - } else if (!strcmp(argv[formula_index], "-KC")) { output = 15; @@ -1485,24 +1478,7 @@ checked_main(int argc, char** argv) break; } case 10: - { - auto aa = - std::dynamic_pointer_cast(a); - if (!aa) - dump_scc_dot(a, std::cout, false); - else - dump_scc_info_dot(std::cout, aa); - } - break; - case 11: - { - //const spot::twa_graph_ptr g = - // dynamic_cast(a); - //if (!g) - dump_scc_dot(a, std::cout, true); - //else - // dump_scc_info_dot(std::cout, g); - } + dump_scc_info_dot(std::cout, ensure_digraph(a)); break; case 12: stats_reachable(a).dump(std::cout); diff --git a/src/tests/kv.test b/src/tests/kv.test deleted file mode 100755 index c72abc7af..000000000 --- a/src/tests/kv.test +++ /dev/null @@ -1,55 +0,0 @@ -#!/bin/sh -# -*- coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et -# Développement de l'EPITA. -# -# 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 - -check () -{ - run 0 ../ikwiad -f -KV "$1" > out.dot - test -z "$DOT" || "$DOT" out.dot > /dev/null - rm -f out.dot -} - -# We don't check the output, but running these might be -# enough to trigger assertions in the code, or raise valgrind concerns. - -check 'a R (b R c)' -check '(a U b) U (c U d)' -check '((Xp2)U(X(1)))&(p1 R(p2 R p0))' - -# Make sure escaped variables print OK. -check '"G1"U"GG" && "FF"' - - -# Make sure we count 4 atomic propositions in -# G("P_1.p2" <-> (F"P_1.p3" & ("P_0.p3" | (X"P_1.CS" U "P_1.p2")))) U G"P_1.p2" -# even after iterated simulation -# Report from Etienne Renault. - -../ikwiad -KV -R3 -RIS >out \ -'G("P_1.p2" <-> (F"P_1.p3" & ("P_0.p3" | (X"P_1.CS" U "P_1.p2")))) U G"P_1.p2"' -x=`sed -n '/APrec/{ - s/.*APrec=\[\([^]]*\)\].*/\1/p - q -}' out | tr ' ' '\n' | wc -l` -test "$x" -eq 4 diff --git a/src/twa/Makefile.am b/src/twa/Makefile.am index 6ecf7c180..936da7d32 100644 --- a/src/twa/Makefile.am +++ b/src/twa/Makefile.am @@ -34,8 +34,6 @@ twa_HEADERS = \ taatgba.hh \ twa.hh \ twagraph.hh \ - twamask.hh \ - twaproxy.hh \ twaproduct.hh \ twasafracomplement.hh @@ -49,6 +47,4 @@ libtwa_la_SOURCES = \ twa.cc \ twagraph.cc \ twaproduct.cc \ - twamask.cc \ - twaproxy.cc \ twasafracomplement.cc diff --git a/src/twa/twamask.cc b/src/twa/twamask.cc deleted file mode 100644 index 188f61e10..000000000 --- a/src/twa/twamask.cc +++ /dev/null @@ -1,231 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013, 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 "twamask.hh" -#include - -namespace spot -{ - namespace - { - struct transition - { - const state* dest; - bdd cond; - acc_cond::mark_t acc; - }; - typedef std::vector transitions; - - struct succ_iter_filtered: public twa_succ_iterator - { - ~succ_iter_filtered() - { - for (auto& t: trans_) - t.dest->destroy(); - } - - bool first() - { - it_ = trans_.begin(); - return it_ != trans_.end(); - } - - bool next() - { - ++it_; - return it_ != trans_.end(); - } - - bool done() const - { - return it_ == trans_.end(); - } - - state* current_state() const - { - return it_->dest->clone(); - } - - bdd current_condition() const - { - return it_->cond; - } - - acc_cond::mark_t current_acceptance_conditions() const - { - return it_->acc; - } - - transitions trans_; - transitions::const_iterator it_; - }; - - /// \ingroup twa_on_the_fly_algorithms - /// \brief A masked TGBA (abstract). - /// - /// Ignores some states from a TGBA. What state are preserved or - /// ignored is controlled by the wanted() method. - /// - /// This is an abstract class. You should inherit from it and - /// supply a wanted() method to specify which states to keep. - class twa_mask: public twa_proxy - { - protected: - /// \brief Constructor. - /// \param masked The automaton to mask - /// \param init Any state to use as initial state. This state will be - /// destroyed by the destructor. - twa_mask(const const_twa_ptr& masked, const state* init = 0): - twa_proxy(masked), - init_(init) - { - if (!init) - init_ = masked->get_init_state(); - } - - - public: - virtual ~twa_mask() - { - init_->destroy(); - } - - virtual state* get_init_state() const - { - return init_->clone(); - } - - virtual twa_succ_iterator* - succ_iter(const state* local_state) const - { - succ_iter_filtered* res; - if (iter_cache_) - { - res = down_cast(iter_cache_); - res->trans_.clear(); - iter_cache_ = nullptr; - } - else - { - res = new succ_iter_filtered; - } - for (auto it: original_->succ(local_state)) - { - const spot::state* s = it->current_state(); - auto acc = it->current_acceptance_conditions(); - if (!wanted(s, acc)) - { - s->destroy(); - continue; - } - res->trans_.emplace_back - (transition {s, it->current_condition(), acc}); - } - return res; - } - - virtual bool wanted(const state* s, acc_cond::mark_t acc) const = 0; - - protected: - const state* init_; - }; - - class twa_mask_keep: public twa_mask - { - const state_set& mask_; - public: - twa_mask_keep(const const_twa_ptr& masked, - const state_set& mask, - const state* init) - : twa_mask(masked, init), - mask_(mask) - { - } - - bool wanted(const state* s, const acc_cond::mark_t) const - { - state_set::const_iterator i = mask_.find(s); - return i != mask_.end(); - } - }; - - class twa_mask_ignore: public twa_mask - { - const state_set& mask_; - public: - twa_mask_ignore(const const_twa_ptr& masked, - const state_set& mask, - const state* init) - : twa_mask(masked, init), - mask_(mask) - { - } - - bool wanted(const state* s, const acc_cond::mark_t) const - { - state_set::const_iterator i = mask_.find(s); - return i == mask_.end(); - } - }; - - class twa_mask_acc_ignore: public twa_mask - { - unsigned mask_; - public: - twa_mask_acc_ignore(const const_twa_ptr& masked, - unsigned mask, - const state* init) - : twa_mask(masked, init), - mask_(mask) - { - } - - bool wanted(const state*, const acc_cond::mark_t acc) const - { - return !acc.has(mask_); - } - }; - - } - - const_twa_ptr - build_twa_mask_keep(const const_twa_ptr& to_mask, - const state_set& to_keep, - const state* init) - { - return std::make_shared(to_mask, to_keep, init); - } - - const_twa_ptr - build_twa_mask_ignore(const const_twa_ptr& to_mask, - const state_set& to_ignore, - const state* init) - { - return std::make_shared(to_mask, to_ignore, init); - } - - const_twa_ptr - build_twa_mask_acc_ignore(const const_twa_ptr& to_mask, - unsigned to_ignore, - const state* init) - { - return std::make_shared(to_mask, to_ignore, init); - } - -} diff --git a/src/twa/twamask.hh b/src/twa/twamask.hh deleted file mode 100644 index 608fc705b..000000000 --- a/src/twa/twamask.hh +++ /dev/null @@ -1,66 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 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 . - -#pragma once - -#include -#include "twaproxy.hh" - -namespace spot -{ - - /// \ingroup twa_on_the_fly_algorithms - /// \brief Mask a TGBA, keeping a given set of states. - /// - /// Mask the TGBA \a to_mask, keeping only the - /// states from \a to_keep. The initial state - /// can optionally be reset to \a init. - SPOT_API const_twa_ptr - build_twa_mask_keep(const const_twa_ptr& to_mask, - const state_set& to_keep, - const state* init = 0); - - /// \ingroup twa_on_the_fly_algorithms - /// \brief Mask a TGBA, rejecting a given set of states. - /// - /// Mask the TGBA \a to_mask, keeping only the states that are not - /// in \a to_ignore. The initial state can optionally be reset to - /// \a init. - SPOT_API const_twa_ptr - build_twa_mask_ignore(const const_twa_ptr& to_mask, - const state_set& to_ignore, - const state* init = 0); - - - /// \ingroup twa_on_the_fly_algorithms - /// \brief Mask a TGBA, rejecting some acceptance set of transitions. - /// - /// This will ignore all transitions that have the TO_IGNORE - /// acceptance mark. 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_twa_ptr - build_twa_mask_acc_ignore(const const_twa_ptr& to_mask, - unsigned to_ignore, - const state* init = 0); -} diff --git a/src/twa/twaproxy.cc b/src/twa/twaproxy.cc deleted file mode 100644 index 21f2ae4ca..000000000 --- a/src/twa/twaproxy.cc +++ /dev/null @@ -1,75 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 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 . - -#include "twaproxy.hh" - -namespace spot -{ - twa_proxy::twa_proxy(const const_twa_ptr& original) - : twa(original->get_dict()), original_(original) - { - get_dict()->register_all_variables_of(original, this); - acc_.add_sets(original->num_sets()); - } - - twa_proxy::~twa_proxy() - { - get_dict()->unregister_all_my_variables(this); - } - - state* twa_proxy::get_init_state() const - { - return original_->get_init_state(); - } - - twa_succ_iterator* - twa_proxy::succ_iter(const state* state) const - { - if (iter_cache_) - { - original_->release_iter(iter_cache_); - iter_cache_ = nullptr; - } - return original_->succ_iter(state); - } - - std::string - twa_proxy::format_state(const state* state) const - { - return original_->format_state(state); - } - - std::string - twa_proxy::transition_annotation(const twa_succ_iterator* t) const - { - return original_->transition_annotation(t); - } - - state* - twa_proxy::project_state(const state* s, const const_twa_ptr& t) const - { - return original_->project_state(s, t); - } - - bdd - twa_proxy::compute_support_conditions(const state* state) const - { - return original_->support_conditions(state); - } -} diff --git a/src/twa/twaproxy.hh b/src/twa/twaproxy.hh deleted file mode 100644 index c2954bf10..000000000 --- a/src/twa/twaproxy.hh +++ /dev/null @@ -1,59 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 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 . - -#pragma once - -#include "twa.hh" - -namespace spot -{ - /// \ingroup twa_on_the_fly_algorithms - /// \brief A TGBA proxy. - /// - /// This implements a simple proxy to an existing - /// TGBA, forwarding all methods to the original. - /// By itself this class is pointless: better use the - /// original automaton right away. However it is useful - /// to inherit from this class and override some of its - /// methods to implement some on-the-fly algorithm. - class SPOT_API twa_proxy: public twa - { - protected: - twa_proxy(const const_twa_ptr& original); - - public: - virtual ~twa_proxy(); - - virtual state* get_init_state() const; - - virtual twa_succ_iterator* - succ_iter(const state* state) const; - - virtual std::string format_state(const state* state) const; - - virtual std::string - transition_annotation(const twa_succ_iterator* t) const; - - virtual state* project_state(const state* s, const const_twa_ptr& t) const; - - protected: - virtual bdd compute_support_conditions(const state* state) const; - const_twa_ptr original_; - }; -} diff --git a/src/twaalgos/Makefile.am b/src/twaalgos/Makefile.am index fdae1e5c1..e6cc05fef 100644 --- a/src/twaalgos/Makefile.am +++ b/src/twaalgos/Makefile.am @@ -70,7 +70,6 @@ twaalgos_HEADERS = \ safety.hh \ sbacc.hh \ sccfilter.hh \ - scc.hh \ sccinfo.hh \ se05.hh \ sepsets.hh \ @@ -127,7 +126,6 @@ libtwaalgos_la_SOURCES = \ relabel.cc \ safety.cc \ sbacc.cc \ - scc.cc \ sccinfo.cc \ sccfilter.cc \ se05.cc \ diff --git a/src/twaalgos/scc.cc b/src/twaalgos/scc.cc deleted file mode 100644 index 0c72accf2..000000000 --- a/src/twaalgos/scc.cc +++ /dev/null @@ -1,453 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2011, 2012, 2013, 2014, 2015 Laboratoire -// de Recherche et Développement de l'Epita. -// -// 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 -#include "scc.hh" -#include "twa/bddprint.hh" -#include "misc/escape.hh" - -namespace spot -{ - scc_map::scc_map(const const_twa_ptr& aut) - : aut_(aut) - { - } - - scc_map::~scc_map() - { - hash_type::iterator i = h_.begin(); - - while (i != h_.end()) - { - // Advance the iterator before deleting the key. - const state* s = i->first; - ++i; - s->destroy(); - } - } - - unsigned - scc_map::initial() const - { - state* in = aut_->get_init_state(); - int val = scc_of_state(in); - in->destroy(); - return val; - } - - const scc_map::succ_type& - scc_map::succ(unsigned n) const - { - assert(scc_map_.size() > n); - return scc_map_[n].succ; - } - - bool - scc_map::trivial(unsigned n) const - { - assert(scc_map_.size() > n); - return scc_map_[n].trivial; - } - - bool - scc_map::accepting(unsigned n) const - { - if (scc_map_[n].trivial) - return false; - return aut_->acc().accepting(acc_set_of(n)); - } - - const_twa_ptr - scc_map::get_aut() const - { - return aut_; - } - - - int - scc_map::relabel_component() - { - assert(!root_.front().states.empty()); - std::list::iterator i; - int n = scc_map_.size(); - for (i = root_.front().states.begin(); i != root_.front().states.end(); ++i) - { - hash_type::iterator spi = h_.find(*i); - assert(spi != h_.end()); - assert(spi->first == *i); - assert(spi->second < 0); - spi->second = n; - } - scc_map_.push_back(root_.front()); - return n; - } - - // recursively update supp rec - bdd - scc_map::update_supp_rec(unsigned state) - { - assert(scc_map_.size() > state); - - bdd& res = scc_map_[state].supp_rec; - - if (res == bddfalse) - { - const succ_type& s = succ(state); - succ_type::const_iterator it; - - res = scc_map_[state].supp; - - for (it = s.begin(); it != s.end(); ++it) - res &= update_supp_rec(it->first) & bdd_support(it->second); - } - - return res; - } - - void - scc_map::build_map() - { - // Setup depth-first search from the initial state. - { - self_loops_ = 0; - state* init = aut_->get_init_state(); - num_ = -1; - h_.emplace(init, num_); - root_.emplace_front(num_); - arc_acc_.push(0U); - arc_cond_.push(bddfalse); - twa_succ_iterator* iter = aut_->succ_iter(init); - iter->first(); - todo_.emplace(init, iter); - } - - while (!todo_.empty()) - { - assert(root_.size() == arc_acc_.size()); - assert(root_.size() == arc_cond_.size()); - - // We are looking at the next successor in SUCC. - twa_succ_iterator* succ = todo_.top().second; - - // If there is no more successor, backtrack. - if (succ->done()) - { - // We have explored all successors of state CURR. - const state* curr = todo_.top().first; - - // Backtrack TODO_. - todo_.pop(); - - // Fill rem with any component removed, so that - // remove_component() does not have to traverse the SCC - // again. - hash_type::const_iterator spi = h_.find(curr); - assert(spi != h_.end()); - root_.front().states.push_front(spi->first); - - // When backtracking the root of an SCC, we must also - // remove that SCC from the ARC/ROOT stacks. We must - // discard from H all reachable states from this SCC. - assert(!root_.empty()); - if (root_.front().index == spi->second) - { - assert(!arc_acc_.empty()); - assert(arc_cond_.size() == arc_acc_.size()); - bdd cond = arc_cond_.top(); - arc_cond_.pop(); - arc_acc_.pop(); - int num = relabel_component(); - root_.pop_front(); - - // Record the transition between the SCC being popped - // and the previous SCC. - if (!root_.empty()) - root_.front().succ.emplace(num, cond); - } - - aut_->release_iter(succ); - // Do not destroy CURR: it is a key in H. - continue; - } - - // We have a successor to look at. - // Fetch the values we are interested in... - const state* dest = succ->current_state(); - if (!dest->compare(todo_.top().first)) - ++self_loops_; - auto acc = succ->current_acceptance_conditions(); - bdd cond = succ->current_condition(); - root_.front().supp &= bdd_support(cond); - // ... and point the iterator to the next successor, for - // the next iteration. - succ->next(); - // We do not need SUCC from now on. - - // Are we going to a new state? - hash_type::const_iterator spi = h_.find(dest); - if (spi == h_.end()) - { - // Yes. Number it, stack it, and register its successors - // for later processing. - h_.emplace(dest, --num_); - root_.emplace_front(num_); - arc_acc_.push(acc); - arc_cond_.push(cond); - twa_succ_iterator* iter = aut_->succ_iter(dest); - iter->first(); - todo_.emplace(dest, iter); - continue; - } - - // We already know the state. - dest->destroy(); - - // Have we reached a maximal SCC? - if (spi->second >= 0) - { - int dest = spi->second; - // Record that there is a transition from this SCC to the - // dest SCC labelled with cond. - succ_type::iterator i = root_.front().succ.find(dest); - if (i == root_.front().succ.end()) - root_.front().succ.emplace(dest, cond); - else - i->second |= cond; - - continue; - } - - // Now this is the most interesting case. We have reached a - // state S1 which is already part of a non-dead SCC. Any such - // non-dead SCC has necessarily been crossed by our path to - // this state: there is a state S2 in our path which belongs - // to this SCC too. We are going to merge all states between - // this S1 and S2 into this SCC. - // - // This merge is easy to do because the order of the SCC in - // ROOT is descending: we just have to merge all SCCs from the - // top of ROOT that have an index lesser than the one of - // the SCC of S2 (called the "threshold"). - int threshold = spi->second; - std::list states; - succ_type succs; - cond_set conds; - conds.insert(cond); - bdd supp = bddtrue; - std::set used_acc = { acc }; - while (threshold > root_.front().index) - { - assert(!root_.empty()); - assert(!arc_acc_.empty()); - assert(arc_acc_.size() == arc_cond_.size()); - acc |= root_.front().acc; - auto lacc = arc_acc_.top(); - acc |= lacc; - used_acc.insert(lacc); - used_acc.insert(root_.front().useful_acc.begin(), - root_.front().useful_acc.end()); - states.splice(states.end(), root_.front().states); - succs.insert(root_.front().succ.begin(), - root_.front().succ.end()); - conds.insert(arc_cond_.top()); - conds.insert(root_.front().conds.begin(), - root_.front().conds.end()); - supp &= root_.front().supp; - root_.pop_front(); - arc_acc_.pop(); - arc_cond_.pop(); - } - - // Note that we do not always have - // threshold == root_.front().index - // after this loop, the SCC whose index is threshold might have - // been merged with a higher SCC. - - // Accumulate all acceptance conditions, states, SCC - // successors, and conditions into the merged SCC. - root_.front().acc |= acc; - root_.front().states.splice(root_.front().states.end(), states); - root_.front().succ.insert(succs.begin(), succs.end()); - root_.front().conds.insert(conds.begin(), conds.end()); - root_.front().supp &= supp; - // This SCC is no longer trivial. - root_.front().trivial = false; - assert(!used_acc.empty()); - root_.front().useful_acc.insert(used_acc.begin(), used_acc.end()); - } - - // recursively update supp_rec - (void) update_supp_rec(initial()); - } - - unsigned scc_map::scc_of_state(const state* s) const - { - hash_type::const_iterator i = h_.find(s); - assert(i != h_.end()); - return i->second; - } - - const scc_map::cond_set& scc_map::cond_set_of(unsigned n) const - { - assert(scc_map_.size() > n); - return scc_map_[n].conds; - } - - bdd scc_map::ap_set_of(unsigned n) const - { - assert(scc_map_.size() > n); - return scc_map_[n].supp; - } - - - bdd scc_map::aprec_set_of(unsigned n) const - { - assert(scc_map_.size() > n); - return scc_map_[n].supp_rec; - } - - - acc_cond::mark_t scc_map::acc_set_of(unsigned n) const - { - assert(scc_map_.size() > n); - return scc_map_[n].acc; - } - - unsigned scc_map::self_loops() const - { - return self_loops_; - } - - const std::list& scc_map::states_of(unsigned n) const - { - assert(scc_map_.size() > n); - return scc_map_[n].states; - } - - const state* scc_map::one_state_of(unsigned n) const - { - assert(scc_map_.size() > n); - return scc_map_[n].states.front(); - } - - unsigned scc_map::scc_count() const - { - return scc_map_.size(); - } - - const std::set& - scc_map::useful_acc_of(unsigned n) const - { - assert(scc_map_.size() > n); - return scc_map_[n].useful_acc; - } - - std::ostream& - dump_scc_dot(const scc_map& m, std::ostream& out, bool verbose) - { - out << "digraph G {\n i [label=\"\", style=invis, height=0]" << std::endl; - int start = m.initial(); - out << " i -> " << start << std::endl; - - std::vector seen(m.scc_count()); - seen[start] = true; - - std::queue q; - q.push(start); - while (!q.empty()) - { - int state = q.front(); - q.pop(); - - const scc_map::cond_set& cs = m.cond_set_of(state); - - std::ostringstream ostr; - ostr << state; - if (verbose) - { - size_t n = m.states_of(state).size(); - ostr << " (" << n << " state"; - if (n > 1) - ostr << 's'; - ostr << ")\\naccs="; - escape_str(ostr, m.get_aut()->acc().format(m.acc_set_of(state))); - ostr << "\\nconds=["; - for (scc_map::cond_set::const_iterator i = cs.begin(); - i != cs.end(); ++i) - { - if (i != cs.begin()) - ostr << ", "; - escape_str(ostr, - bdd_format_formula(m.get_aut()->get_dict(), *i)); - } - ostr << "]\\n AP=["; - escape_str(ostr, - bdd_format_sat(m.get_aut()->get_dict(), - m.ap_set_of(state))); - ostr << "]\\n APrec=["; - escape_str(ostr, bdd_format_sat(m.get_aut()->get_dict(), - m.aprec_set_of(state))); - ostr << "]\\n useful=["; - for (auto a: m.useful_acc_of(state)) - m.get_aut()->acc().format(a); - ostr << ']'; - } - - out << " " << state << " [shape=box," - << (m.accepting(state) ? "style=bold," : "") - << "label=\"" << ostr.str() << "\"]" << std::endl; - - const scc_map::succ_type& succ = m.succ(state); - - scc_map::succ_type::const_iterator it; - for (it = succ.begin(); it != succ.end(); ++it) - { - int dest = it->first; - bdd label = it->second; - - out << " " << state << " -> " << dest - << " [label=\""; - escape_str(out, bdd_format_formula(m.get_aut()->get_dict(), label)); - out << "\"]" << std::endl; - - if (seen[dest]) - continue; - - seen[dest] = true; - q.push(dest); - } - } - - out << '}' << std::endl; - - return out; - } - - std::ostream& - dump_scc_dot(const const_twa_ptr& a, std::ostream& out, bool verbose) - { - scc_map m(a); - m.build_map(); - return dump_scc_dot(m, out, verbose); - } - -} diff --git a/src/twaalgos/scc.hh b/src/twaalgos/scc.hh deleted file mode 100644 index b09158566..000000000 --- a/src/twaalgos/scc.hh +++ /dev/null @@ -1,210 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 -// Laboratoire de Recherche et Développement de l'Epita. -// -// 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 . - -#pragma once - -#include -#include -#include -#include "twa/twa.hh" -#include -#include "misc/hash.hh" -#include "misc/bddlt.hh" - -namespace spot -{ - - /// Build a map of Strongly Connected components in in a TGBA. - class SPOT_API scc_map - { - public: - typedef std::map succ_type; - typedef std::set cond_set; - - /// \brief Constructor. - /// - /// This will note compute the map initially. You should call - /// build_map() to do so. - scc_map(const const_twa_ptr& aut); - - ~scc_map(); - - /// Actually compute the graph of strongly connected components. - void build_map(); - - /// Get the automaton for which the map has been constructed. - const_twa_ptr get_aut() const; - - /// \brief Get the number of SCC in the automaton. - /// - /// SCCs are labelled from 0 to scc_count()-1. - /// - /// \pre This should only be called once build_map() has run. - unsigned scc_count() const; - - /// \brief Get number of the SCC containing the initial state. - /// - /// \pre This should only be called once build_map() has run. - unsigned initial() const; - - /// \brief Successor SCCs of a SCC. - /// - /// \pre This should only be called once build_map() has run. - const succ_type& succ(unsigned n) const; - - /// \brief Return whether an SCC is trivial. - /// - /// Trivial SCCs have one state and no self-loop. - /// - /// \pre This should only be called once build_map() has run. - bool trivial(unsigned n) const; - - /// \brief Return whether an SCC is accepting. - /// - /// \pre This should only be called once build_map() has run. - bool accepting(unsigned n) const; - - /// \brief Return the set of conditions occurring in an SCC. - /// - /// \pre This should only be called once build_map() has run. - const cond_set& cond_set_of(unsigned n) const; - - /// \brief Return the set of atomic properties occurring on the - /// transitions leaving states from SCC \a n. - /// - /// The transitions considered are all transitions inside SCC - /// \a n, as well as the transitions leaving SCC \a n. - /// - /// \return a BDD that is a conjuction of all atomic properties - /// occurring on the transitions leaving the states of SCC \a n. - /// - /// \pre This should only be called once build_map() has run. - bdd ap_set_of(unsigned n) const; - - /// \brief Return the set of atomic properties reachable from this SCC. - /// - /// \return a BDD that is a conjuction of all atomic properties - /// occurring on the transitions reachable from this SCC n. - /// - /// \pre This should only be called once build_map() has run. - bdd aprec_set_of(unsigned n) const; - - /// \brief Return the set of acceptance conditions occurring in an SCC. - /// - /// \pre This should only be called once build_map() has run. - acc_cond::mark_t acc_set_of(unsigned n) const; - - /// \brief Return the set of useful acceptance conditions of SCC \a n. - /// - /// Useless acceptances conditions are always implied by other acceptances - /// conditions. This returns all the other acceptance conditions. - const std::set& useful_acc_of(unsigned n) const; - - /// \brief Return the set of states of an SCC. - /// - /// The states in the returned list are still owned by the scc_map - /// instance. They should NOT be destroyed by the client code. - /// - /// \pre This should only be called once build_map() has run. - const std::list& states_of(unsigned n) const; - - /// \brief Return one state of an SCC. - /// - /// The state in the returned list is still owned by the scc_map - /// instance. It should NOT be destroyed by the client code. - /// - /// \pre This should only be called once build_map() has run. - const state* one_state_of(unsigned n) const; - - /// \brief Return the number of the SCC a state belongs too. - /// - /// \pre This should only be called once build_map() has run. - unsigned scc_of_state(const state* s) const; - - /// \brief Return the number of self loops in the automaton. - unsigned self_loops() const; - - protected: - bdd update_supp_rec(unsigned state); - int relabel_component(); - - struct scc - { - public: - scc(int index) : index(index), acc(0U), - supp(bddtrue), supp_rec(bddfalse), - trivial(true) {}; - /// Index of the SCC. - int index; - /// The union of all acceptance conditions of transitions which - /// connect the states of the connected component. - acc_cond::mark_t acc; - /// States of the component. - std::list states; - /// Set of conditions used in the SCC. - cond_set conds; - /// Conjunction of atomic propositions used in the SCC. - bdd supp; - /// Conjunction of atomic propositions used in the SCC. - bdd supp_rec; - /// Successor SCC. - succ_type succ; - /// Trivial SCC have one state and no self-loops. - bool trivial; - /// \brief Set of acceptance combinations used in the SCC. - std::set useful_acc; - }; - - const_twa_ptr aut_; // Automata to decompose. - typedef std::list stack_type; - stack_type root_; // Stack of SCC roots. - std::stack arc_acc_; // A stack of acceptance conditions - // between each of these SCC. - std::stack arc_cond_; // A stack of conditions - // between each of these SCC. - typedef std::unordered_map hash_type; - hash_type h_; // Map of visited states. Values >= 0 - // designate maximal SCC. Values < 0 - // number states that are part of - // incomplete SCCs being completed. - int num_; // Number of visited nodes, negated. - typedef std::pair pair_state_iter; - std::stack todo_; // DFS stack. Holds (STATE, - // ITERATOR) pairs where - // ITERATOR is an iterator over - // the successors of STATE. - // ITERATOR should always be - // freed when TODO is popped, - // but STATE should not because - // it is used as a key in H. - - typedef std::vector scc_map_type; - scc_map_type scc_map_; // Map of constructed maximal SCC. - // SCC number "n" in H_ corresponds to entry - // "n" in SCC_MAP_. - unsigned self_loops_; // Self loops count. - }; - - SPOT_API std::ostream& - dump_scc_dot(const const_twa_ptr& a, - std::ostream& out, bool verbose = false); - SPOT_API std::ostream& - dump_scc_dot(const scc_map& m, std::ostream& out, bool verbose = false); -}