Line data Source code
1 : // Author(s): Wieger Wesselink 2 : // Copyright: see the accompanying file COPYING or copy at 3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING 4 : // 5 : // Distributed under the Boost Software License, Version 1.0. 6 : // (See accompanying file LICENSE_1_0.txt or copy at 7 : // http://www.boost.org/LICENSE_1_0.txt) 8 : // 9 : /// \file mcrl2/pbes/remove_equations.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_PBES_REMOVE_EQUATIONS_H 13 : #define MCRL2_PBES_REMOVE_EQUATIONS_H 14 : 15 : #include "mcrl2/pbes/pbes.h" 16 : 17 : namespace mcrl2 { 18 : 19 : namespace pbes_system { 20 : 21 : namespace detail { 22 : 23 : inline 24 0 : std::string print_removed_equations(const std::vector<propositional_variable>& removed) 25 : { 26 0 : std::ostringstream out; 27 0 : out << "\nremoved the following equations:" << std::endl; 28 0 : for (const propositional_variable& v: removed) 29 : { 30 0 : out << " " << pbes_system::pp(v) << std::endl; 31 : } 32 0 : return out.str(); 33 0 : } 34 : 35 : } // namespace detail 36 : 37 : inline 38 20 : std::set<propositional_variable> reachable_variables(const pbes& p) 39 : { 40 : typedef std::vector<pbes_equation>::const_iterator iterator; 41 : 42 : // create a mapping from variable names to iterators 43 20 : std::map<core::identifier_string, iterator> index; 44 59 : for (auto i = p.equations().begin(); i != p.equations().end(); ++i) 45 : { 46 : // index[i->variable().name()] = i; <-- This leads to a attempt to copy- 47 : // construct an iterator from a singular iterator when the toolset 48 : // is compiled in maintainer mode. 49 39 : index.insert(std::pair<core::identifier_string, iterator>(i->variable().name(),i)); 50 : } 51 : 52 20 : std::set<core::identifier_string> visited; 53 20 : std::set<core::identifier_string> explored; 54 20 : visited.insert(p.initial_state().name()); 55 55 : while (!visited.empty()) 56 : { 57 35 : core::identifier_string X = *visited.begin(); 58 35 : visited.erase(visited.begin()); 59 35 : explored.insert(X); 60 35 : pbes_expression phi = index[X]->formula(); 61 35 : std::set<propositional_variable_instantiation> iocc = pbes_system::find_propositional_variable_instantiations(phi); 62 80 : for (const propositional_variable_instantiation& i: iocc) 63 : { 64 45 : if (explored.find(i.name()) == explored.end()) 65 : { 66 17 : visited.insert(i.name()); 67 : } 68 : } 69 35 : } 70 : 71 20 : std::set<propositional_variable> result; 72 55 : for (const core::identifier_string& i: explored) 73 : { 74 35 : result.insert(index[i]->variable()); 75 : } 76 40 : return result; 77 20 : } 78 : 79 : /// \brief Removes equations that are not (syntactically) reachable from the initial state of a PBES. 80 : /// \return The removed variables 81 : inline 82 20 : std::vector<propositional_variable> remove_unreachable_variables(pbes& p) 83 : { 84 20 : std::vector<propositional_variable> result; 85 : 86 20 : std::set<propositional_variable> V = reachable_variables(p); 87 20 : std::vector<pbes_equation> equations; 88 59 : for (pbes_equation& eqn: p.equations()) 89 : { 90 39 : if (V.find(eqn.variable()) != V.end()) 91 : { 92 35 : equations.push_back(eqn); 93 : } 94 : else 95 : { 96 4 : result.push_back(eqn.variable()); 97 : } 98 : } 99 20 : p.equations() = equations; 100 40 : return result; 101 20 : } 102 : 103 : } // namespace pbes_system 104 : 105 : } // namespace mcrl2 106 : 107 : #endif // MCRL2_PBES_REMOVE_EQUATIONS_H