Line data    Source code

       1             : // Author(s): Luc Engelen
       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 include/disjointness_checker.h
      10             : /// \brief Add your file description here.
      11             : 
      12             : // Interface to class Disjointness_Checker
      13             : // file: disjointness_checker.h
      14             : 
      15             : #ifndef MCRL2_LPS_DISJOINTNESS_CHECKER_H
      16             : #define MCRL2_LPS_DISJOINTNESS_CHECKER_H
      17             : 
      18             : #include "mcrl2/lps/linear_process.h"
      19             : 
      20             : /// \brief Class that can determine if two summands are syntactically disjoint.
      21             : /// Two summands are syntactically disjoint if the following conditions hold:
      22             : /// - The set of variables used by one summand is disjoint from the set of variables changed by the other summand and
      23             : ///   vice versa.
      24             : /// - The set of variables changed by one summand is disjoint from the set of variables changed by the other summand.
      25             : ///
      26             : /// An instance of the class Disjointness_Checker is created using the constructor
      27             : /// Disjointness_Checker::Disjointness_Checker. The parameter a_process_equations is used to pass the summands to be
      28             : /// checked for disjointness. The function Disjointness_Checker::disjoint indicates whether the two summands with numbers
      29             : /// n_1 and n_2 are syntactically disjoint.
      30             : 
      31             : namespace mcrl2
      32             : {
      33             : namespace lps
      34             : {
      35             : namespace detail
      36             : {
      37             : 
      38             : class Disjointness_Checker
      39             : {
      40             :   private:
      41             :     /// \brief The number of summands of the LPS passed as argument of the constructor.
      42             :     std::size_t f_number_of_summands;
      43             : 
      44             :     /// \brief A two dimensional array, indicating which parameters a summand uses, for each of the summands.
      45             :     std::vector<std::set<data::variable> > f_used_parameters_per_summand;
      46             : 
      47             :     /// \brief A two dimensional array, indicating which parameters a summand changes, for each of the summands.
      48             :     std::vector<std::set<data::variable> > f_changed_parameters_per_summand;
      49             : 
      50             :     /// \brief Updates the array Disjointness_Checker::f_used_parameters_per_summand, given the expression a_expression.
      51             :     void process_data_expression(std::size_t n, const data::data_expression& x);
      52             : 
      53             :     /// \brief Updates the array Disjointness_Checker::f_used_parameters_per_summand, given the multiaction a.
      54             :     void process_multi_action(std::size_t n, const multi_action& a);
      55             : 
      56             :     /// \brief Updates the arrays Disjointness_Checker::f_changed_parameters_per_summand and
      57             :     /// \brief Disjointness_Checker::f_used_parameters_per_summand, given the summand s.
      58             :     void process_summand(std::size_t n, const action_summand& s);
      59             : 
      60             :   public:
      61             :     /// \brief Constructor that initializes the sets Disjointness_Checker::f_used_parameters_per_summand and
      62             :     /// \brief Disjointness_Checker::f_changed_parameters_per_summand, and the indexed set
      63             :     /// \brief Disjointness_Checker::f_parameter_set.
      64             :     /// precondition: the argument passed as parameter a_process_equations is a specification of process equations in mCRL2
      65             :     /// format
      66             :     /// precondition: the arguments passed as parameters n_1 and n_2 correspond to summands in
      67             :     /// the proces equations passed as parameter a_process_equations. They lie in the interval from and including 1 upto and
      68             :     /// including the highest summand number
      69             :     template <typename LinearProcess>
      70             :     Disjointness_Checker(const LinearProcess& a_process_equation);
      71             : 
      72             :     /// \brief Indicates whether or not the summands with number n_1 and n_2 are disjoint.
      73             :     bool disjoint(std::size_t n1, std::size_t n2);
      74             : };
      75             : 
      76             : inline
      77         271 : void Disjointness_Checker::process_data_expression(std::size_t n, const data::data_expression& x)
      78             : {
      79             :   // This should probably once be replaced by a visitor.
      80         271 :   if (data::is_variable(x))
      81             :   {
      82          43 :     f_used_parameters_per_summand[n].insert(data::variable(x));
      83             :   }
      84         228 :   else if (data::is_where_clause(x))
      85             :   {
      86           0 :     const data::where_clause& t = atermpp::down_cast<data::where_clause>(x);
      87           0 :     process_data_expression(n, t.body());
      88           0 :     const data::assignment_list& assignments = t.assignments();
      89           0 :     for (const auto & assignment : assignments)
      90             :     {
      91           0 :       process_data_expression(n, assignment.rhs());
      92             :     }
      93             :   }
      94         228 :   else if (data::is_function_symbol(x))
      95             :   {
      96             :     // do nothing
      97             :   }
      98          71 :   else if (data::is_application(x))
      99             :   {
     100          71 :     const data::application& t = atermpp::down_cast<data::application>(x);
     101          71 :     process_data_expression(n, t.head());
     102         205 :     for (auto i = t.begin(); i != t.end(); ++i)
     103             :     {
     104         134 :       process_data_expression(n,*i);
     105             :     }
     106             :   }
     107           0 :   else if (data::is_abstraction(x))
     108             :   {
     109           0 :     const data::abstraction& t = atermpp::down_cast<data::abstraction>(x);
     110           0 :     process_data_expression(n, t.body());
     111             :   }
     112             :   else
     113             :   {
     114           0 :     throw mcrl2::runtime_error("disjointness checker encountered unknown term " + data::pp(x));
     115             :   }
     116         271 : }
     117             : 
     118             : inline
     119          20 : void Disjointness_Checker::process_multi_action(std::size_t n, const multi_action& a)
     120             : {
     121          20 :   if (a.has_time())
     122             :   {
     123           0 :     process_data_expression(n, a.time());
     124             :   }
     125             : 
     126          20 :   const process::action_list& v_actions = a.actions();
     127          31 :   for (const auto & v_action : v_actions)
     128             :   {
     129          11 :     const data::data_expression_list v_expressions=v_action.arguments();
     130             : 
     131          15 :     for (const auto & v_expression : v_expressions)
     132             :     {
     133           4 :       process_data_expression(n, v_expression);
     134             :     }
     135          11 :   }
     136          20 : }
     137             : 
     138             : inline
     139          20 : void Disjointness_Checker::process_summand(std::size_t n, const action_summand& s)
     140             : {
     141             :   // variables used in condition
     142          20 :   process_data_expression(n, s.condition());
     143             : 
     144             :   // variables used in multiaction
     145          20 :   process_multi_action(n, s.multi_action());
     146             : 
     147             :   // variables used and changed in assignments
     148          20 :   const data::assignment_list& v_assignments = s.assignments();
     149          62 :   for (const auto & v_assignment : v_assignments)
     150             :   {
     151             :     // variables changed in the assignment
     152          42 :     f_changed_parameters_per_summand[n].insert(v_assignment.lhs());
     153             : 
     154             :     // variables used in assignment
     155          42 :     process_data_expression(n, v_assignment.rhs());
     156             :   }
     157          20 : }
     158             : 
     159             : template <typename LinearProcess>
     160           5 : Disjointness_Checker::Disjointness_Checker(const LinearProcess& a_process_equation)
     161             : {
     162           5 :   const auto& v_summands = a_process_equation.action_summands();
     163           5 :   std::size_t v_summand_number = 1;
     164             : 
     165           5 :   f_number_of_summands = v_summands.size();
     166           5 :   f_used_parameters_per_summand =
     167          10 :     std::vector<std::set<data::variable> >(f_number_of_summands + 1, std::set<data::variable>());
     168           5 :   f_changed_parameters_per_summand =
     169          10 :     std::vector<std::set<data::variable> >(f_number_of_summands + 1, std::set<data::variable>());
     170             : 
     171          25 :   for (const auto & v_summand : v_summands)
     172             :   {
     173          20 :     process_summand(v_summand_number, v_summand);
     174          20 :     v_summand_number++;
     175             :   }
     176           5 : }
     177             : 
     178             : inline
     179          44 : bool Disjointness_Checker::disjoint(std::size_t n1, std::size_t n2)
     180             : {
     181             :   using utilities::detail::has_empty_intersection;
     182          44 :   assert(n1 <= f_number_of_summands && n2 <= f_number_of_summands);
     183          44 :   bool v_used_1_changed_2 = has_empty_intersection(f_used_parameters_per_summand[n1], f_changed_parameters_per_summand[n2]);
     184          44 :   bool v_used_2_changed_1 = has_empty_intersection(f_used_parameters_per_summand[n2], f_changed_parameters_per_summand[n1]);
     185          44 :   bool v_changed_1_changed_2 = has_empty_intersection(f_changed_parameters_per_summand[n1], f_changed_parameters_per_summand[n2]);
     186          44 :   return v_used_1_changed_2 && v_used_2_changed_1 && v_changed_1_changed_2;
     187             : }
     188             : 
     189             : } // namespace detail
     190             : } // namespace lps
     191             : } // namespace mcrl2
     192             : 
     193             : #endif