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/process/is_linear.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_IS_LINEAR_H
      13             : #define MCRL2_PROCESS_IS_LINEAR_H
      14             : 
      15             : #include "mcrl2/process/traverser.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : 
      20             : namespace process
      21             : {
      22             : 
      23             : namespace detail
      24             : {
      25             : 
      26             : /// \brief Returns true if the process instance assignment a matches with the process equation eq.
      27             : inline
      28         617 : bool check_process_instance_assignment(const process_equation& eq, const process_instance_assignment& inst)
      29             : {
      30         617 :   if (inst.identifier() != eq.identifier())
      31             :   {
      32           0 :     return false;
      33             :   }
      34         617 :   const data::variable_list& v = eq.formal_parameters();
      35             : 
      36             :   // check if the left hand sides of the assignments exist
      37        2289 :   for (const auto& a: inst.assignments())
      38             :   {
      39        1672 :     if (std::find(v.begin(), v.end(), a.lhs()) == v.end())
      40             :     {
      41           0 :       return false;
      42             :     }
      43             :   }
      44         617 :   return true;
      45             : }
      46             : 
      47             : /// \brief Returns true if the process instance a matches with the process equation eq.
      48             : inline
      49         453 : bool check_process_instance(const process_equation& eq, const process_instance& init)
      50             : {
      51         453 :   if (eq.identifier() != init.identifier())
      52             :   {
      53           0 :     return false;
      54             :   }
      55         453 :   const data::variable_list& v = eq.formal_parameters();
      56         453 :   const data::data_expression_list& e = init.actual_parameters();
      57         453 :   data::variable_list::const_iterator i = v.begin();
      58         453 :   data::data_expression_list::const_iterator j = e.begin();
      59        1094 :   for (; i != v.end(); ++i, ++j)
      60             :   {
      61         641 :     if (i->sort() != j->sort())
      62             :     {
      63           0 :       return false;
      64             :     }
      65             :   }
      66         453 :   return true;
      67             : }
      68             : 
      69             : /// \brief Returns true if the argument is a process instance
      70             : inline
      71         688 : bool is_process(const process_expression& x)
      72             : {
      73         688 :   return is_process_instance(x)
      74         688 :          || is_process_instance_assignment(x)
      75             :          ;
      76             : }
      77             : 
      78             : /// \brief Returns true if the argument is a process instance, optionally wrapped in a stochastic
      79             : /// distribution.
      80             : inline
      81         666 : bool is_stochastic_process(const process_expression& x)
      82             : {
      83         666 :   if (is_process(x))
      84             :   {
      85         638 :     return true;
      86             :   }
      87          28 :   if (is_stochastic_operator(x))
      88             :   {
      89          22 :     return is_process(atermpp::down_cast<stochastic_operator>(x).operand());
      90             :   }
      91           6 :   return false;
      92             : }
      93             : 
      94             : /// \brief Returns true if the argument is a deadlock
      95             : inline
      96          12 : bool is_timed_deadlock(const process_expression& x)
      97             : {
      98          12 :   return is_delta(x)
      99          12 :          || is_at(x)
     100             :          ;
     101             : }
     102             : 
     103             : /// \brief Returns true if the argument is a multi-action
     104             : inline
     105         476 : bool is_multiaction(const process_expression& x)
     106             : {
     107         476 :   return is_tau(x)
     108         444 :          || is_sync(x)
     109         920 :          || is_action(x)
     110             :          ;
     111             : }
     112             : 
     113             : /// \brief Returns true if the argument is a multi-action
     114             : inline
     115         474 : bool is_timed_multiaction(const process_expression& x)
     116             : {
     117         474 :   return is_at(x)
     118         474 :          || is_multiaction(x);
     119             : }
     120             : 
     121             : /// \brief Returns true if the argument is an action prefix
     122             : inline
     123         428 : bool is_action_prefix(const process_expression& x)
     124             : {
     125         428 :   return is_seq(x)
     126         428 :          || is_timed_multiaction(x);
     127             : }
     128             : 
     129             : /// \brief Returns true if the argument is a conditional deadlock
     130             : inline
     131           0 : bool is_conditional_deadlock(const process_expression& x)
     132             : {
     133           0 :   return is_if_then(x)
     134           0 :          || is_timed_deadlock(x);
     135             : }
     136             : 
     137             : /// \brief Returns true if the argument is a conditional action prefix.
     138             : inline
     139         129 : bool is_conditional_action_prefix(const process_expression& x)
     140             : {
     141         129 :   return is_if_then(x)
     142         129 :          || is_action_prefix(x);
     143             : }
     144             : 
     145             : /// \brief Returns true if the argument is an alternative composition
     146             : inline
     147         141 : bool is_alternative(const process_expression& x)
     148             : {
     149         141 :   return is_sum(x)
     150         129 :          || is_conditional_action_prefix(x)
     151         270 :          || is_conditional_deadlock(x)
     152             :          ;
     153             : }
     154             : 
     155             : /// \brief Returns true if the argument is a linear process
     156             : inline
     157             : bool is_linear_process_term(const process_expression& x)
     158             : {
     159             :   return is_choice(x)
     160             :          || is_alternative(x)
     161             :          ;
     162             : }
     163             : 
     164             : /// \brief Checks if a process equation is linear.
     165             : /// Use the is_linear() member function for this.
     166             : struct linear_process_expression_traverser: public process_expression_traverser<linear_process_expression_traverser>
     167             : {
     168             :   typedef process_expression_traverser<linear_process_expression_traverser> super;
     169             :   using super::enter;
     170             :   using super::leave;
     171             :   using super::apply;
     172             : 
     173             :   /// \brief The process equation that is checked.
     174             :   process_equation eqn;
     175             : 
     176             :   /// \brief Exception that is thrown by linear_process_expression_traverser.
     177             :   struct non_linear_process_error: public mcrl2::runtime_error
     178             :   {
     179           2 :     explicit non_linear_process_error(const std::string& msg)
     180           2 :       : mcrl2::runtime_error(msg)
     181           2 :     {}
     182             :   };
     183             : 
     184         206 :   linear_process_expression_traverser(const process_equation& eqn_ = process_equation())
     185         206 :    : eqn(eqn_)
     186         206 :   {}
     187             : 
     188             :   // TODO: check if this function is needed
     189         150 :   void enter(const process::process_instance& x)
     190             :   {
     191         150 :     if (!detail::check_process_instance(eqn, x))
     192             :     {
     193           0 :       throw non_linear_process_error(process::pp(x) + " is not a valid process instance");
     194             :     }
     195         150 :   }
     196             : 
     197         310 :   void enter(const process::process_instance_assignment& x)
     198             :   {
     199         310 :     if (!detail::check_process_instance_assignment(eqn, x))
     200             :     {
     201           0 :       throw non_linear_process_error(process::pp(x) + " is not a valid process instance assignment");
     202             :     }
     203         310 :   }
     204             : 
     205         141 :   void enter(const process::sum& x)
     206             :   {
     207         141 :     if (!is_alternative(x.operand()))
     208             :     {
     209           0 :       throw non_linear_process_error(process::pp(x.operand()) + " is not an alternative expression");
     210             :     }
     211         141 :   }
     212             : 
     213           0 :   void enter(const process::block& x)
     214             :   {
     215           0 :     throw non_linear_process_error("block expression " + process::pp(x) + " encountered");
     216             :   }
     217             : 
     218           0 :   void enter(const process::hide& x)
     219             :   {
     220           0 :     throw non_linear_process_error("hide expression " + process::pp(x) + " encountered");
     221             :   }
     222             : 
     223           0 :   void enter(const process::rename& x)
     224             :   {
     225           0 :     throw non_linear_process_error("rename expression " + process::pp(x) + " encountered");
     226             :   }
     227             : 
     228           0 :   void enter(const process::comm& x)
     229             :   {
     230           0 :     throw non_linear_process_error("comm expression " + process::pp(x) + " encountered");
     231             :   }
     232             : 
     233           0 :   void enter(const process::allow& x)
     234             :   {
     235           0 :     throw non_linear_process_error("allow expression " + process::pp(x) + " encountered");
     236             :   }
     237             : 
     238           2 :   void enter(const process::sync& x)
     239             :   {
     240           2 :     if (!is_multiaction(x.left()) || !is_multiaction(x.right()))
     241             :     {
     242           0 :       if (!is_multiaction(x.left()))
     243             :       {
     244           0 :         throw non_linear_process_error(process::pp(x.left()) + " is not a multi action");
     245             :       }
     246             :       else
     247             :       {
     248           0 :         throw non_linear_process_error(process::pp(x.right()) + " is not a multi action");
     249             :       }
     250             :     }
     251           2 :   }
     252             : 
     253           8 :   void enter(const process::at& x)
     254             :   {
     255           8 :     if (!is_multiaction(x.operand()) && !is_delta(x.operand()))
     256             :     {
     257           0 :       throw non_linear_process_error(process::pp(x.operand()) + " is not a multi action and not a deadlock");
     258             :     }
     259           8 :   }
     260             : 
     261         462 :   void enter(const process::seq& x)
     262             :   {
     263         462 :     if (!is_timed_multiaction(x.left()) || !is_stochastic_process(x.right()))
     264             :     {
     265           2 :       throw non_linear_process_error(process::pp(x.left()) + " is not a timed multi action and not a process");
     266             :     }
     267         460 :     process_expression right = x.right();
     268         460 :     if (is_stochastic_operator(right))
     269             :     {
     270          18 :       right = atermpp::down_cast<stochastic_operator>(right).operand();
     271             :     }
     272         460 :     if (is_process_instance(right))
     273             :     {
     274         150 :       const auto& right_ = atermpp::down_cast<process_instance>(right);
     275         150 :       if (right_.identifier() != eqn.identifier())
     276             :       {
     277           0 :         throw non_linear_process_error(process::pp(right_) + " has an unexpected identifier");
     278             :       }
     279             :     }
     280         310 :     else if (is_process_instance_assignment(right))
     281             :     {
     282         310 :       const auto& right_ = atermpp::down_cast<process_instance_assignment>(right);
     283         310 :       if (right_.identifier() != eqn.identifier())
     284             :       {
     285           0 :         throw non_linear_process_error(process::pp(right_) + " has an unexpected identifier");
     286             :       }
     287             :     }
     288             :     else
     289             :     {
     290           0 :       std::cerr << "seq right hand side: " << process::pp(right) << std::endl;
     291           0 :       throw std::runtime_error("unexpected error in visit_seq");
     292             :     }
     293         460 :   }
     294             : 
     295         404 :   void enter(const process::if_then& x)
     296             :   {
     297         404 :     if (!is_action_prefix(x.then_case()) && !is_timed_deadlock(x.then_case()))
     298             :     {
     299           0 :       throw non_linear_process_error(process::pp(x) + " is not an action prefix and not a timed deadlock");
     300             :     }
     301         404 :   }
     302             : 
     303           0 :   void enter(const process::if_then_else& x)
     304             :   {
     305           0 :     throw non_linear_process_error("if then else expression " + process::pp(x) + " encountered");
     306             :   }
     307             : 
     308           0 :   void enter(const process::bounded_init& x)
     309             :   {
     310           0 :     throw non_linear_process_error("bounded init expression " + process::pp(x) + " encountered");
     311             :   }
     312             : 
     313           0 :   void enter(const process::merge& x)
     314             :   {
     315           0 :     throw non_linear_process_error("merge expression " + process::pp(x) + " encountered");
     316             :   }
     317             : 
     318           0 :   void enter(const process::left_merge& x)
     319             :   {
     320           0 :     throw non_linear_process_error("left merge expression " + process::pp(x) + " encountered");
     321             :   }
     322             : 
     323             : 
     324             :   /// \brief Returns true if the process equation e is linear.
     325         206 :   bool is_linear(const process_expression& x, bool verbose = false)
     326             :   {
     327             :     try
     328             :     {
     329         206 :       this->apply(x);
     330             :     }
     331           2 :     catch (non_linear_process_error& p)
     332             :     {
     333           2 :       if (verbose)
     334             :       {
     335           1 :         std::clog << p.what() << std::endl;
     336             :       }
     337           2 :       return false;
     338           2 :     }
     339         204 :     return true;
     340             :   }
     341             : };
     342             : 
     343             : } // namespace detail
     344             : 
     345             : /// \brief Returns true if the process specification is linear.
     346             : inline
     347         206 : bool is_linear(const process_specification& p, bool verbose = false)
     348             : {
     349         206 :   if (p.equations().size() != 1)
     350             :   {
     351           0 :     if (verbose)
     352             :     {
     353           0 :       std::clog << "warning: the number of equations is not equal to 1" << std::endl;
     354             :     }
     355           0 :     return false;
     356             :   }
     357         206 :   const process_equation& eqn = p.equations().front();
     358         206 :   detail::linear_process_expression_traverser visitor(eqn);
     359             :   {
     360         206 :     if (!visitor.is_linear(eqn.expression(), verbose))
     361             :     {
     362           2 :       if (verbose)
     363             :       {
     364           1 :         std::clog << "warning: the first equation is not linear" << std::endl;
     365             :       }
     366           2 :       return false;
     367             :     }
     368         204 :     if (!detail::is_stochastic_process(p.init()))
     369             :     {
     370           4 :       if (verbose)
     371             :       {
     372           2 :         std::clog << "warning: the initial process " << process::pp(p.init()) << " is not a process instance or a process instance assignment" << std::endl;
     373             :       }
     374           4 :       return false;
     375             :     }
     376             :   }
     377         200 :   return true;
     378         206 : }
     379             : 
     380             : /// \brief Returns true if the process equation is linear.
     381             : inline
     382             : bool is_linear(const process_equation& eqn)
     383             : {
     384             :   detail::linear_process_expression_traverser f(eqn);
     385             :   return f.is_linear(eqn.expression());
     386             : }
     387             : 
     388             : /// \brief Returns true if the process expression is linear.
     389             : /// \param x A process expression.
     390             : /// \param eqn The linear equation belonging to the indicated process.
     391             : inline
     392             : bool is_linear(const process_expression& x, const process_equation& eqn)
     393             : {
     394             :   detail::linear_process_expression_traverser f(eqn);
     395             :   return f.is_linear(x);
     396             : }
     397             : 
     398             : } // namespace process
     399             : 
     400             : } // namespace mcrl2
     401             : 
     402             : #endif // MCRL2_PROCESS_IS_LINEAR_H