stategraph_global_reset_variables.h

Go to the documentation of this file.

// Author(s): Wieger Wesselink
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
/// \file mcrl2/pbes/detail/stategraph_global_reset_variables.h
/// \brief add your file description here.
 
#ifndef MCRL2_PBES_DETAIL_STATEGRAPH_GLOBAL_RESET_VARIABLES_H
#define MCRL2_PBES_DETAIL_STATEGRAPH_GLOBAL_RESET_VARIABLES_H
 
#include "mcrl2/pbes/detail/stategraph_global_algorithm.h"
#include "mcrl2/pbes/detail/stategraph_reset_variables.h"
 
namespace mcrl2::pbes_system::detail {
 
class global_reset_variables_algorithm;
pbes_expression reset_variables(global_reset_variables_algorithm& algorithm, const pbes_expression& x, const stategraph_equation& eq_X);
 
/// \brief Adds the reset variables procedure to the stategraph algorithm
class global_reset_variables_algorithm: public stategraph_global_algorithm
{
  public:
    using super = stategraph_global_algorithm;
 
  protected:
    const pbes& m_original_pbes;
    pbes m_transformed_pbes; // will contain the result of the computation
 
    // if true, the resulting PBES is simplified
    bool m_simplify;
 
    data::data_expression default_value(const data::sort_expression& x)
    {
      // TODO: make this an attribute
      data::representative_generator f(m_pbes.data());
      return f(x);
    }
 
    // returns the parameters of the propositional variable with name X
    std::set<data::variable> propvar_parameters(const core::identifier_string& X) const
    {
      auto const& eq_X = *find_equation(m_pbes, X);
      auto const& d_X = eq_X.parameters();
      return std::set<data::variable>(d_X.begin(), d_X.end());
    }
 
    template <typename Graph>
    void compute_global_control_flow_marking(Graph& G)
    {
      using utilities::detail::pick_element;
 
      mCRL2log(log::log_level_t::debug) << "--- compute initial marking ---" << std::endl;
 
      // initialization
      for (auto i = G.begin(); i != G.end(); ++i)
      {
        auto const& v = *i;
        std::set<data::variable> dx = propvar_parameters(v.name());
        v.set_marking(utilities::detail::set_intersection(v.sig(), dx));
        mCRL2log(log::log_level_t::debug) << "vertex " << v << " sig = " << core::detail::print_set(v.sig()) << " dx = " << core::detail::print_set(dx) << "\n";
      }
      mCRL2log(log::log_level_t::debug) << "--- initial control flow marking ---\n" << G.print_marking();
 
      // backwards reachability algorithm
      std::set<const typename Graph::vertex_type*> todo;
      for (auto i = G.begin(); i != G.end(); ++i)
      {
        auto const& v = *i;
        todo.insert(&v);
      }
      mCRL2log(log::log_level_t::debug) << "--- update marking ---" << std::endl;
      while (!todo.empty())
      {
        auto const& v = *pick_element(todo);
        mCRL2log(log::log_level_t::debug) << "selected marking todo element " << v << std::endl;
        std::set<std::size_t> I = v.marking_variable_indices(m_pbes);
 
        auto const& incoming_edges = v.incoming_edges();
        for (auto ei = incoming_edges.begin(); ei != incoming_edges.end(); ++ei)
        {
          auto const& u = *ei->first;
          const std::set<std::size_t>& labels = ei->second;
          for (std::size_t i: labels)
          {
            std::size_t last_size = u.marking().size();
            const stategraph_equation& eq_X = *find_equation(m_pbes, u.name());
            const propositional_variable_instantiation& Y = eq_X.predicate_variables()[i].variable();
            std::set<data::variable> dx = propvar_parameters(u.name());
            mCRL2log(log::log_level_t::debug) << "  vertex u = " << v << " label = " << i << " I = " << print_set(I) << " u.marking = " << core::detail::print_set(u.marking()) << std::endl;
            for (std::size_t m: I)
            {
              const data::data_expression_list& e = Y.parameters();
              const data::data_expression& e_m = nth_element(e, m);
              std::set<data::variable> fv = data::find_free_variables(e_m);
              u.set_marking(utilities::detail::set_union(utilities::detail::set_intersection(fv, dx), u.marking()));
              mCRL2log(log::log_level_t::debug) << "  m = " << m << " freevars = " << core::detail::print_set(fv) << " dx = " << core::detail::print_set(dx) << "\n";
            }
            if (u.marking().size() > last_size)
            {
              todo.insert(&u);
              mCRL2log(log::log_level_t::debug) << "updated marking " << u.print_marking() << " using edge " << pbes_system::pp(Y) << "\n";
            }
          }
        }
      }
 
      // set the marking_parameters attributes
      for (auto i = G.begin(); i != G.end(); ++i)
      {
        auto const& v = *i;
        const stategraph_equation& eqn = *find_equation(m_pbes, v.name());
        for (const data::variable& w: eqn.parameters())
        {
          v.add_marked_parameter(v.marking().find(w) != v.marking().end());
        }
      }
    }
 
