LCOV - code coverage report
Current view: top level - process/include/mcrl2/process/detail - process_context.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 50 73 68.5 %
Date: 2024-03-08 02:52:28 Functions: 9 11 81.8 %
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 mcrl2/process/detail/process_context.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_DETAIL_PROCESS_CONTEXT_H
      13             : #define MCRL2_PROCESS_DETAIL_PROCESS_CONTEXT_H
      14             : 
      15             : #include "mcrl2/data/detail/data_utility.h"
      16             : #include "mcrl2/process/detail/action_context.h"
      17             : #include "mcrl2/process/process_expression.h"
      18             : 
      19             : namespace mcrl2 {
      20             : 
      21             : namespace process {
      22             : 
      23             : namespace detail {
      24             : 
      25             : class process_context
      26             : {
      27             :   private:
      28             :     std::multimap<core::identifier_string, process_identifier> m_process_identifiers;
      29             : 
      30             :     // returns true if all left hand sides of assignments appear as the name of a variable in parameters
      31         441 :     bool is_matching_assignment(const data::untyped_identifier_assignment_list& assignments, const data::variable_list& parameters) const
      32             :     {
      33        1404 :       for (const data::untyped_identifier_assignment& a: assignments)
      34             :       {
      35        5217 :         if (std::find_if(parameters.begin(), parameters.end(), [&](const data::variable& v) { return a.lhs() == v.name(); }) == parameters.end())
      36             :         {
      37           0 :           return false;
      38             :         }
      39             :       }
      40         441 :       return true;
      41             :     }
      42             : 
      43             :     // returns an assignment that does not match with the list of parameters
      44           0 :     data::untyped_identifier_assignment find_violating_assignment(const data::untyped_identifier_assignment_list& assignments, const data::variable_list& parameters) const
      45             :     {
      46             :       using utilities::detail::contains;
      47           0 :       std::set<core::identifier_string> parameter_names;
      48           0 :       for (const data::variable& param: parameters)
      49             :       {
      50           0 :         parameter_names.insert(param.name());
      51             :       }
      52           0 :       auto i = std::find_if(assignments.begin(), assignments.end(), [&](const data::untyped_identifier_assignment& a) { return !contains(parameter_names, a.lhs()); });
      53           0 :       assert(i != assignments.end());
      54           0 :       return *i;
      55           0 :     }
      56             : 
      57             :   public:
      58        2562 :     bool is_declared(const core::identifier_string& name) const
      59             :     {
      60        2562 :       return m_process_identifiers.find(name) != m_process_identifiers.end();
      61             :     }
      62             : 
      63             :     template <typename ProcessIdentifierContainer>
      64        1148 :     void add_process_identifiers(const ProcessIdentifierContainer& ids, const action_context& action_ctx, const data::sort_type_checker& sort_typechecker)
      65             :     {
      66        2304 :       for (const process_identifier& id: ids)
      67             :       {
      68        1146 :         const core::identifier_string& name = id.name();
      69             : 
      70        1146 :         if (action_ctx.is_declared(name))
      71             :         {
      72           0 :           throw mcrl2::runtime_error("declaration of both process and action " + core::pp(name));
      73             :         }
      74             : 
      75             :         // Insert id in m_process_identifiers; N.B. Before that check if it already exists
      76        1146 :         auto range = m_process_identifiers.equal_range(id.name());
      77        1146 :         if (range.first != m_process_identifiers.end())
      78             :         {
      79          81 :           for (auto i = range.first; i != range.second; ++i)
      80             :           {
      81          12 :             if (i->second == id)
      82             :             {
      83           0 :               throw mcrl2::runtime_error("double declaration of process " + process::pp(id));
      84             :             }
      85             :           }
      86             :         }
      87        1146 :         m_process_identifiers.insert(range.first, std::make_pair(id.name(), id));
      88             : 
      89        3257 :         for (const data::variable& v: id.variables())
      90             :         {
      91         965 :           sort_typechecker(v.sort());
      92             :         }
      93             : 
      94             :         //check that all formal parameters of the process are unique.
      95        1146 :         if (!data::detail::unique_names(id.variables()))
      96             :         {
      97           0 :           throw mcrl2::runtime_error("the formal variables in process " + process::pp(id) + " are not unique");
      98             :         }
      99             :       }
     100        1148 :     }
     101             : 
     102             :     // returns the process identifier that corresponds to the untyped process assignment x
     103         441 :     process_identifier match_untyped_process_instance_assignment(const untyped_process_assignment& x) const
     104             :     {
     105         441 :       auto range = m_process_identifiers.equal_range(x.name());
     106         441 :       if (range.first == m_process_identifiers.end())
     107             :       {
     108           0 :         throw mcrl2::runtime_error("process " + core::pp(x.name()) + " not declared");
     109             :       }
     110         441 :       std::vector<process_identifier> result;
     111         882 :       for (auto k = range.first; k != range.second; ++k)
     112             :       {
     113         441 :         const process_identifier& id = k->second;
     114         441 :         if (is_matching_assignment(x.assignments(), id.variables()))
     115             :         {
     116         441 :           result.push_back(id);
     117             :         }
     118             :       }
     119         441 :       if (result.empty())
     120             :       {
     121           0 :         std::string detailed_message;
     122             : 
     123             :         // If there is only one matching process, give a more detailed error message.
     124           0 :         if (std::distance(range.first, range.second) == 1)
     125             :         {
     126           0 :           const process_identifier& id = range.first->second;
     127           0 :           const data::untyped_identifier_assignment& a = find_violating_assignment(x.assignments(), id.variables());
     128           0 :           detailed_message = "Missing parameter: " + core::pp(a.lhs()) + '\n';
     129           0 :         }
     130           0 :         throw mcrl2::runtime_error("There is no process " + core::pp(x.name()) + " containing all assignments in " + process::pp(x) + ".\n" + detailed_message);
     131           0 :       }
     132         441 :       if (result.size() > 1)
     133             :       {
     134           0 :         throw mcrl2::runtime_error("There are multiple processes named " + core::pp(x.name()) + " containing all assignments in " + process::pp(x) + ".");
     135             :       }
     136         882 :       return result.front();
     137         441 :     }
     138             : 
     139        2121 :     process_instance make_process_instance(const core::identifier_string& name, const data::sort_expression_list& formal_parameters, const data::data_expression_list& actual_parameters) const
     140             :     {
     141        2121 :       auto range = m_process_identifiers.equal_range(name);
     142        2121 :       assert(range.first != m_process_identifiers.end());
     143        2145 :       for (auto k = range.first; k != range.second; ++k)
     144             :       {
     145        2145 :         const process_identifier& id = k->second;
     146        2145 :         if (data::detail::parameter_sorts(id.variables()) == formal_parameters)
     147             :         {
     148        4242 :           return process_instance(id, actual_parameters);
     149             :         }
     150             :       }
     151           0 :       throw mcrl2::runtime_error("no matching process found for " + core::pp(name) + "(" + data::pp(formal_parameters) + ")");
     152             :     }
     153             : 
     154        2121 :     data::sorts_list matching_process_sorts(const core::identifier_string& name, const data::data_expression_list& parameters) const
     155             :     {
     156        2121 :       data::sorts_list result;
     157        2121 :       auto range = m_process_identifiers.equal_range(name);
     158        4278 :       for (auto k = range.first; k != range.second; ++k)
     159             :       {
     160        2157 :         const process_identifier& id = k->second;
     161        2157 :         if (id.variables().size() == parameters.size())
     162             :         {
     163        2121 :           result.push_front(data::detail::parameter_sorts(id.variables()));
     164             :         }
     165             :       }
     166        4242 :       return atermpp::reverse(result);
     167        2121 :     }
     168             : 
     169        1135 :     void clear()
     170             :     {
     171        1135 :       m_process_identifiers.clear();
     172        1135 :     }
     173             : };
     174             : 
     175             : } // namespace detail
     176             : 
     177             : } // namespace process
     178             : 
     179             : } // namespace mcrl2
     180             : 
     181             : #endif // MCRL2_PROCESS_DETAIL_PROCESS_CONTEXT_H

Generated by: LCOV version 1.14