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