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         203 : void replace_global_variables(Specification& lpsspec, const data::mutable_map_substitution<>& sigma)
      30             : {
      31         203 :   lps::replace_free_variables(lpsspec.process(), sigma);
      32         203 :   lpsspec.initial_process() = lps::replace_free_variables(lpsspec.initial_process(), sigma);
      33         203 :   lpsspec.global_variables().clear();
      34         203 : }
      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         203 : data::mutable_map_substitution<> instantiate_global_variables(Specification& lpsspec)
      41             : {
      42         203 :   data::mutable_map_substitution<> sigma;
      43             : 
      44         203 :   mCRL2log(log::verbose) << "Replacing global variables with dummy values." << std::endl;
      45         203 :   data::representative_generator default_expression_generator(lpsspec.data());
      46         699 :   for (const data::variable& v : lpsspec.global_variables())
      47             :   {
      48         496 :     data::data_expression d = default_expression_generator(v.sort());
      49         496 :     if (!d.defined())
      50             :     {
      51           0 :       throw mcrl2::runtime_error("Error in lps::instantiate_global_variables: could not instantiate " + data::pp(v) + ". ");
      52             :     }
      53         496 :     sigma[v] = d;
      54             :   }
      55             : 
      56         203 :   mCRL2log(log::debug) << "instantiating global LPS variables " << sigma << std::endl;
      57         203 :   replace_global_variables(lpsspec, sigma);
      58             : 
      59         406 :   return sigma;
      60         203 : }
      61             : 
      62             : } // namespace detail
      63             : 
      64             : } // namespace lps
      65             : 
      66             : } // namespace mcrl2
      67             : 
      68             : #endif // MCRL2_LPS_DETAIL_INSTANTIATE_GLOBAL_VARIABLES_H