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/pbesinst_symbolic.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_PBES_PBESINST_SYMBOLIC_H 13 : #define MCRL2_PBES_PBESINST_SYMBOLIC_H 14 : 15 : #include "mcrl2/pbes/algorithms.h" 16 : 17 : #include "mcrl2/pbes/pbesinst_algorithm.h" 18 : 19 : namespace mcrl2 { 20 : 21 : namespace pbes_system { 22 : 23 : /// \brief Algorithm class for the symbolic_exploration instantiation algorithm. 24 : class pbesinst_symbolic_algorithm 25 : { 26 : public: 27 : typedef propositional_variable_instantiation state_type; 28 : 29 : protected: 30 : /// \brief The PBES that is being instantiated. 31 : pbes& m_pbes; 32 : 33 : /// \brief Data rewriter. 34 : data::rewriter datar; 35 : 36 : /// \brief The rewriter. 37 : enumerate_quantifiers_rewriter R; 38 : 39 : /// \brief Propositional variable instantiations that need to be handled. 40 : std::set<state_type> todo; 41 : 42 : /// \brief Propositional variable instantiations that have been handled. 43 : std::set<state_type> done; 44 : 45 : /// \brief Data structure for storing the result. E[i] corresponds to the equations 46 : /// generated from the i-th PBES equation. 47 : std::multimap<state_type, state_type> edges; 48 : 49 : /// \brief The initial value. 50 : state_type init; 51 : 52 : /// \brief A lookup map for PBES equations. 53 : std::map<core::identifier_string, std::size_t> m_equation_index; 54 : 55 : public: 56 4 : pbesinst_symbolic_algorithm(pbes& p, data::rewriter::strategy rewrite_strategy = data::jitty) 57 4 : : m_pbes(p), 58 4 : datar(p.data(), rewrite_strategy), 59 4 : R(datar, p.data()) 60 : { 61 4 : pbes_system::algorithms::instantiate_global_variables(p); 62 : 63 : // initialize m_equation_index 64 4 : std::size_t eqn_index = 0; 65 8 : for (const pbes_equation& eqn: p.equations()) 66 : { 67 4 : m_equation_index[eqn.variable().name()] = eqn_index++; 68 : } 69 4 : } 70 : 71 : /// \brief Runs the algorithm. The result is obtained by calling the function \p get_result. 72 4 : void run() 73 : { 74 4 : init = atermpp::down_cast<propositional_variable_instantiation>(R(m_pbes.initial_state())); 75 4 : todo.insert(init); 76 4 : mCRL2log(log::debug) << "discovered vertex " << init << std::endl; 77 : 78 12 : while (!todo.empty()) 79 : { 80 8 : state_type X = *todo.begin(); 81 8 : mCRL2log(log::debug) << "handling vertex " << X << std::endl; 82 8 : todo.erase(todo.begin()); 83 8 : done.insert(X); 84 8 : std::size_t index = m_equation_index[X.name()]; 85 8 : const pbes_equation& eqn = m_pbes.equations()[index]; 86 8 : const pbes_expression& phi = eqn.formula(); 87 8 : data::rewriter::substitution_type sigma; 88 8 : make_pbesinst_substitution(eqn.variable().parameters(), X.parameters(), sigma); 89 8 : pbes_expression psi = R(phi, sigma); 90 8 : R.clear_identifier_generator(); 91 16 : for (const propositional_variable_instantiation& v: find_propositional_variable_instantiations(psi)) 92 : { 93 8 : if (done.find(v) == done.end()) 94 : { 95 4 : todo.insert(v); 96 4 : mCRL2log(log::debug) << "discovered vertex " << v << std::endl; 97 : } 98 8 : } 99 8 : } 100 4 : } 101 : }; 102 : 103 : } // namespace pbes_system 104 : 105 : } // namespace mcrl2 106 : 107 : #endif // MCRL2_PBES_PBESINST_SYMBOLIC_H