LCOV - code coverage report
Current view: top level - lps/include/mcrl2/lps/detail - instantiate_global_variables.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 16 17 94.1 %
Date: 2020-02-19 00:44:21 Functions: 4 4 100.0 %
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/lps/detail/instantiate_global_variables.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_DETAIL_INSTANTIATE_GLOBAL_VARIABLES_H
      13             : #define MCRL2_LPS_DETAIL_INSTANTIATE_GLOBAL_VARIABLES_H
      14             : 
      15             : #include "mcrl2/data/representative_generator.h"
      16             : #include "mcrl2/lps/remove.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace lps
      22             : {
      23             : 
      24             : namespace detail
      25             : {
      26             : 
      27             : /// \brief Applies a global variable substitution to an LPS.
      28             : template <typename Specification>
      29         350 : void replace_global_variables(Specification& lpsspec, const data::mutable_map_substitution<>& sigma)
      30             : {
      31         350 :   lps::replace_free_variables(lpsspec.process(), sigma);
      32         350 :   lpsspec.initial_process() = lps::replace_free_variables(lpsspec.initial_process(), sigma);
      33         350 :   lpsspec.global_variables().clear();
      34         350 : }
      35             : 
      36             : /// \brief Eliminates the global variables of an LPS, by substituting
      37             : /// a constant value for them. If no constant value is found for one of the variables,
      38             : /// an exception is thrown.
      39             : template <typename Specification>
      40         350 : data::mutable_map_substitution<> instantiate_global_variables(Specification& lpsspec)
      41             : {
      42         350 :   data::mutable_map_substitution<> sigma;
      43             : 
      44         350 :   mCRL2log(log::verbose) << "Replacing global variables with dummy values." << std::endl;
      45         700 :   data::representative_generator default_expression_generator(lpsspec.data());
      46        1130 :   for (const data::variable& v : lpsspec.global_variables())
      47             :   {
      48        1560 :     data::data_expression d = default_expression_generator(v.sort());
      49         780 :     if (!d.defined())
      50             :     {
      51           0 :       throw mcrl2::runtime_error("Error in lps::instantiate_global_variables: could not instantiate " + data::pp(v) + ". ");
      52             :     }
      53         780 :     sigma[v] = d;
      54             :   }
      55             : 
      56         350 :   mCRL2log(log::debug) << "instantiating global LPS variables " << sigma << std::endl;
      57         350 :   replace_global_variables(lpsspec, sigma);
      58             : 
      59         700 :   return sigma;
      60             : }
      61             : 
      62             : } // namespace detail
      63             : 
      64             : } // namespace lps
      65             : 
      66             : } // namespace mcrl2
      67             : 
      68             : #endif // MCRL2_LPS_DETAIL_INSTANTIATE_GLOBAL_VARIABLES_H

Generated by: LCOV version 1.13