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 pbes.cpp 10 : /// \brief 11 : 12 : #include "mcrl2/pbes/normalize.h" 13 : #include "mcrl2/pbes/pbesinst_finite_algorithm.h" 14 : #include "mcrl2/pbes/remove_equations.h" 15 : #include "mcrl2/pbes/remove_parameters.h" 16 : #include "mcrl2/pbes/significant_variables.h" 17 : 18 : namespace mcrl2 19 : { 20 : 21 : namespace pbes_system 22 : { 23 : 24 : namespace algorithms { 25 : 26 0 : void remove_parameters(pbes& x, const std::set<data::variable>& to_be_removed) 27 : { 28 0 : pbes_system::remove_parameters(x, to_be_removed); 29 0 : } 30 : 31 22 : void remove_parameters(pbes& x, const std::map<core::identifier_string, std::vector<std::size_t> >& to_be_removed) 32 : { 33 22 : pbes_system::remove_parameters(x, to_be_removed); 34 22 : } 35 : 36 418 : void normalize(pbes& x) 37 : { 38 : try 39 : { 40 418 : pbes_system::normalize(x); 41 : } 42 0 : catch (const mcrl2::runtime_error&) 43 : { 44 0 : throw mcrl2::runtime_error("The PBES is not monotonic!"); 45 0 : } 46 418 : } 47 : 48 137 : bool is_normalized(const pbes& x) 49 : { 50 137 : return pbes_system::is_normalized(x); 51 : } 52 : 53 0 : void pbesinst_finite(pbes& p, data::rewrite_strategy rewrite_strategy, const std::string& finite_parameter_selection) 54 : { 55 0 : pbes_system::pbesinst_finite(p, rewrite_strategy, finite_parameter_selection); 56 0 : } 57 : 58 0 : std::string print_removed_equations(const std::vector<propositional_variable>& removed) 59 : { 60 0 : return pbes_system::detail::print_removed_equations(removed); 61 : } 62 : 63 0 : std::vector<propositional_variable> remove_unreachable_variables(pbes& p) 64 : { 65 0 : return pbes_system::remove_unreachable_variables(p); 66 : } 67 : 68 6 : std::set<data::variable> significant_variables(const pbes_expression& x) 69 : { 70 6 : return pbes_system::significant_variables(x); 71 : } 72 : 73 : } // namespace algorithms 74 : 75 : } // namespace pbes_system 76 : 77 : } // namespace mcrl2 78 :