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/detail/stategraph_global_algorithm.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_DETAIL_STATEGRAPH_GLOBAL_ALGORITHM_H
      13             : #define MCRL2_PBES_DETAIL_STATEGRAPH_GLOBAL_ALGORITHM_H
      14             : 
      15             : #include "mcrl2/data/substitutions/sequence_sequence_substitution.h"
      16             : #include "mcrl2/pbes/algorithms.h"
      17             : #include "mcrl2/pbes/detail/stategraph_algorithm.h"
      18             : #include "mcrl2/pbes/detail/stategraph_global_graph.h"
      19             : 
      20             : namespace mcrl2 {
      21             : 
      22             : namespace pbes_system {
      23             : 
      24             : namespace detail {
      25             : 
      26             : /// \brief Algorithm class for the global variant of the stategraph algorithm
      27             : class stategraph_global_algorithm: public stategraph_algorithm
      28             : {
      29             :   public:
      30             :     typedef stategraph_algorithm super;
      31             : 
      32             :   protected:
      33             :     // the control flow graph
      34             :     global_control_flow_graph m_control_flow_graph;
      35             : 
      36             :     // eq_X is the equation corresponding to u = (X, e)
      37             :     // eq_Y is the equation corresponding to Yf
      38           0 :     bool enabled_edge(const global_control_flow_graph_vertex& u, const stategraph_equation& eq_X, const predicate_variable& Yf)
      39             :     {
      40           0 :       auto const& e = u.values();
      41           0 :       auto const& cfp_X = eq_X.control_flow_parameter_indices();
      42           0 :       for (std::size_t k = 0; k < cfp_X.size(); k++)
      43             :       {
      44           0 :         auto q = Yf.source(cfp_X[k]);
      45           0 :         if (q != data::undefined_data_expression() && q != nth_element(e, k))
      46             :         {
      47           0 :           return false;
      48             :         }
      49           0 :       }
      50           0 :       return true;
      51             :     }
      52             : 
      53             :     // Returns k such that cfp[k] == l. Throws an exception if no such k exists.
      54           0 :     std::size_t unproject(const predicate_variable& Yf, const std::vector<std::size_t>& cfp, std::size_t l) const
      55             :     {
      56           0 :       mCRL2log(log::trace) << "stategraph_global_algorithm::unproject: cfp = " << core::detail::print_list(cfp) << " l = " << l << std::endl;
      57           0 :       for (std::size_t k = 0; k < cfp.size(); k++)
      58             :       {
      59           0 :         if (Yf.copy(cfp[k]) == l)
      60             :         {
      61           0 :           return k;
      62             :         }
      63             :       }
      64           0 :       throw mcrl2::runtime_error("no index found in stategraph_global_algorithm::unproject");
      65             :     }
      66             : 
      67           0 :     const global_control_flow_graph_vertex& compute_vertex(global_control_flow_graph& G, const global_control_flow_graph_vertex& u, const stategraph_equation& eq_X, const predicate_variable& Yf, const stategraph_equation& eq_Y)
      68             :     {
      69           0 :       data::data_expression_vector f;
      70           0 :       auto const& X = u.name();
      71           0 :       auto const& e = u.values();
      72           0 :       auto const& cfp_X = eq_X.control_flow_parameter_indices();
      73           0 :       auto const& cfp_Y = eq_Y.control_flow_parameter_indices();
      74             : 
      75           0 :       mCRL2log(log::trace) << "compute_vertex u = (X, e) = (" << X << ", " << core::detail::print_list(e) << "), Y(f) = " << Yf << std::endl;
      76           0 :       mCRL2log(log::trace) << "cfp_X = " << core::detail::print_list(cfp_X) << std::endl;
      77           0 :       mCRL2log(log::trace) << "cfp_Y = " << core::detail::print_list(cfp_Y) << std::endl;
      78             : 
      79           0 :       for (std::size_t l = 0; l < cfp_Y.size(); l++)
      80             :       {
      81           0 :         auto q = Yf.target(cfp_Y[l]);
      82           0 :         if (q != data::undefined_data_expression())
      83             :         {
      84           0 :           mCRL2log(log::trace) << "q = " << q << std::endl;
      85           0 :           f.push_back(q);
      86             :         }
      87             :         else
      88             :         {
      89           0 :           mCRL2log(log::trace) << "q = undefined" << std::endl;
      90             :           // Compute k such that (X, k) and (Y, l) are related. This implies copy(X, i, cfp_X[k]) == cfp_Y[l].
      91             :           //                                                                 Yf.copy[cfp_X[k]] = cfp_Y[l]
      92           0 :           auto p = cfp_Y[l];
      93           0 :           mCRL2log(log::trace) << "Yf = " << Yf << "\n" << Yf.print() << " l = " << l << " Yf.copy(" << l << ") = " << p << std::endl;
      94           0 :           assert(p != data::undefined_index());
      95           0 :           std::size_t k = unproject(Yf, cfp_X, p);
      96           0 :           assert(k < e.size());
      97           0 :           f.push_back(nth_element(e, k));
      98             :         }
      99           0 :       }
     100           0 :       return G.insert_vertex(global_control_flow_graph_vertex(Yf.variable().name(), data::data_expression_list(f.begin(), f.end())));
     101           0 :     }
     102             : 
     103           0 :     void compute_significant_variables()
     104             :     {
     105           0 :       pbes_system::simplify_data_rewriter<data::rewriter> pbesr(m_datar);
     106           0 :       for (const auto& u : m_control_flow_graph)
     107             :       {
     108           0 :         auto const& X = u.name();
     109           0 :         auto const& eq_X = *find_equation(m_pbes, X);
     110           0 :         auto const& d = eq_X.control_flow_parameters();
     111           0 :         auto const& e = u.values();
     112           0 :         assert(d.size() == e.size());
     113           0 :         data::sequence_sequence_substitution<data::variable_vector, data::data_expression_list> sigma(d, e);
     114           0 :         u.set_significant_variables(pbes_system::algorithms::significant_variables(pbesr(eq_X.formula(), sigma)));
     115             :       }
     116           0 :     }
     117             : 
     118           0 :     void compute_global_control_flow_graph()
     119             :     {
     120             :       using utilities::detail::contains;
     121             :       using utilities::detail::pick_element;
     122             : 
     123           0 :       mCRL2log(log::debug) << "=== compute control flow graph ===" << std::endl;
     124           0 :       std::set<const global_control_flow_graph_vertex*> todo;
     125           0 :       std::set<const global_control_flow_graph_vertex*> done;
     126             : 
     127             :       // initialize todo
     128           0 :       auto const& Xinit = m_pbes.initial_state();
     129           0 :       auto const& eq_Xinit = *find_equation(m_pbes, Xinit.name());
     130           0 :       auto einit = eq_Xinit.project(Xinit.parameters());
     131           0 :       auto const& w = m_control_flow_graph.insert_vertex(global_control_flow_graph_vertex(Xinit.name(), einit));
     132           0 :       todo.insert(&w);
     133             : 
     134           0 :       while (!todo.empty())
     135             :       {
     136             :         // u = (X, e)
     137           0 :         auto const& u = *pick_element(todo);
     138           0 :         auto const& X = u.name();
     139           0 :         auto const& eq_X = *find_equation(m_pbes, X);
     140           0 :         auto const& predvars = eq_X.predicate_variables();
     141             : 
     142           0 :         mCRL2log(log::trace) << "choose todo element " << u << std::endl;
     143             : 
     144           0 :         for (std::size_t i = 0; i < predvars.size(); i++)
     145             :         {
     146           0 :           auto const& Yf = predvars[i];
     147           0 :           auto const& Y = Yf.variable().name();
     148           0 :           auto const& eq_Y = *find_equation(m_pbes, Y);
     149           0 :           if (enabled_edge(u, eq_X, Yf))
     150             :           {
     151           0 :             const global_control_flow_graph_vertex& v = compute_vertex(m_control_flow_graph, u, eq_X, Yf, eq_Y);
     152           0 :             m_control_flow_graph.insert_edge(u, i, v);
     153           0 :             if (!contains(done, &v))
     154             :             {
     155           0 :               mCRL2log(log::trace) << "insert todo element " << v << std::endl;
     156           0 :               todo.insert(&v);
     157           0 :               done.insert(&v);
     158             :             }
     159             :           }
     160             :         }
     161             :       }
     162           0 :       m_control_flow_graph.compute_index();
     163           0 :       compute_significant_variables();
     164           0 :       mCRL2log(log::debug) << "--- global control flow graph ---\n" << m_control_flow_graph << std::endl;
     165           0 :     }
     166             : 
     167             :   public:
     168           0 :     stategraph_global_algorithm(const pbes& p, const pbesstategraph_options& options)
     169           0 :       : stategraph_algorithm(p, options)
     170           0 :     { }
     171             : 
     172             :     /// \brief Computes the control flow graph
     173           0 :     void run() override
     174             :     {
     175           0 :       super::run();
     176           0 :       start_timer("compute_global_control_flow_graph");
     177           0 :       compute_global_control_flow_graph();
     178           0 :       finish_timer("compute_global_control_flow_graph");
     179           0 :     }
     180             : 
     181             :     const global_control_flow_graph& global_graph() const
     182             :     {
     183             :       return m_control_flow_graph;
     184             :     }
     185             : };
     186             : 
     187             : } // namespace detail
     188             : 
     189             : } // namespace pbes_system
     190             : 
     191             : } // namespace mcrl2
     192             : 
     193             : #endif // MCRL2_PBES_DETAIL_STATEGRAPH_GLOBAL_ALGORITHM_H