    // First determine whether this location should be considered
    template <typename Vertex>
    bool location_possibly_reachable(const core::identifier_string& Y, const Vertex& u, const std::vector<data::data_expression>& e_X, const stategraph_equation& eq_X,std::size_t i)
    {
      std::size_t N = e_X.size();
      data::data_expression_list::const_iterator k = u.values().begin();
      for (std::size_t j = 0; j < N; ++j)
      {
        if (is_global_control_flow_parameter(Y, j))
        {
          const predicate_variable& X_i = eq_X.predicate_variables()[i];
          auto target_j = X_i.target().find(j);
          if (target_j != X_i.target().end())
          {
            data::data_expression f_k = *k;
            if(f_k != target_j->second)
            {
              return false;
            }
          }
          ++k;
        }
      }
      return true;
    }
 
  public:
    // expands a propositional variable instantiation using the control flow graph
    // x = Y(e)
    // Y(e) = PVI(phi_X, i)
    pbes_expression reset_variable(const propositional_variable_instantiation& x, const stategraph_equation& eq_X, std::size_t i)
    {
      mCRL2log(log::log_level_t::debug) << "--- resetting variable Y(e) = " << pbes_system::pp(x) << " with index " << i << std::endl;
      assert(eq_X.predicate_variables()[i].variable() == x);
 
      std::vector<pbes_expression> phi;
      const core::identifier_string& Y = x.name();
      std::vector<data::data_expression> e(x.parameters().begin(),x.parameters().end());
 
      // iterate over the alternatives as defined by the control flow graph
      auto inst = m_control_flow_graph.index(Y);
      if (inst.empty())
      {
        mCRL2log(log::log_level_t::verbose) << "Equation " << Y << " is not reachable!" << std::endl;
      }
      for (auto q: inst)
      {
        auto& u = *q;
        mCRL2log(log::log_level_t::debug) << "  vertex u = " << u << std::endl;
 
        if(!location_possibly_reachable(Y, u, e, eq_X, i))
        {
          continue;
        }
 
        // Now build the actual formula
        std::vector<data::data_expression> r;
        std::size_t N = u.marked_parameters().size();
        assert(e.size() == u.marked_parameters().size());
        auto k = u.values().begin();
        data::data_expression condition = data::true_();
        for (std::size_t j = 0; j < N; ++j)
        {
          mCRL2log(log::log_level_t::debug) << "    j = " << j;
          if (is_global_control_flow_parameter(Y, j))
          {
            mCRL2log(log::log_level_t::debug) << " CFP(Y, j) = true";
            const data::data_expression& f_k = *k++;
            const predicate_variable& X_i = eq_X.predicate_variables()[i];
            if (X_i.target().find(j) == X_i.target().end() || !m_simplify)
            {
              condition = data::lazy::and_(condition, data::equal_to(e[j], f_k));
              r.push_back(e[j]);
              mCRL2log(log::log_level_t::debug) << " target(X, i, j) = false";
              mCRL2log(log::log_level_t::debug) << " c := c && " << data::pp(data::equal_to(e[j], f_k));
            }
            else
            {
              r.push_back(X_i.target().find(j)->second);
            }
            mCRL2log(log::log_level_t::debug) << " r := r <| " << data::pp(r.back());
 
          }
          else if (u.is_marked_parameter(j))
          {
            mCRL2log(log::log_level_t::debug) << " e[j] is in marking(u)";
            mCRL2log(log::log_level_t::debug) << " r := r <| " << data::pp(e[j]);
            r.push_back(e[j]);
          }
          else
          {
            mCRL2log(log::log_level_t::debug) << " default parameter ";
            mCRL2log(log::log_level_t::debug) << " r := r <| " << data::pp(default_value(e[j].sort()));
            r.push_back(default_value(e[j].sort()));
          }
          mCRL2log(log::log_level_t::debug) << std::endl;
        }
        propositional_variable_instantiation Yr(Y, data::data_expression_list(r.begin(),r.end()));
        if (m_simplify)
        {
          condition = m_datar(condition);
          if (condition != data::false_())
          {
            phi.push_back(imp(atermpp::down_cast<pbes_expression>(condition), Yr));
          }
        }
        else
        {
          phi.push_back(imp(atermpp::down_cast<pbes_expression>(condition), Yr));
        }
      }
      return join_and(phi.begin(), phi.end());
    }
 
