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 lps.cpp
      10             : /// \brief
      11             : 
      12             : #include "mcrl2/lps/is_well_typed.h"
      13             : #include "mcrl2/lps/normalize_sorts.h"
      14             : #include "mcrl2/lps/parse_impl.h"
      15             : #include "mcrl2/lps/print.h"
      16             : #include "mcrl2/lps/replace.h"
      17             : #include "mcrl2/lps/translate_user_notation.h"
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : 
      22             : namespace lps
      23             : {
      24             : 
      25             : //--- start generated lps overloads ---//
      26           0 : std::string pp(const lps::action_summand& x) { return lps::pp< lps::action_summand >(x); }
      27           4 : std::string pp(const lps::deadlock& x) { return lps::pp< lps::deadlock >(x); }
      28           4 : std::string pp(const lps::deadlock_summand& x) { return lps::pp< lps::deadlock_summand >(x); }
      29           4 : std::string pp(const lps::linear_process& x) { return lps::pp< lps::linear_process >(x); }
      30        1160 : std::string pp(const lps::multi_action& x) { return lps::pp< lps::multi_action >(x); }
      31           0 : std::string pp(const lps::process_initializer& x) { return lps::pp< lps::process_initializer >(x); }
      32          34 : std::string pp(const lps::specification& x) { return lps::pp< lps::specification >(x); }
      33           0 : std::string pp(const lps::stochastic_action_summand& x) { return lps::pp< lps::stochastic_action_summand >(x); }
      34           1 : std::string pp(const lps::stochastic_distribution& x) { return lps::pp< lps::stochastic_distribution >(x); }
      35           0 : std::string pp(const lps::stochastic_linear_process& x) { return lps::pp< lps::stochastic_linear_process >(x); }
      36           0 : std::string pp(const lps::stochastic_process_initializer& x) { return lps::pp< lps::stochastic_process_initializer >(x); }
      37           6 : std::string pp(const lps::stochastic_specification& x) { return lps::pp< lps::stochastic_specification >(x); }
      38          22 : lps::multi_action normalize_sorts(const lps::multi_action& x, const data::sort_specification& sortspec) { return lps::normalize_sorts< lps::multi_action >(x, sortspec); }
      39          16 : void normalize_sorts(lps::specification& x, const data::sort_specification& /* sortspec */) { lps::normalize_sorts< lps::specification >(x, x.data()); }
      40           0 : void normalize_sorts(lps::stochastic_specification& x, const data::sort_specification& /* sortspec */) { lps::normalize_sorts< lps::stochastic_specification >(x, x.data()); }
      41          22 : lps::multi_action translate_user_notation(const lps::multi_action& x) { return lps::translate_user_notation< lps::multi_action >(x); }
      42         274 : std::set<data::sort_expression> find_sort_expressions(const lps::specification& x) { return lps::find_sort_expressions< lps::specification >(x); }
      43        2506 : std::set<data::sort_expression> find_sort_expressions(const lps::stochastic_specification& x) { return lps::find_sort_expressions< lps::stochastic_specification >(x); }
      44           0 : std::set<data::variable> find_all_variables(const lps::linear_process& x) { return lps::find_all_variables< lps::linear_process >(x); }
      45           0 : std::set<data::variable> find_all_variables(const lps::stochastic_linear_process& x) { return lps::find_all_variables< lps::stochastic_linear_process >(x); }
      46         130 : std::set<data::variable> find_all_variables(const lps::specification& x) { return lps::find_all_variables< lps::specification >(x); }
      47           1 : std::set<data::variable> find_all_variables(const lps::stochastic_specification& x) { return lps::find_all_variables< lps::stochastic_specification >(x); }
      48           3 : std::set<data::variable> find_all_variables(const lps::deadlock& x) { return lps::find_all_variables< lps::deadlock >(x); }
      49          27 : std::set<data::variable> find_all_variables(const lps::multi_action& x) { return lps::find_all_variables< lps::multi_action >(x); }
      50          35 : std::set<data::variable> find_free_variables(const lps::linear_process& x) { return lps::find_free_variables< lps::linear_process >(x); }
      51           1 : std::set<data::variable> find_free_variables(const lps::stochastic_linear_process& x) { return lps::find_free_variables< lps::stochastic_linear_process >(x); }
      52          18 : std::set<data::variable> find_free_variables(const lps::specification& x) { return lps::find_free_variables< lps::specification >(x); }
      53         617 : std::set<data::variable> find_free_variables(const lps::stochastic_specification& x) { return lps::find_free_variables< lps::stochastic_specification >(x); }
      54           2 : std::set<data::variable> find_free_variables(const lps::deadlock& x) { return lps::find_free_variables< lps::deadlock >(x); }
      55       14676 : std::set<data::variable> find_free_variables(const lps::multi_action& x) { return lps::find_free_variables< lps::multi_action >(x); }
      56           0 : std::set<data::variable> find_free_variables(const lps::process_initializer& x) { return lps::find_free_variables< lps::process_initializer >(x); }
      57           0 : std::set<data::variable> find_free_variables(const lps::stochastic_process_initializer& x) { return lps::find_free_variables< lps::stochastic_process_initializer >(x); }
      58           0 : std::set<data::function_symbol> find_function_symbols(const lps::specification& x) { return lps::find_function_symbols< lps::specification >(x); }
      59           0 : std::set<data::function_symbol> find_function_symbols(const lps::stochastic_specification& x) { return lps::find_function_symbols< lps::stochastic_specification >(x); }
      60         209 : std::set<core::identifier_string> find_identifiers(const lps::specification& x) { return lps::find_identifiers< lps::specification >(x); }
      61         318 : std::set<core::identifier_string> find_identifiers(const lps::stochastic_specification& x) { return lps::find_identifiers< lps::stochastic_specification >(x); }
      62           0 : std::set<process::action_label> find_action_labels(const lps::linear_process& x) { return lps::find_action_labels< lps::linear_process >(x); }
      63           0 : std::set<process::action_label> find_action_labels(const lps::process_initializer& x) { return lps::find_action_labels< lps::process_initializer >(x); }
      64           0 : std::set<process::action_label> find_action_labels(const lps::specification& x) { return lps::find_action_labels< lps::specification >(x); }
      65           0 : std::set<process::action_label> find_action_labels(const lps::stochastic_specification& x) { return lps::find_action_labels< lps::stochastic_specification >(x); }
      66             : //--- end generated lps overloads ---//
      67             : 
      68        3284 : data::data_expression_list action_summand::next_state(const data::variable_list& process_parameters) const
      69             : {
      70             :   return data::replace_variables(atermpp::container_cast<data::data_expression_list>(process_parameters),
      71        6568 :                                  data::assignment_sequence_substitution(assignments()));
      72             : }
      73             : 
      74           0 : std::string pp_with_summand_numbers(const specification& x)
      75             : {
      76           0 :   std::ostringstream out;
      77           0 :   core::detail::apply_printer<lps::detail::printer> printer(out);
      78           0 :   printer.print_summand_numbers() = true;
      79           0 :   printer.apply(x);
      80           0 :   return out.str();
      81           0 : }
      82             : 
      83           0 : std::string pp_with_summand_numbers(const stochastic_specification& x)
      84             : {
      85           0 :   std::ostringstream out;
      86           0 :   core::detail::apply_printer<lps::detail::printer> printer(out);
      87           0 :   printer.print_summand_numbers() = true;
      88           0 :   printer.apply(x);
      89           0 :   return out.str();
      90           0 : }
      91             : 
      92           0 : bool check_well_typedness(const linear_process& x)
      93             : {
      94           0 :   return lps::detail::check_well_typedness(x);
      95             : }
      96             : 
      97           1 : bool check_well_typedness(const stochastic_linear_process& x)
      98             : {
      99           1 :   return lps::detail::check_well_typedness(x);
     100             : }
     101             : 
     102          17 : bool check_well_typedness(const specification& x)
     103             : {
     104          17 :   return lps::detail::check_well_typedness(x);
     105             : }
     106             : 
     107          10 : bool check_well_typedness(const stochastic_specification& x)
     108             : {
     109          10 :   return lps::detail::check_well_typedness(x);
     110             : }
     111             : 
     112             : namespace detail {
     113             : 
     114          22 : process::untyped_multi_action parse_multi_action_new(const std::string& text)
     115             : {
     116          22 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     117          22 :   unsigned int start_symbol_index = p.start_symbol_index("MultAct");
     118          22 :   bool partial_parses = false;
     119          22 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     120          22 :   process::untyped_multi_action result = multi_action_actions(p).parse_MultAct(node);
     121          44 :   return result;
     122          22 : }
     123             : 
     124          12 : multi_action complete_multi_action(process::untyped_multi_action& x, multi_action_type_checker& typechecker, const data::data_specification& data_spec = data::detail::default_specification())
     125             : {
     126          12 :   multi_action result = lps::typecheck_multi_action(x, typechecker);
     127          12 :   result = lps::translate_user_notation(result);
     128          12 :   lps::normalize_sorts(result, data_spec);
     129          12 :   return result;
     130           0 : }
     131             : 
     132          10 : multi_action complete_multi_action(process::untyped_multi_action& x, const process::action_label_list& action_decls, const data::data_specification& data_spec = data::detail::default_specification())
     133             : {
     134          10 :   multi_action result = lps::typecheck_multi_action(x, data_spec, action_decls);
     135          10 :   result = lps::translate_user_notation(result);
     136          10 :   lps::normalize_sorts(result, data_spec);
     137          10 :   return result;
     138           0 : }
     139             : 
     140           6 : action_rename_specification parse_action_rename_specification_new(const std::string& text)
     141             : {
     142           6 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     143           6 :   unsigned int start_symbol_index = p.start_symbol_index("ActionRenameSpec");
     144           6 :   bool partial_parses = false;
     145           6 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     146           6 :   action_rename_specification result = action_rename_actions(p).parse_ActionRenameSpec(node);
     147          12 :   return result;
     148           6 : }
     149             : 
     150           6 : void complete_action_rename_specification(action_rename_specification& x, const lps::stochastic_specification& spec)
     151             : {
     152             :   using namespace mcrl2::data;
     153           6 :   x = lps::typecheck_action_rename_specification(x, spec);
     154           6 :   x = action_rename_specification(x.data() + spec.data(), x.action_labels(), x.rules());
     155           6 :   detail::translate_user_notation(x);
     156           6 : }
     157             : 
     158             : } // namespace detail
     159             : 
     160             : } // namespace lps
     161             : 
     162             : } // namespace mcrl2