LCOV - code coverage report
Current view: top level - process/source - process.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 73 114 64.0 %
Date: 2019-09-14 00:54:39 Functions: 24 65 36.9 %
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 process.cpp
      10             : /// \brief
      11             : 
      12             : #include <algorithm>
      13             : #include <iostream>
      14             : #include <limits>
      15             : #include <sstream>
      16             : #include "mcrl2/core/parser_utility.h"
      17             : #include "mcrl2/data/parse_impl.h"
      18             : #include "mcrl2/process/alphabet_reduce.h"
      19             : #include "mcrl2/process/detail/alphabet_push_block.h"
      20             : #include "mcrl2/process/detail/pcrl_equation_cache.h"
      21             : #include "mcrl2/process/find.h"
      22             : #include "mcrl2/process/index_traits.h"
      23             : #include "mcrl2/process/normalize_sorts.h"
      24             : #include "mcrl2/process/parse.h"
      25             : #include "mcrl2/process/parse_impl.h"
      26             : #include "mcrl2/process/print.h"
      27             : #include "mcrl2/process/translate_user_notation.h"
      28             : #include "mcrl2/process/remove_equations.h"
      29             : #include "mcrl2/process/traverser.h"
      30             : #include "mcrl2/process/typecheck.h"
      31             : #include "mcrl2/process/utility.h"
      32             : #include "mcrl2/utilities/logger.h"
      33             : #include "mcrl2/utilities/detail/separate_keyword_section.h"
      34             : #include "mcrl2/utilities/text_utility.h"
      35             : 
      36             : 
      37             : namespace mcrl2
      38             : {
      39             : 
      40             : namespace process
      41             : {
      42             : 
      43             : //--- start generated process overloads ---//
      44           0 : std::string pp(const process::action_list& x) { return process::pp< process::action_list >(x); }
      45           0 : std::string pp(const process::action_vector& x) { return process::pp< process::action_vector >(x); }
      46           0 : std::string pp(const process::action_label_list& x) { return process::pp< process::action_label_list >(x); }
      47           0 : std::string pp(const process::action_label_vector& x) { return process::pp< process::action_label_vector >(x); }
      48           0 : std::string pp(const process::process_identifier_list& x) { return process::pp< process::process_identifier_list >(x); }
      49           0 : std::string pp(const process::process_identifier_vector& x) { return process::pp< process::process_identifier_vector >(x); }
      50           0 : std::string pp(const process::process_expression_list& x) { return process::pp< process::process_expression_list >(x); }
      51           0 : std::string pp(const process::process_expression_vector& x) { return process::pp< process::process_expression_vector >(x); }
      52           0 : std::string pp(const process::process_equation_list& x) { return process::pp< process::process_equation_list >(x); }
      53           0 : std::string pp(const process::process_equation_vector& x) { return process::pp< process::process_equation_vector >(x); }
      54         129 : std::string pp(const process::action& x) { return process::pp< process::action >(x); }
      55          18 : std::string pp(const process::action_label& x) { return process::pp< process::action_label >(x); }
      56           1 : std::string pp(const process::action_name_multiset& x) { return process::pp< process::action_name_multiset >(x); }
      57           1 : std::string pp(const process::allow& x) { return process::pp< process::allow >(x); }
      58           0 : std::string pp(const process::at& x) { return process::pp< process::at >(x); }
      59           0 : std::string pp(const process::block& x) { return process::pp< process::block >(x); }
      60           0 : std::string pp(const process::bounded_init& x) { return process::pp< process::bounded_init >(x); }
      61           0 : std::string pp(const process::choice& x) { return process::pp< process::choice >(x); }
      62           0 : std::string pp(const process::comm& x) { return process::pp< process::comm >(x); }
      63           0 : std::string pp(const process::communication_expression& x) { return process::pp< process::communication_expression >(x); }
      64           0 : std::string pp(const process::delta& x) { return process::pp< process::delta >(x); }
      65           0 : std::string pp(const process::hide& x) { return process::pp< process::hide >(x); }
      66           0 : std::string pp(const process::if_then& x) { return process::pp< process::if_then >(x); }
      67           0 : std::string pp(const process::if_then_else& x) { return process::pp< process::if_then_else >(x); }
      68           0 : std::string pp(const process::left_merge& x) { return process::pp< process::left_merge >(x); }
      69           0 : std::string pp(const process::merge& x) { return process::pp< process::merge >(x); }
      70           0 : std::string pp(const process::process_equation& x) { return process::pp< process::process_equation >(x); }
      71          39 : std::string pp(const process::process_expression& x) { return process::pp< process::process_expression >(x); }
      72           0 : std::string pp(const process::process_identifier& x) { return process::pp< process::process_identifier >(x); }
      73           0 : std::string pp(const process::process_instance& x) { return process::pp< process::process_instance >(x); }
      74           0 : std::string pp(const process::process_instance_assignment& x) { return process::pp< process::process_instance_assignment >(x); }
      75           7 : std::string pp(const process::process_specification& x) { return process::pp< process::process_specification >(x); }
      76           0 : std::string pp(const process::rename& x) { return process::pp< process::rename >(x); }
      77           0 : std::string pp(const process::rename_expression& x) { return process::pp< process::rename_expression >(x); }
      78           0 : std::string pp(const process::seq& x) { return process::pp< process::seq >(x); }
      79           0 : std::string pp(const process::stochastic_operator& x) { return process::pp< process::stochastic_operator >(x); }
      80           0 : std::string pp(const process::sum& x) { return process::pp< process::sum >(x); }
      81           0 : std::string pp(const process::sync& x) { return process::pp< process::sync >(x); }
      82           0 : std::string pp(const process::tau& x) { return process::pp< process::tau >(x); }
      83           0 : std::string pp(const process::timed_multi_action& x) { return process::pp< process::timed_multi_action >(x); }
      84           0 : std::string pp(const process::untyped_multi_action& x) { return process::pp< process::untyped_multi_action >(x); }
      85           0 : std::string pp(const process::untyped_process_assignment& x) { return process::pp< process::untyped_process_assignment >(x); }
      86           8 : process::action normalize_sorts(const process::action& x, const data::sort_specification& sortspec) { return process::normalize_sorts< process::action >(x, sortspec); }
      87           6 : 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); }
      88           0 : void normalize_sorts(process::process_equation_vector& x, const data::sort_specification& sortspec) { process::normalize_sorts< process::process_equation_vector >(x, sortspec); }
      89         950 : void normalize_sorts(process::process_specification& x, const data::sort_specification& /* sortspec */) { process::normalize_sorts< process::process_specification >(x, x.data()); }
      90           8 : process::action translate_user_notation(const process::action& x) { return process::translate_user_notation< process::action >(x); }
      91          11 : process::process_expression translate_user_notation(const process::process_expression& x) { return process::translate_user_notation< process::process_expression >(x); }
      92         944 : void translate_user_notation(process::process_specification& x) { process::translate_user_notation< process::process_specification >(x); }
      93           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); }
      94           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); }
      95           1 : std::set<data::sort_expression> find_sort_expressions(const process::process_expression& x) { return process::find_sort_expressions< process::process_expression >(x); }
      96           0 : std::set<data::sort_expression> find_sort_expressions(const process::process_specification& x) { return process::find_sort_expressions< process::process_specification >(x); }
      97           7 : std::set<data::variable> find_all_variables(const process::action& x) { return process::find_all_variables< process::action >(x); }
      98          16 : std::set<data::variable> find_free_variables(const process::action& x) { return process::find_free_variables< process::action >(x); }
      99           0 : std::set<data::variable> find_free_variables(const process::process_specification& x) { return process::find_free_variables< process::process_specification >(x); }
     100        1369 : std::set<core::identifier_string> find_identifiers(const process::process_specification& x) { return process::find_identifiers< process::process_specification >(x); }
     101             : //--- end generated process overloads ---//
     102             : 
     103          94 : static bool register_hooks()
     104             : {
     105          94 :   register_process_identifier_hooks();
     106          94 :   return true;
     107             : }
     108          94 : static bool mcrl2_register_process(register_hooks());
     109             : 
     110         677 : void alphabet_reduce(process_specification& procspec, std::size_t duplicate_equation_limit)
     111             : {
     112         677 :   mCRL2log(log::verbose) << "applying alphabet reduction..." << std::endl;
     113        1354 :   process_expression init = procspec.init();
     114             : 
     115             :   // cache the alphabet of pcrl equations and apply alphabet reduction to block({}, init)
     116         677 :   std::vector<process_equation>& equations = procspec.equations();
     117        1354 :   std::map<process_identifier, multi_action_name_set> pcrl_equation_cache;
     118        1354 :   data::set_identifier_generator id_generator;
     119        1498 :   for (process_equation& equation: equations)
     120             :   {
     121         821 :     id_generator.add_identifier(equation.identifier().name());
     122             :   }
     123         677 :   pcrl_equation_cache = detail::compute_pcrl_equation_cache(equations, init);
     124        1354 :   core::identifier_string_list empty_blockset;
     125         677 :   procspec.init() = push_block(empty_blockset, init, equations, id_generator, pcrl_equation_cache);
     126             : 
     127             :   // remove duplicate equations
     128         677 :   if (procspec.equations().size() < duplicate_equation_limit)
     129             :   {
     130         677 :     mCRL2log(log::debug) << "removing duplicate equations..." << std::endl;
     131         677 :     remove_duplicate_equations(procspec);
     132         677 :     mCRL2log(log::debug) << "removing duplicate equations finished" << std::endl;
     133             :   }
     134             : 
     135         677 :   mCRL2log(log::debug) << "alphabet reduction finished" << std::endl;
     136         677 : }
     137             : 
     138           1 : process::action_label_list parse_action_declaration(const std::string& text, const data::data_specification& data_spec)
     139             : {
     140           2 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     141           1 :   unsigned int start_symbol_index = p.start_symbol_index("ActDecl");
     142           1 :   bool partial_parses = false;
     143           2 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     144           2 :   action_label_vector result;
     145           1 :   detail::action_actions(p).callback_ActDecl(node, result);
     146           1 :   process::action_label_list v(result.begin(), result.end());
     147           1 :   v = process::normalize_sorts(v, data_spec);
     148           2 :   return v;
     149             : }
     150             : 
     151             : namespace detail {
     152             : 
     153           3 : process_expression parse_process_expression_new(const std::string& text)
     154             : {
     155           6 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     156           3 :   unsigned int start_symbol_index = p.start_symbol_index("ProcExpr");
     157           3 :   bool partial_parses = false;
     158           6 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     159           3 :   core::warn_and_or(node);
     160           3 :   core::warn_left_merge_merge(node);
     161           3 :   process_expression result = process_actions(p).parse_ProcExpr(node);
     162           6 :   return result;
     163             : }
     164             : 
     165         960 : process_specification parse_process_specification_new(const std::string& text)
     166             : {
     167        1920 :   core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
     168         960 :   unsigned int start_symbol_index = p.start_symbol_index("mCRL2Spec");
     169         960 :   bool partial_parses = false;
     170        1920 :   core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
     171         960 :   core::warn_and_or(node);
     172         960 :   core::warn_left_merge_merge(node);
     173        1920 :   untyped_process_specification untyped_procspec = process_actions(p).parse_mCRL2Spec(node);
     174         960 :   process_specification result = untyped_procspec.construct_process_specification();
     175        1920 :   return result;
     176             : }
     177             : 
     178         954 : void complete_process_specification(process_specification& x, bool alpha_reduce)
     179             : {
     180         954 :   typecheck_process_specification(x);
     181         944 :   if (alpha_reduce)
     182             :   {
     183         675 :     alphabet_reduce(x, 1000ul);
     184             :   }
     185         944 :   process::translate_user_notation(x);
     186         944 : }
     187             : 
     188             : } // namespace detail
     189             : 
     190             : } // namespace process
     191             : 
     192         282 : } // namespace mcrl2
     193             : 

Generated by: LCOV version 1.12