    // Applies resetting of variables to the original PBES p.
    void reset_variables_to_original(pbes& p)
    {
      mCRL2log(log::log_level_t::debug) << "--- resetting variables to the original PBES ---" << std::endl;
 
      // apply the reset variable procedure to all propositional variable instantiations
      std::vector<pbes_equation>& p_eqn = p.equations();
      const std::vector<stategraph_equation>& s_eqn = m_pbes.equations();
 
      for (std::size_t k = 0; k < p_eqn.size(); k++)
      {
 
        p_eqn[k].formula() = reset_variables(*this, p_eqn[k].formula(), s_eqn[k]);
      }
 
      // TODO: merge the two rewriters?
      if (m_simplify)
      {
        pbes_system::simplify_data_rewriter<data::rewriter> pbesr(m_datar);
        pbes_system::pbes_rewrite(p, pbesr);
      }
    }
 
    global_reset_variables_algorithm(const pbes& p, const pbesstategraph_options& options)
      : stategraph_global_algorithm(p, options),
        m_original_pbes(p),
        m_simplify(options.simplify)
    {}
 
    void execute_core() override
    {
      start_timer("compute_global_control_flow_marking");
      compute_global_control_flow_marking(m_control_flow_graph);
      finish_timer("compute_global_control_flow_marking");
      mCRL2log(log::log_level_t::verbose) << "Computed control flow marking" << std::endl;
      mCRL2log(log::log_level_t::debug) <<  "--- control flow marking ---\n" << m_control_flow_graph.print_marking();
      m_transformed_pbes = m_original_pbes;
      reset_variables_to_original(m_transformed_pbes);
    }
 
    const pbes& result() const
    {
      return m_transformed_pbes;
    }
};
 
/// \brief reset propositional variables
/// N.B. It is essential that this traverser uses the same traversal order as the guard_traverser.
struct reset_traverser: public pbes_expression_traverser<reset_traverser>
{
  using super = pbes_expression_traverser<reset_traverser>;
  using super::enter;
  using super::leave;
  using super::apply;
 
  global_reset_variables_algorithm& algorithm;
  const stategraph_equation& eq_X;
  std::size_t& i;
 
  reset_traverser(global_reset_variables_algorithm& algorithm_, const stategraph_equation& eq_X_, std::size_t& i_)
    : algorithm(algorithm_),
      eq_X(eq_X_),
      i(i_)
  {}
 
  std::vector<pbes_expression> expression_stack;
 
  void push(const pbes_expression& x)
  {
    mCRL2log(log::log_level_t::trace) << "<push>" << "\n" << x << std::endl;
    expression_stack.push_back(x);
  }
 
  pbes_expression& top()
  {
    return expression_stack.back();
  }
 
  const pbes_expression& top() const
  {
    return expression_stack.back();
  }
 
  pbes_expression pop()
  {
    pbes_expression result = top();
    expression_stack.pop_back();
    return result;
  }
 
  void leave(const data::data_expression& x)
  {
    push(atermpp::down_cast<pbes_expression>(x));
  }
 
  void leave(const pbes_system::propositional_variable_instantiation& x)
  {
    pbes_expression result = algorithm.reset_variable(x, eq_X, i);
    mCRL2log(log::log_level_t::debug) << "reset variable " << pbes_system::pp(x) << " with index " << i << " to " << pbes_system::pp(result) << std::endl;
    i++;
    push(result);
  }
 
  void leave(const pbes_system::not_& /* x */)
  {
    pbes_expression operand = pop();
    push(not_(static_cast<atermpp::aterm>(operand)));
  }
 
  void leave(const pbes_system::and_& /* x */)
  {
    pbes_expression right = pop();
    pbes_expression left = pop();
    push(and_(left, right));
  }
 
  void leave(const pbes_system::or_& /* x */)
  {
    pbes_expression right = pop();
    pbes_expression left = pop();
    push(or_(left, right));
  }
 
  void leave(const pbes_system::imp& /* x */)
  {
    pbes_expression right = pop();
    pbes_expression left = pop();
    push(imp(left, right));
  }
 
  void leave(const pbes_system::forall& x)
  {
    pbes_expression operand = pop();
    push(forall(x.variables(), operand));
  }
 
  void leave(const pbes_system::exists& x)
  {
    pbes_expression operand = pop();
    push(exists(x.variables(), operand));
  }
};
 
inline
pbes_expression reset_variables(global_reset_variables_algorithm& algorithm, const pbes_expression& x, const stategraph_equation& eq_X)
{
  std::size_t i = 0;
  reset_traverser f(algorithm, eq_X, i);
  f.apply(x);
  return f.top();
}
 
} // namespace mcrl2::pbes_system::detail
 
#endif // MCRL2_PBES_DETAIL_STATEGRAPH_GLOBAL_RESET_VARIABLES_H