LCOV - code coverage report
Current view: top level - lps/source - lps.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 59 91 64.8 %
Date: 2020-02-28 00:44:21 Functions: 35 52 67.3 %
Legend: Lines: hit not hit

          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           0 : std::string pp(const lps::deadlock& x) { return lps::pp< lps::deadlock >(x); }
      28           0 : 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        1908 : 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           5 : std::string pp(const lps::stochastic_specification& x) { return lps::pp< lps::stochastic_specification >(x); }
      38           7 : void normalize_sorts(lps::multi_action& x, const data::sort_specification& sortspec) { 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           7 : void translate_user_notation(lps::multi_action& x) { lps::translate_user_notation< lps::multi_action >(x); }
      41         269 : std::set<data::sort_expression> find_sort_expressions(const lps::specification& x) { return lps::find_sort_expressions< lps::specification >(x); }
      42        2129 : std::set<data::sort_expression> find_sort_expressions(const lps::stochastic_specification& x) { return lps::find_sort_expressions< lps::stochastic_specification >(x); }
      43           0 : std::set<data::variable> find_all_variables(const lps::linear_process& x) { return lps::find_all_variables< lps::linear_process >(x); }
      44           0 : std::set<data::variable> find_all_variables(const lps::stochastic_linear_process& x) { return lps::find_all_variables< lps::stochastic_linear_process >(x); }
      45         130 : std::set<data::variable> find_all_variables(const lps::specification& x) { return lps::find_all_variables< lps::specification >(x); }
      46           1 : std::set<data::variable> find_all_variables(const lps::stochastic_specification& x) { return lps::find_all_variables< lps::stochastic_specification >(x); }
      47           3 : std::set<data::variable> find_all_variables(const lps::deadlock& x) { return lps::find_all_variables< lps::deadlock >(x); }
      48          27 : std::set<data::variable> find_all_variables(const lps::multi_action& x) { return lps::find_all_variables< lps::multi_action >(x); }
      49          35 : std::set<data::variable> find_free_variables(const lps::linear_process& x) { return lps::find_free_variables< lps::linear_process >(x); }
      50           1 : std::set<data::variable> find_free_variables(const lps::stochastic_linear_process& x) { return lps::find_free_variables< lps::stochastic_linear_process >(x); }
      51          26 : std::set<data::variable> find_free_variables(const lps::specification& x) { return lps::find_free_variables< lps::specification >(x); }
      52          10 : std::set<data::variable> find_free_variables(const lps::stochastic_specification& x) { return lps::find_free_variables< lps::stochastic_specification >(x); }
      53           2 : std::set<data::variable> find_free_variables(const lps::deadlock& x) { return lps::find_free_variables< lps::deadlock >(x); }
      54        2145 : std::set<data::variable> find_free_variables(const lps::multi_action& x) { return lps::find_free_variables< lps::multi_action >(x); }
      55           0 : std::set<data::variable> find_free_variables(const lps::process_initializer& x) { return lps::find_free_variables< lps::process_initializer >(x); }
      56           0 : std::set<data::variable> find_free_variables(const lps::stochastic_process_initializer& x) { return lps::find_free_variables< lps::stochastic_process_initializer >(x); }
      57           5 : std::set<data::function_symbol> find_function_symbols(const lps::specification& x) { return lps::find_function_symbols< lps::specification >(x); }
      58         181 : std::set<data::function_symbol> find_function_symbols(const lps::stochastic_specification& x) { return lps::find_function_symbols< lps::stochastic_specification >(x); }
      59         463 : std::set<core::identifier_string> find_identifiers(const lps::specification& x) { return lps::find_identifiers< lps::specification >(x); }
      60         199 : std::set<core::identifier_string> find_identifiers(const lps::stochastic_specification& x) { return lps::find_identifiers< lps::stochastic_specification >(x); }
      61         167 : std::set<process::action_label> find_action_labels(const lps::linear_process& x) { return lps::find_action_labels< lps::linear_process >(x); }
      62           0 : std::set<process::action_label> find_action_labels(const lps::process_initializer& x) { return lps::find_action_labels< lps::process_initializer >(x); }
      63           0 : std::set<process::action_label> find_action_labels(const lps::specification& x) { return lps::find_action_labels< lps::specification >(x); }
      64             : //--- end generated lps overloads ---//
      65             : 
      66        3691 : data::data_expression_list action_summand::next_state(const data::variable_list& process_parameters) const
      67             : {
      68             :   return data::replace_variables(atermpp::container_cast<data::data_expression_list>(process_parameters),
      69        3691 :                                  data::assignment_sequence_substitution(assignments()));
      70             : }
      71             : 
      72           0 : std::string pp_with_summand_numbers(const specification& x)
      73             : {
      74           0 :   std::ostringstream out;
      75           0 :   core::detail::apply_printer<lps::detail::printer> printer(out);
      76           0 :   printer.print_summand_numbers() = true;
      77           0 :   printer.apply(x);
      78           0 :   return out.str();
      79             : }
      80             : 
      81           0 : std::string pp_with_summand_numbers(const stochastic_specification& x)
      82             : {
      83           0 :   std::ostringstream out;
      84           0 :   core::detail::apply_printer<lps::detail::printer> printer(out);
      85           0 :   printer.print_summand_numbers() = true;
      86           0 :   printer.apply(x);
      87           0 :   return out.str();
      88             : }
      89             : 
      90           0 : bool check_well_typedness(const linear_process& x)
      91             : {
      92           0 :   return lps::detail::check_well_typedness(x);
      93             : }
      94             : 
      95           1 : bool check_well_typedness(const stochastic_linear_process& x)
      96             : {
      97           1 :   return lps::detail::check_well_typedness(x);
      98             : }
      99             : 
     100          25 : bool check_well_typedness(const specification& x)
     101             : {
     102          25 :   return lps::detail::check_well_typedness(x);
     103             : }
     104             : 
     105           4 : bool check_well_typedness(const stochastic_specification& x)
     106             : {
     107           4 :   return lps::detail::check_well_typedness(x);
     108             : }
     109             : 
     110             : namespace detail {
     111             : 
     112           7 : process::untyped_multi_action parse_multi_action_new(const std::string& text)
     113             : {
     114          14 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     115           7 :   unsigned int start_symbol_index = p.start_symbol_index("MultAct");
     116           7 :   bool partial_parses = false;
     117          14 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     118           7 :   process::untyped_multi_action result = multi_action_actions(p).parse_MultAct(node);
     119          14 :   return result;
     120             : }
     121             : 
     122           0 : 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())
     123             : {
     124           0 :   multi_action result = lps::typecheck_multi_action(x, typechecker);
     125           0 :   lps::translate_user_notation(result);
     126           0 :   lps::normalize_sorts(result, data_spec);
     127           0 :   return result;
     128             : }
     129             : 
     130           7 : 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())
     131             : {
     132           7 :   multi_action result = lps::typecheck_multi_action(x, data_spec, action_decls);
     133           7 :   lps::translate_user_notation(result);
     134           7 :   lps::normalize_sorts(result, data_spec);
     135           7 :   return result;
     136             : }
     137             : 
     138           5 : action_rename_specification parse_action_rename_specification_new(const std::string& text)
     139             : {
     140          10 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     141           5 :   unsigned int start_symbol_index = p.start_symbol_index("ActionRenameSpec");
     142           5 :   bool partial_parses = false;
     143          10 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     144           5 :   action_rename_specification result = action_rename_actions(p).parse_ActionRenameSpec(node);
     145          10 :   return result;
     146             : }
     147             : 
     148           5 : void complete_action_rename_specification(action_rename_specification& x, const lps::stochastic_specification& spec)
     149             : {
     150             :   using namespace mcrl2::data;
     151           5 :   x = lps::typecheck_action_rename_specification(x, spec);
     152           5 :   x.data().declare_data_specification_to_be_type_checked();
     153           5 :   x = action_rename_specification(x.data() + spec.data(), x.action_labels(), x.rules());
     154           5 :   detail::translate_user_notation(x);
     155           5 : }
     156             : 
     157             : } // namespace detail
     158             : 
     159             : } // namespace lps
     160             : 
     161         261 : } // namespace mcrl2

Generated by: LCOV version 1.13