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 process.cpp
      10             : /// \brief
      11             : 
      12             : #include "mcrl2/process/detail/alphabet_push_block.h"
      13             : #include "mcrl2/process/parse_impl.h"
      14             : #include "mcrl2/process/translate_user_notation.h"
      15             : #include "mcrl2/process/remove_equations.h"
      16             : 
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace process
      22             : {
      23             : 
      24             : //--- start generated process overloads ---//
      25           0 : std::string pp(const process::action_list& x) { return process::pp< process::action_list >(x); }
      26           0 : std::string pp(const process::action_vector& x) { return process::pp< process::action_vector >(x); }
      27           0 : std::string pp(const process::action_label_list& x) { return process::pp< process::action_label_list >(x); }
      28           0 : std::string pp(const process::action_label_vector& x) { return process::pp< process::action_label_vector >(x); }
      29           0 : std::string pp(const process::process_identifier_list& x) { return process::pp< process::process_identifier_list >(x); }
      30           0 : std::string pp(const process::process_identifier_vector& x) { return process::pp< process::process_identifier_vector >(x); }
      31           0 : std::string pp(const process::process_expression_list& x) { return process::pp< process::process_expression_list >(x); }
      32           0 : std::string pp(const process::process_expression_vector& x) { return process::pp< process::process_expression_vector >(x); }
      33           0 : std::string pp(const process::process_equation_list& x) { return process::pp< process::process_equation_list >(x); }
      34           0 : std::string pp(const process::process_equation_vector& x) { return process::pp< process::process_equation_vector >(x); }
      35         161 : std::string pp(const process::action& x) { return process::pp< process::action >(x); }
      36           0 : std::string pp(const process::action_label& x) { return process::pp< process::action_label >(x); }
      37           1 : std::string pp(const process::action_name_multiset& x) { return process::pp< process::action_name_multiset >(x); }
      38           1 : std::string pp(const process::allow& x) { return process::pp< process::allow >(x); }
      39           0 : std::string pp(const process::at& x) { return process::pp< process::at >(x); }
      40           0 : std::string pp(const process::block& x) { return process::pp< process::block >(x); }
      41           0 : std::string pp(const process::bounded_init& x) { return process::pp< process::bounded_init >(x); }
      42           0 : std::string pp(const process::choice& x) { return process::pp< process::choice >(x); }
      43           0 : std::string pp(const process::comm& x) { return process::pp< process::comm >(x); }
      44           0 : std::string pp(const process::communication_expression& x) { return process::pp< process::communication_expression >(x); }
      45           0 : std::string pp(const process::delta& x) { return process::pp< process::delta >(x); }
      46           0 : std::string pp(const process::hide& x) { return process::pp< process::hide >(x); }
      47           0 : std::string pp(const process::if_then& x) { return process::pp< process::if_then >(x); }
      48           0 : std::string pp(const process::if_then_else& x) { return process::pp< process::if_then_else >(x); }
      49           0 : std::string pp(const process::left_merge& x) { return process::pp< process::left_merge >(x); }
      50           0 : std::string pp(const process::merge& x) { return process::pp< process::merge >(x); }
      51           0 : std::string pp(const process::process_equation& x) { return process::pp< process::process_equation >(x); }
      52          45 : std::string pp(const process::process_expression& x) { return process::pp< process::process_expression >(x); }
      53           7 : std::string pp(const process::process_identifier& x) { return process::pp< process::process_identifier >(x); }
      54           0 : std::string pp(const process::process_instance& x) { return process::pp< process::process_instance >(x); }
      55           0 : std::string pp(const process::process_instance_assignment& x) { return process::pp< process::process_instance_assignment >(x); }
      56           7 : std::string pp(const process::process_specification& x) { return process::pp< process::process_specification >(x); }
      57           0 : std::string pp(const process::rename& x) { return process::pp< process::rename >(x); }
      58           0 : std::string pp(const process::rename_expression& x) { return process::pp< process::rename_expression >(x); }
      59           0 : std::string pp(const process::seq& x) { return process::pp< process::seq >(x); }
      60           0 : std::string pp(const process::stochastic_operator& x) { return process::pp< process::stochastic_operator >(x); }
      61           0 : std::string pp(const process::sum& x) { return process::pp< process::sum >(x); }
      62           0 : std::string pp(const process::sync& x) { return process::pp< process::sync >(x); }
      63           0 : std::string pp(const process::tau& x) { return process::pp< process::tau >(x); }
      64           0 : std::string pp(const process::untyped_multi_action& x) { return process::pp< process::untyped_multi_action >(x); }
      65           0 : std::string pp(const process::untyped_process_assignment& x) { return process::pp< process::untyped_process_assignment >(x); }
      66          10 : process::action normalize_sorts(const process::action& x, const data::sort_specification& sortspec) { return process::normalize_sorts< process::action >(x, sortspec); }
      67          10 : process::action_label_list normalize_sorts(const process::action_label_list& x, const data::sort_specification& sortspec) { return process::normalize_sorts< process::action_label_list >(x, sortspec); }
      68           0 : void normalize_sorts(process::process_equation_vector& x, const data::sort_specification& sortspec) { process::normalize_sorts< process::process_equation_vector >(x, sortspec); }
      69        1136 : void normalize_sorts(process::process_specification& x, const data::sort_specification& /* sortspec */) { process::normalize_sorts< process::process_specification >(x, x.data()); }
      70          10 : process::action translate_user_notation(const process::action& x) { return process::translate_user_notation< process::action >(x); }
      71          13 : process::process_expression translate_user_notation(const process::process_expression& x) { return process::translate_user_notation< process::process_expression >(x); }
      72        1129 : void translate_user_notation(process::process_specification& x) { process::translate_user_notation< process::process_specification >(x); }
      73           0 : std::set<data::sort_expression> find_sort_expressions(const process::action_label_list& x) { return process::find_sort_expressions< process::action_label_list >(x); }
      74           0 : std::set<data::sort_expression> find_sort_expressions(const process::process_equation_vector& x) { return process::find_sort_expressions< process::process_equation_vector >(x); }
      75           1 : std::set<data::sort_expression> find_sort_expressions(const process::process_expression& x) { return process::find_sort_expressions< process::process_expression >(x); }
      76           0 : std::set<data::sort_expression> find_sort_expressions(const process::process_specification& x) { return process::find_sort_expressions< process::process_specification >(x); }
      77          10 : std::set<data::variable> find_all_variables(const process::action& x) { return process::find_all_variables< process::action >(x); }
      78          20 : std::set<data::variable> find_free_variables(const process::action& x) { return process::find_free_variables< process::action >(x); }
      79           0 : std::set<data::variable> find_free_variables(const process::process_specification& x) { return process::find_free_variables< process::process_specification >(x); }
      80         877 : std::set<core::identifier_string> find_identifiers(const process::process_specification& x) { return process::find_identifiers< process::process_specification >(x); }
      81             : //--- end generated process overloads ---//
      82             : 
      83           2 : void alphabet_reduce(process_specification& procspec, std::size_t duplicate_equation_limit)
      84             : {
      85           2 :   mCRL2log(log::verbose) << "applying alphabet reduction..." << std::endl;
      86           2 :   process_expression init = procspec.init();
      87             : 
      88             :   // cache the alphabet of pcrl equations and apply alphabet reduction to block({}, init)
      89           2 :   std::vector<process_equation>& equations = procspec.equations();
      90           2 :   std::map<process_identifier, multi_action_name_set> pcrl_equation_cache;
      91           2 :   data::set_identifier_generator id_generator;
      92           4 :   for (process_equation& equation: equations)
      93             :   {
      94           2 :     id_generator.add_identifier(equation.identifier().name());
      95             :   }
      96           2 :   pcrl_equation_cache = detail::compute_pcrl_equation_cache(equations, init);
      97           2 :   core::identifier_string_list empty_blockset;
      98           2 :   procspec.init() = push_block(empty_blockset, init, equations, id_generator, pcrl_equation_cache);
      99             : 
     100             :   // remove duplicate equations
     101           2 :   if (procspec.equations().size() < duplicate_equation_limit)
     102             :   {
     103           2 :     mCRL2log(log::debug) << "removing duplicate equations..." << std::endl;
     104           2 :     remove_duplicate_equations(procspec);
     105           2 :     mCRL2log(log::debug) << "removing duplicate equations finished" << std::endl;
     106             :   }
     107             : 
     108           2 :   mCRL2log(log::debug) << "alphabet reduction finished" << std::endl;
     109           2 : }
     110             : 
     111           4 : process::action_label_list parse_action_declaration(const std::string& text, const data::data_specification& data_spec)
     112             : {
     113           4 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     114           4 :   unsigned int start_symbol_index = p.start_symbol_index("ActDecl");
     115           4 :   bool partial_parses = false;
     116           4 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     117           4 :   action_label_vector result;
     118           4 :   detail::action_actions(p).callback_ActDecl(node, result);
     119           4 :   process::action_label_list v(result.begin(), result.end());
     120           4 :   v = process::normalize_sorts(v, data_spec);
     121           8 :   return v;
     122           4 : }
     123             : 
     124             : namespace detail {
     125             : 
     126           3 : process_expression parse_process_expression_new(const std::string& text)
     127             : {
     128           3 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     129           3 :   unsigned int start_symbol_index = p.start_symbol_index("ProcExpr");
     130           3 :   bool partial_parses = false;
     131           3 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     132           3 :   core::warn_and_or(node);
     133           3 :   core::warn_left_merge_merge(node);
     134           3 :   process_expression result = process_actions(p).parse_ProcExpr(node);
     135           6 :   return result;
     136           3 : }
     137             : 
     138        1153 : process_specification parse_process_specification_new(const std::string& text)
     139             : {
     140        1153 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     141        1153 :   unsigned int start_symbol_index = p.start_symbol_index("mCRL2Spec");
     142        1153 :   bool partial_parses = false;
     143        1153 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     144        1152 :   core::warn_and_or(node);
     145        1152 :   core::warn_left_merge_merge(node);
     146        1152 :   untyped_process_specification untyped_procspec = process_actions(p).parse_mCRL2Spec(node);
     147        1152 :   process_specification result = untyped_procspec.construct_process_specification();
     148        2304 :   return result;
     149        1153 : }
     150             : 
     151        1146 : void complete_process_specification(process_specification& x, bool alpha_reduce)
     152             : {
     153        1146 :   typecheck_process_specification(x);
     154        1129 :   process::translate_user_notation(x);
     155        1129 :   if (alpha_reduce)
     156             :   {
     157           0 :     alphabet_reduce(x, 1000ul);
     158             :   }
     159        1129 : }
     160             : 
     161             : } // namespace detail
     162             : 
     163             : } // namespace process
     164             : 
     165             : } // namespace mcrl2
     166             :