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/lps/detail/linear_process_conversion_traverser.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_DETAIL_LINEAR_PROCESS_CONVERSION_TRAVERSER_H
      13             : #define MCRL2_LPS_DETAIL_LINEAR_PROCESS_CONVERSION_TRAVERSER_H
      14             : 
      15             : #include "mcrl2/lps/stochastic_specification.h"
      16             : #include "mcrl2/process/is_linear.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace process
      22             : {
      23             : 
      24             : namespace detail
      25             : {
      26             : 
      27             : // TODO: join the stochastic and non-stochastic versions of the traversers
      28             : 
      29             : /// \brief Converts a process expression into linear process format.
      30             : /// Use the \p convert member functions for this.
      31             : struct linear_process_conversion_traverser: public process_expression_traverser<linear_process_conversion_traverser>
      32             : {
      33             :   typedef process_expression_traverser<linear_process_conversion_traverser> super;
      34             :   using super::enter;
      35             :   using super::leave;
      36             :   using super::apply;
      37             : 
      38             :   /// \brief The result of the conversion.
      39             :   lps::action_summand_vector m_action_summands;
      40             : 
      41             :   /// \brief The result of the conversion.
      42             :   lps::deadlock_summand_vector m_deadlock_summands;
      43             : 
      44             :   /// \brief The process equation that is checked.
      45             :   process_equation m_equation;
      46             : 
      47             :   /// \brief Contains intermediary results.
      48             :   data::variable_list m_sum_variables;
      49             : 
      50             :   /// \brief Contains intermediary results.
      51             :   data::assignment_list m_next_state;
      52             : 
      53             :   /// \brief Contains intermediary results.
      54             :   lps::multi_action m_multi_action;
      55             : 
      56             :   /// \brief Contains intermediary results.
      57             :   lps::deadlock m_deadlock;
      58             : 
      59             :   /// \brief True if m_deadlock was changed.
      60             :   bool m_deadlock_changed;
      61             : 
      62             :   /// \brief True if m_multi_action was changed.
      63             :   bool m_multi_action_changed;
      64             : 
      65             :   /// \brief True if m_next_state was changed.
      66             :   bool m_next_state_changed;
      67             : 
      68             :   /// \brief Contains intermediary results.
      69             :   data::data_expression m_condition;
      70             : 
      71             :   /// \brief Exception that is thrown to denote that the process is not linear.
      72             :   struct non_linear_process
      73             :   {
      74             :     process_expression expr;
      75             : 
      76           0 :     non_linear_process(const process_expression& p)
      77           0 :       : expr(p)
      78           0 :     {}
      79             :   };
      80             : 
      81             :   /// \brief Clears the current summand
      82         554 :   void clear_summand()
      83             :   {
      84         554 :     m_sum_variables = data::variable_list();
      85         554 :     m_deadlock = lps::deadlock();
      86         554 :     m_deadlock_changed = false;
      87         554 :     m_multi_action = lps::multi_action();
      88         554 :     m_multi_action_changed = false;
      89         554 :     m_condition = data::sort_bool::true_();
      90         554 :     m_next_state = data::assignment_list();
      91         554 :     m_next_state_changed = false;
      92         554 :   }
      93             : 
      94             :   /// \brief Adds a summand to the result
      95         477 :   void add_summand()
      96             :   {
      97         477 :     if (m_multi_action_changed)
      98             :     {
      99         361 :       if (m_next_state_changed)
     100             :       {
     101         359 :         m_action_summands.push_back(lps::action_summand(m_sum_variables, m_condition, m_multi_action, m_next_state));
     102         359 :         mCRL2log(log::debug) << "adding action summand\n" << m_action_summands.back() << std::endl;
     103         359 :         clear_summand();
     104             :       }
     105             :       else
     106             :       {
     107           2 :         throw mcrl2::runtime_error("Error in linear_process_conversion_traverser::convert: encountered a multi action without process reference");
     108             :       }
     109             :     }
     110         116 :     else if (m_deadlock_changed)
     111             :     {
     112          57 :       m_deadlock_summands.push_back(lps::deadlock_summand(m_sum_variables, m_condition, m_deadlock));
     113          57 :       mCRL2log(log::debug) << "adding deadlock summand\n" << m_deadlock_summands.back() << std::endl;
     114          57 :       clear_summand();
     115             :     }
     116         475 :   }
     117             : 
     118             :   /// \brief Visit delta node
     119             :   /// \return The result of visiting the node
     120             :   /// \param x A process expression
     121          57 :   void leave(const delta& /* x */)
     122             :   {
     123          57 :     m_deadlock = lps::deadlock();
     124          57 :     m_deadlock_changed = true;
     125          57 :     mCRL2log(log::debug) << "adding deadlock\n" << m_deadlock << std::endl;
     126          57 :   }
     127             : 
     128             :   /// \brief Visit tau node
     129             :   /// \return The result of visiting the node
     130             :   /// \param x A process expression
     131          25 :   void leave(const process::tau& /* x */)
     132             :   {
     133          25 :     m_multi_action = lps::multi_action();
     134          25 :     m_multi_action_changed = true;
     135          25 :     mCRL2log(log::debug) << "adding multi action tau\n" << m_multi_action << std::endl;
     136          25 :   }
     137             : 
     138             :   /// \brief Visit action node
     139             :   /// \return The result of visiting the node
     140             :   /// \param x A process expression
     141             :   /// \param l An action label
     142             :   /// \param v A sequence of data expressions
     143         336 :   void leave(const process::action& x)
     144             :   {
     145         336 :     action a(x.label(), x.arguments());
     146         336 :     m_multi_action = lps::multi_action(a);
     147         336 :     m_multi_action_changed = true;
     148         336 :     mCRL2log(log::debug) << "adding multi action\n" << m_multi_action << std::endl;
     149         336 :   }
     150             : 
     151             :   /// \brief Visit sum node
     152             :   /// \return The result of visiting the node
     153             :   /// \param x A process expression
     154             :   /// \param v A sequence of data variables
     155             :   /// \param right A process expression
     156          84 :   void leave(const process::sum& x)
     157             :   {
     158          84 :     m_sum_variables = m_sum_variables + x.variables();
     159          84 :     mCRL2log(log::debug) << "adding sum variables\n" << data::pp(x.variables()) << std::endl;
     160          84 :   }
     161             : 
     162             :   /// \brief Visit block node
     163             :   /// \return The result of visiting the node
     164             :   /// \param x A process expression
     165             :   /// \param s A sequence of identifiers
     166             :   /// \param right A process expression
     167           0 :   void leave(const process::block& x)
     168             :   {
     169           0 :     throw non_linear_process(x);
     170             :   }
     171             : 
     172             :   /// \brief Visit hide node
     173             :   /// \return The result of visiting the node
     174             :   /// \param x A process expression
     175             :   /// \param s A sequence of identifiers
     176             :   /// \param right A process expression
     177           0 :   void leave(const process::hide& x)
     178             :   {
     179           0 :     throw non_linear_process(x);
     180             :   }
     181             : 
     182             :   /// \brief Visit rename node
     183             :   /// \return The result of visiting the node
     184             :   /// \param x A process expression
     185             :   /// \param r A sequence of rename expressions
     186             :   /// \param right A process expression
     187           0 :   void leave(const process::rename& x)
     188             :   {
     189           0 :     throw non_linear_process(x);
     190             :   }
     191             : 
     192             :   /// \brief Visit comm node
     193             :   /// \return The result of visiting the node
     194             :   /// \param x A process expression
     195             :   /// \param c A sequence of communication expressions
     196             :   /// \param right A process expression
     197           0 :   void leave(const process::comm& x)
     198             :   {
     199           0 :     throw non_linear_process(x);
     200             :   }
     201             : 
     202             :   /// \brief Visit allow node
     203             :   /// \return The result of visiting the node
     204             :   /// \param x A process expression
     205             :   /// \param s A sequence of multi-action names
     206             :   /// \param right A process expression
     207           0 :   void leave(const process::allow& x)
     208             :   {
     209           0 :     throw non_linear_process(x);
     210             :   }
     211             : 
     212             :   /// \brief Visit sync node
     213             :   /// \return The result of visiting the node
     214             :   /// \param x A process expression
     215             :   /// \param left A process expression
     216             :   /// \param right A process expression
     217           0 :   void apply(const process::sync& x)
     218             :   {
     219           0 :     apply(x.left());
     220           0 :     lps::multi_action l = m_multi_action;
     221           0 :     apply(x.right());
     222           0 :     lps::multi_action r = m_multi_action;
     223           0 :     m_multi_action = l + r;
     224           0 :     m_multi_action_changed = true;
     225           0 :     mCRL2log(log::debug) << "adding multi action\n" << m_multi_action << std::endl;
     226           0 :   }
     227             : 
     228             :   /// \brief Visit at node
     229             :   /// \return The result of visiting the node
     230             :   /// \param x A process expression
     231             :   /// \param left A process expression
     232             :   /// \param d A data expression
     233           3 :   void leave(const process::at& x)
     234             :   {
     235           3 :     if (is_delta(x))
     236             :     {
     237           0 :       m_deadlock.time() = x.time_stamp();
     238           0 :       mCRL2log(log::debug) << "adding deadlock\n" << m_deadlock << std::endl;
     239             :     }
     240             :     else
     241             :     {
     242           3 :       m_multi_action=lps::multi_action(m_multi_action.actions(), x.time_stamp());
     243           3 :       mCRL2log(log::debug) << "adding multi action\n" << m_multi_action << std::endl;
     244             :     }
     245           3 :   }
     246             : 
     247             :   /// \brief Visit seq node
     248             :   /// \return The result of visiting the node
     249             :   /// \param x A process expression
     250             :   /// \param left A process expression
     251             :   /// \param right A process expression
     252         359 :   void apply(const process::seq& x)
     253             :   {
     254         359 :     apply(x.left());
     255             : 
     256             :     // Check 1) The expression right must be a process instance or a process assignment
     257         359 :     if (is_process_instance(x.right()))
     258             :     {
     259         106 :       const process_instance& p = atermpp::down_cast<process_instance>(x.right());
     260             :       // Check 2) The process equation and and the process instance must match
     261         106 :       if (!detail::check_process_instance(m_equation, p))
     262             :       {
     263           0 :         std::clog << "seq right hand side: " << process::pp(x.right()) << std::endl;
     264           0 :         throw mcrl2::runtime_error("Error in linear_process_conversion_traverser::convert: seq expression encountered that does not match the process equation");
     265             :       }
     266         106 :       m_next_state = data::make_assignment_list(m_equation.formal_parameters(), p.actual_parameters());
     267         106 :       m_next_state_changed = true;
     268             :     }
     269         253 :     else if (is_process_instance_assignment(x.right()))
     270             :     {
     271         253 :       const process_instance_assignment& p = atermpp::down_cast<process_instance_assignment>(x.right());
     272             :       // Check 2) The process equation and and the process instance assignment must match
     273         253 :       if (!detail::check_process_instance_assignment(m_equation, p))
     274             :       {
     275           0 :         std::clog << "seq right hand side: " << process::pp(x.right()) << std::endl;
     276           0 :         throw mcrl2::runtime_error("Error in linear_process_conversion_traverser::convert: seq expression encountered that does not match the process equation");
     277             :       }
     278         253 :       m_next_state = p.assignments(); // TODO: check if this is correct
     279         253 :       m_next_state_changed = true;
     280             :     }
     281             :     else
     282             :     {
     283           0 :       std::clog << "seq right hand side: " << process::pp(x.right()) << std::endl;
     284           0 :       throw mcrl2::runtime_error("Error in linear_process_conversion_traverser::convert: seq expression encountered with an unexpected right hand side");
     285             :     }
     286             : 
     287         359 :     mCRL2log(log::debug) << "adding next state\n" << data::pp(m_next_state) << std::endl;
     288         359 :   }
     289             : 
     290             :   /// \brief Visit if_then node
     291             :   /// \return The result of visiting the node
     292             :   /// \param x A process expression
     293             :   /// \param d A data expression
     294             :   /// \param right A process expression
     295         313 :   void leave(const process::if_then& x)
     296             :   {
     297         313 :     m_condition = x.condition();
     298         313 :     mCRL2log(log::debug) << "adding condition\n" << data::pp(m_condition) << std::endl;
     299         313 :   }
     300             : 
     301             :   /// \brief Visit if_then_else node
     302             :   /// \return The result of visiting the node
     303             :   /// \param x A process expression
     304             :   /// \param d A data expression
     305             :   /// \param left A process expression
     306             :   /// \param right A process expression
     307           0 :   void leave(const process::if_then_else& x)
     308             :   {
     309           0 :     throw non_linear_process(x);
     310             :   }
     311             : 
     312             :   /// \brief Visit bounded_init node
     313             :   /// \return The result of visiting the node
     314             :   /// \param x A process expression
     315             :   /// \param left A process expression
     316             :   /// \param right A process expression
     317           0 :   void leave(const process::bounded_init& x)
     318             :   {
     319           0 :     throw non_linear_process(x);
     320             :   }
     321             : 
     322             :   /// \brief Visit merge node
     323             :   /// \return The result of visiting the node
     324             :   /// \param x A process expression
     325             :   /// \param left A process expression
     326             :   /// \param right A process expression
     327           0 :   void leave(const process::merge& x)
     328             :   {
     329           0 :     throw non_linear_process(x);
     330             :   }
     331             : 
     332             :   /// \brief Visit left_merge node
     333             :   /// \return The result of visiting the node
     334             :   /// \param x A process expression
     335             :   /// \param left A process expression
     336             :   /// \param right A process expression
     337           0 :   void leave(const process::left_merge& x)
     338             :   {
     339           0 :     throw non_linear_process(x);
     340             :   }
     341             : 
     342             :   /// \brief Visit choice node
     343             :   /// \return The result of visiting the node
     344             :   /// \param x A process expression
     345             :   /// \param left A process expression
     346             :   /// \param right A process expression
     347         280 :   void apply(const process::choice& x)
     348             :   {
     349         280 :     apply(x.left());
     350         280 :     if (!is_choice(x.left()))
     351             :     {
     352          59 :       add_summand();
     353             :     }
     354         280 :     apply(x.right());
     355         280 :     if (!is_choice(x.right()))
     356             :     {
     357         280 :       add_summand();
     358             :     }
     359         280 :   }
     360             : 
     361             :   /// \brief Returns true if the process equation e is linear.
     362             :   /// \param e A process equation
     363         138 :   void convert(const process_equation& /* e */)
     364             :   {
     365         138 :     clear_summand();
     366         138 :     apply(m_equation.expression());
     367         138 :     add_summand(); // needed if it is not a choice
     368         136 :   }
     369             : 
     370             :   /// \brief Converts a process_specification into a specification.
     371             :   /// Throws \p non_linear_process if a non-linear sub-expression is encountered.
     372             :   /// Throws \p mcrl2::runtime_error in the following cases:
     373             :   /// \li The number of equations is not equal to one
     374             :   /// \li The initial process is not a process instance, or it does not match with the equation
     375             :   /// \li A sequential process is found with a right hand side that is not a process instance,
     376             :   /// or it doesn't match the equation
     377             :   /// \param p A process specification
     378             :   /// \return The converted specification
     379         138 :   lps::specification convert(const process_specification& p)
     380             :   {
     381         138 :     m_action_summands.clear();
     382         138 :     m_deadlock_summands.clear();
     383             : 
     384             :     // Check 1) The number of equations must be one
     385         138 :     if (p.equations().size() != 1)
     386             :     {
     387           0 :       throw mcrl2::runtime_error("Error in linear_process_conversion_traverser::convert: the number of process equations is not equal to 1!");
     388             :     }
     389         138 :     m_equation = p.equations().front();
     390             : 
     391         138 :     lps::process_initializer proc_init;
     392             : 
     393         138 :     if (is_process_instance(p.init()))
     394             :     {
     395         137 :       const process_instance& init = atermpp::down_cast<process_instance>(p.init());
     396         137 :       if (!check_process_instance(m_equation, init))
     397             :       {
     398           0 :         throw mcrl2::runtime_error("Error in linear_process_conversion_traverser::convert: the initial process does not match the process equation");
     399             :       }
     400         137 :       proc_init = lps::process_initializer(init.actual_parameters());
     401             :     }
     402           1 :     else if (is_process_instance_assignment(p.init()))
     403             :     {
     404           1 :       const process_instance_assignment& init = atermpp::down_cast<process_instance_assignment>(p.init());
     405           1 :       if (!check_process_instance_assignment(m_equation, init))
     406             :       {
     407           0 :         throw mcrl2::runtime_error("Error in linear_process_conversion_traverser::convert: the initial process does not match the process equation");
     408             :       }
     409           1 :       proc_init = lps::process_initializer(data::right_hand_sides(init.assignments()));
     410             :     }
     411             :     else
     412             :     {
     413           0 :       throw mcrl2::runtime_error("Error in linear_process_conversion_traverser::convert: the initial process has an unexpected value");
     414             :     }
     415             : 
     416             :     // Do the conversion
     417         138 :     convert(m_equation);
     418             : 
     419         136 :     lps::linear_process proc(m_equation.formal_parameters(), m_deadlock_summands, m_action_summands);
     420         272 :     return lps::specification(p.data(), p.action_labels(), p.global_variables(), proc, proc_init);
     421         138 :   }
     422             : };
     423             : 
     424             : /// \brief Converts a process expression into linear process format.
     425             : /// Use the \p convert member functions for this.
     426             : struct stochastic_linear_process_conversion_traverser: public process_expression_traverser<stochastic_linear_process_conversion_traverser>
     427             : {
     428             :   typedef process_expression_traverser<stochastic_linear_process_conversion_traverser> super;
     429             :   using super::enter;
     430             :   using super::leave;
     431             :   using super::apply;
     432             : 
     433             :   /// \brief The result of the conversion.
     434             :   lps::stochastic_action_summand_vector m_action_summands;
     435             : 
     436             :   /// \brief The result of the conversion.
     437             :   lps::deadlock_summand_vector m_deadlock_summands;
     438             : 
     439             :   /// \brief The process equation that is checked.
     440             :   process_equation m_equation;
     441             : 
     442             :   /// \brief Contains intermediary results.
     443             :   data::variable_list m_sum_variables;
     444             : 
     445             :   /// \brief Contains intermediary results.
     446             :   data::assignment_list m_next_state;
     447             : 
     448             :   /// \brief Contains intermediary results.
     449             :   lps::multi_action m_multi_action;
     450             : 
     451             :   /// \brief Contains intermediary results.
     452             :   lps::deadlock m_deadlock;
     453             : 
     454             :   /// \brief Contains intermediary results.
     455             :   lps::stochastic_distribution m_distribution;
     456             : 
     457             :   /// \brief True if m_deadlock was changed.
     458             :   bool m_deadlock_changed;
     459             : 
     460             :   /// \brief True if m_multi_action was changed.
     461             :   bool m_multi_action_changed;
     462             : 
     463             :   /// \brief True if m_next_state was changed.
     464             :   bool m_next_state_changed;
     465             : 
     466             :   /// \brief Contains intermediary results.
     467             :   data::data_expression m_condition;
     468             : 
     469             :   /// \brief Exception that is thrown to denote that the process is not linear.
     470             :   struct non_linear_process
     471             :   {
     472             :     process_expression expr;
     473             : 
     474           0 :     non_linear_process(const process_expression& p)
     475           0 :       : expr(p)
     476           0 :     {}
     477             :   };
     478             : 
     479             :   /// \brief Clears the current summand
     480         124 :   void clear_summand()
     481             :   {
     482         124 :     m_sum_variables = data::variable_list();
     483         124 :     m_deadlock = lps::deadlock();
     484         124 :     m_deadlock_changed = false;
     485         124 :     m_multi_action = lps::multi_action();
     486         124 :     m_multi_action_changed = false;
     487         124 :     m_condition = data::sort_bool::true_();
     488         124 :     m_distribution = lps::stochastic_distribution();
     489         124 :     m_next_state = data::assignment_list();
     490         124 :     m_next_state_changed = false;
     491         124 :   }
     492             : 
     493             :   /// \brief Adds a summand to the result
     494         102 :   void add_summand()
     495             :   {
     496         102 :     if (m_multi_action_changed)
     497             :     {
     498          77 :       if (m_next_state_changed)
     499             :       {
     500          77 :         m_action_summands.push_back(lps::stochastic_action_summand(m_sum_variables, m_condition, m_multi_action, m_next_state, m_distribution));
     501          77 :         mCRL2log(log::debug) << "adding action summand\n" << m_action_summands.back() << std::endl;
     502          77 :         clear_summand();
     503             :       }
     504             :       else
     505             :       {
     506           0 :         throw mcrl2::runtime_error("Error in stochastic_linear_process_conversion_traverser::convert: encountered a multi action without process reference");
     507             :       }
     508             :     }
     509          25 :     else if (m_deadlock_changed)
     510             :     {
     511          11 :       m_deadlock_summands.push_back(lps::deadlock_summand(m_sum_variables, m_condition, m_deadlock));
     512          11 :       mCRL2log(log::debug) << "adding deadlock summand\n" << m_deadlock_summands.back() << std::endl;
     513          11 :       clear_summand();
     514             :     }
     515         102 :   }
     516             : 
     517             :   /// \brief Visit delta node
     518             :   /// \return The result of visiting the node
     519             :   /// \param x A process expression
     520          11 :   void leave(const delta& /* x */)
     521             :   {
     522          11 :     m_deadlock = lps::deadlock();
     523          11 :     m_deadlock_changed = true;
     524          11 :     mCRL2log(log::debug) << "adding deadlock\n" << m_deadlock << std::endl;
     525          11 :   }
     526             : 
     527             :   /// \brief Visit tau node
     528             :   /// \return The result of visiting the node
     529             :   /// \param x A process expression
     530           8 :   void leave(const process::tau& /* x */)
     531             :   {
     532           8 :     m_multi_action = lps::multi_action();
     533           8 :     m_multi_action_changed = true;
     534           8 :     mCRL2log(log::debug) << "adding multi action tau\n" << m_multi_action << std::endl;
     535           8 :   }
     536             : 
     537             :   /// \brief Visit action node
     538             :   /// \return The result of visiting the node
     539             :   /// \param x A process expression
     540             :   /// \param l An action label
     541             :   /// \param v A sequence of data expressions
     542          71 :   void leave(const process::action& x)
     543             :   {
     544          71 :     action a(x.label(), x.arguments());
     545          71 :     m_multi_action = lps::multi_action(a);
     546          71 :     m_multi_action_changed = true;
     547          71 :     mCRL2log(log::debug) << "adding multi action\n" << m_multi_action << std::endl;
     548          71 :   }
     549             : 
     550             :   /// \brief Visit sum node
     551             :   /// \return The result of visiting the node
     552             :   /// \param x A process expression
     553             :   /// \param v A sequence of data variables
     554             :   /// \param right A process expression
     555          27 :   void leave(const process::sum& x)
     556             :   {
     557          27 :     m_sum_variables = m_sum_variables + x.variables();
     558          27 :     mCRL2log(log::debug) << "adding sum variables\n" << data::pp(x.variables()) << std::endl;
     559          27 :   }
     560             : 
     561             :   /// \brief Visit block node
     562             :   /// \return The result of visiting the node
     563             :   /// \param x A process expression
     564             :   /// \param s A sequence of identifiers
     565             :   /// \param right A process expression
     566           0 :   void leave(const process::block& x)
     567             :   {
     568           0 :     throw non_linear_process(x);
     569             :   }
     570             : 
     571             :   /// \brief Visit hide node
     572             :   /// \return The result of visiting the node
     573             :   /// \param x A process expression
     574             :   /// \param s A sequence of identifiers
     575             :   /// \param right A process expression
     576           0 :   void leave(const process::hide& x)
     577             :   {
     578           0 :     throw non_linear_process(x);
     579             :   }
     580             : 
     581             :   /// \brief Visit rename node
     582             :   /// \return The result of visiting the node
     583             :   /// \param x A process expression
     584             :   /// \param r A sequence of rename expressions
     585             :   /// \param right A process expression
     586           0 :   void leave(const process::rename& x)
     587             :   {
     588           0 :     throw non_linear_process(x);
     589             :   }
     590             : 
     591             :   /// \brief Visit comm node
     592             :   /// \return The result of visiting the node
     593             :   /// \param x A process expression
     594             :   /// \param c A sequence of communication expressions
     595             :   /// \param right A process expression
     596           0 :   void leave(const process::comm& x)
     597             :   {
     598           0 :     throw non_linear_process(x);
     599             :   }
     600             : 
     601             :   /// \brief Visit allow node
     602             :   /// \return The result of visiting the node
     603             :   /// \param x A process expression
     604             :   /// \param s A sequence of multi-action names
     605             :   /// \param right A process expression
     606           0 :   void leave(const process::allow& x)
     607             :   {
     608           0 :     throw non_linear_process(x);
     609             :   }
     610             : 
     611             :   /// \brief Visit sync node
     612             :   /// \return The result of visiting the node
     613             :   /// \param x A process expression
     614             :   /// \param left A process expression
     615             :   /// \param right A process expression
     616           2 :   void apply(const process::sync& x)
     617             :   {
     618           2 :     apply(x.left());
     619           2 :     lps::multi_action l = m_multi_action;
     620           2 :     apply(x.right());
     621           2 :     lps::multi_action r = m_multi_action;
     622           2 :     m_multi_action = l + r;
     623           2 :     m_multi_action_changed = true;
     624           2 :     mCRL2log(log::debug) << "adding multi action\n" << m_multi_action << std::endl;
     625           2 :   }
     626             : 
     627             :   /// \brief Visit at node
     628             :   /// \return The result of visiting the node
     629             :   /// \param x A process expression
     630             :   /// \param left A process expression
     631             :   /// \param d A data expression
     632           1 :   void leave(const process::at& x)
     633             :   {
     634           1 :     if (is_delta(x))
     635             :     {
     636           0 :       m_deadlock.time() = x.time_stamp();
     637           0 :       mCRL2log(log::debug) << "adding deadlock\n" << m_deadlock << std::endl;
     638             :     }
     639             :     else
     640             :     {
     641           1 :       m_multi_action=lps::multi_action(m_multi_action.actions(), x.time_stamp());
     642           1 :       mCRL2log(log::debug) << "adding multi action\n" << m_multi_action << std::endl;
     643             :     }
     644           1 :   }
     645             : 
     646             :   /// \brief Visit seq node
     647             :   /// \return The result of visiting the node
     648             :   /// \param x A process expression
     649             :   /// \param left A process expression
     650             :   /// \param right A process expression
     651          77 :   void apply(const process::seq& x)
     652             :   {
     653          77 :     apply(x.left());
     654             : 
     655          77 :     process_expression right = x.right();
     656          77 :     if (is_stochastic_operator(right))
     657             :     {
     658          18 :       auto const& op = atermpp::down_cast<stochastic_operator>(right);
     659          18 :       m_distribution = lps::stochastic_distribution(op.variables(), op.distribution());
     660          18 :       right = op.operand();
     661             :     }
     662             : 
     663             :     // Check 1) The expression right must be a process instance or a process assignment
     664          77 :     if (is_process_instance(right))
     665             :     {
     666          24 :       const process_instance& p = atermpp::down_cast<process_instance>(right);
     667             :       // Check 2) The process equation and and the process instance must match
     668          24 :       if (!detail::check_process_instance(m_equation, p))
     669             :       {
     670           0 :         std::clog << "seq right hand side: " << process::pp(right) << std::endl;
     671           0 :         throw mcrl2::runtime_error("Error in linear_process_conversion_traverser::convert: seq expression encountered that does not match the process equation");
     672             :       }
     673          24 :       m_next_state = data::make_assignment_list(m_equation.formal_parameters(), p.actual_parameters());
     674          24 :       m_next_state_changed = true;
     675             :     }
     676          53 :     else if (is_process_instance_assignment(right))
     677             :     {
     678          53 :       const process_instance_assignment& p = atermpp::down_cast<process_instance_assignment>(right);
     679             :       // Check 2) The process equation and and the process instance assignment must match
     680          53 :       if (!detail::check_process_instance_assignment(m_equation, p))
     681             :       {
     682           0 :         std::clog << "seq right hand side: " << process::pp(right) << std::endl;
     683           0 :         throw mcrl2::runtime_error("Error in linear_process_conversion_traverser::convert: seq expression encountered that does not match the process equation");
     684             :       }
     685          53 :       m_next_state = p.assignments(); // TODO: check if this is correct
     686          53 :       m_next_state_changed = true;
     687             :     }
     688             :     else
     689             :     {
     690           0 :       std::clog << "seq right hand side: " << process::pp(right) << std::endl;
     691           0 :       throw mcrl2::runtime_error("Error in linear_process_conversion_traverser::convert: seq expression encountered with an unexpected right hand side");
     692             :     }
     693             : 
     694          77 :     mCRL2log(log::debug) << "adding next state\n" << data::pp(m_next_state) << std::endl;
     695          77 :   }
     696             : 
     697             :   /// \brief Visit if_then node
     698             :   /// \return The result of visiting the node
     699             :   /// \param x A process expression
     700             :   /// \param d A data expression
     701             :   /// \param right A process expression
     702          63 :   void leave(const process::if_then& x)
     703             :   {
     704          63 :     m_condition = x.condition();
     705          63 :     mCRL2log(log::debug) << "adding condition\n" << data::pp(m_condition) << std::endl;
     706          63 :   }
     707             : 
     708             :   /// \brief Visit if_then_else node
     709             :   /// \return The result of visiting the node
     710             :   /// \param x A process expression
     711             :   /// \param d A data expression
     712             :   /// \param left A process expression
     713             :   /// \param right A process expression
     714           0 :   void leave(const process::if_then_else& x)
     715             :   {
     716           0 :     throw non_linear_process(x);
     717             :   }
     718             : 
     719             :   /// \brief Visit bounded_init node
     720             :   /// \return The result of visiting the node
     721             :   /// \param x A process expression
     722             :   /// \param left A process expression
     723             :   /// \param right A process expression
     724           0 :   void leave(const process::bounded_init& x)
     725             :   {
     726           0 :     throw non_linear_process(x);
     727             :   }
     728             : 
     729             :   /// \brief Visit merge node
     730             :   /// \return The result of visiting the node
     731             :   /// \param x A process expression
     732           0 :   void leave(const process::merge& x)
     733             :   {
     734           0 :     throw non_linear_process(x);
     735             :   }
     736             : 
     737             :   /// \brief Visit left_merge node
     738             :   /// \return The result of visiting the node
     739             :   /// \param x A process expression
     740           0 :   void leave(const process::left_merge& x)
     741             :   {
     742           0 :     throw non_linear_process(x);
     743             :   }
     744             : 
     745             :   /// \brief Visit stochastic operator node
     746             :   /// \param x A process expression
     747           1 :   void leave(const process::stochastic_operator& x)
     748             :   {
     749           1 :     m_distribution = lps::stochastic_distribution(x.variables(), x.distribution());
     750           1 :   }
     751             : 
     752             :   /// \brief Visit choice node
     753             :   /// \return The result of visiting the node
     754             :   /// \param x A process expression
     755          52 :   void apply(const process::choice& x)
     756             :   {
     757          52 :     apply(x.left());
     758          52 :     if (!is_choice(x.left()))
     759             :     {
     760          14 :       add_summand();
     761             :     }
     762          52 :     apply(x.right());
     763          52 :     if (!is_choice(x.right()))
     764             :     {
     765          52 :       add_summand();
     766             :     }
     767          52 :   }
     768             : 
     769             :   /// \brief Returns true if the process equation e is linear.
     770             :   /// \param e A process equation
     771          36 :   void convert(const process_equation& /* e */)
     772             :   {
     773          36 :     clear_summand();
     774          36 :     apply(m_equation.expression());
     775          36 :     add_summand(); // needed if it is not a choice
     776          36 :   }
     777             : 
     778             :   /// \brief Converts a process_specification into a stochastic_specification.
     779             :   /// Throws \p non_linear_process if a non-linear sub-expression is encountered.
     780             :   /// Throws \p mcrl2::runtime_error in the following cases:
     781             :   /// \li The number of equations is not equal to one
     782             :   /// \li The initial process is not a process instance, or it does not match with the equation
     783             :   /// \li A sequential process is found with a right hand side that is not a process instance,
     784             :   /// or it doesn't match the equation
     785             :   /// \param p A process specification
     786             :   /// \return The converted specification
     787          36 :   lps::stochastic_specification convert(const process_specification& p)
     788             :   {
     789          36 :     m_action_summands.clear();
     790          36 :     m_deadlock_summands.clear();
     791             : 
     792             :     // Check 1) The number of equations must be one
     793          36 :     if (p.equations().size() != 1)
     794             :     {
     795           0 :       throw mcrl2::runtime_error("Error in stochastic_linear_process_conversion_traverser::convert: the number of process equations is not equal to 1!");
     796             :     }
     797             : 
     798          36 :     m_equation = p.equations().front();
     799             : 
     800             :     // convert the initial state
     801          36 :     lps::stochastic_process_initializer proc_init;
     802          36 :     process_expression p_init = p.init();
     803          36 :     lps::stochastic_distribution dist;
     804          36 :     if (is_stochastic_operator(p.init()))
     805             :     {
     806           4 :       auto const& s = atermpp::down_cast<stochastic_operator>(p.init());
     807           4 :       dist = lps::stochastic_distribution(s.variables(), s.distribution());
     808           4 :       p_init = s.operand();
     809             :     }
     810          36 :     if (is_process_instance(p_init))
     811             :     {
     812          36 :       const process_instance& init = atermpp::down_cast<process_instance>(p_init);
     813          36 :       if (!check_process_instance(m_equation, init))
     814             :       {
     815           0 :         throw mcrl2::runtime_error("Error in stochastic_linear_process_conversion_traverser::convert: the initial process does not match the process equation");
     816             :       }
     817          36 :       proc_init = lps::stochastic_process_initializer(init.actual_parameters(), dist);
     818             :     }
     819           0 :     else if (is_process_instance_assignment(p.init()))
     820             :     {
     821           0 :       const process_instance_assignment& init = atermpp::down_cast<process_instance_assignment>(p_init);
     822           0 :       if (!check_process_instance_assignment(m_equation, init))
     823             :       {
     824           0 :         throw mcrl2::runtime_error("Error in stochastic_linear_process_conversion_traverser::convert: the initial process does not match the process equation");
     825             :       }
     826           0 :       proc_init = lps::stochastic_process_initializer(data::right_hand_sides(init.assignments()), dist);
     827             :     }
     828             :     else
     829             :     {
     830           0 :       throw mcrl2::runtime_error("Error in stochastic_linear_process_conversion_traverser::convert: the initial process has an unexpected value");
     831             :     }
     832             : 
     833          36 :     convert(m_equation);
     834             : 
     835          36 :     lps::stochastic_linear_process proc(m_equation.formal_parameters(), m_deadlock_summands, m_action_summands);
     836             : 
     837          72 :     return lps::stochastic_specification(p.data(), p.action_labels(), p.global_variables(), proc, proc_init);
     838          36 :   }
     839             : };
     840             : 
     841             : } // namespace detail
     842             : 
     843             : } // namespace process
     844             : 
     845             : } // namespace mcrl2
     846             : 
     847             : #endif // MCRL2_LPS_DETAIL_LINEAR_PROCESS_CONVERSION_TRAVERSER_H