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/pbes/detail/instantiate_global_variables.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_DETAIL_INSTANTIATE_GLOBAL_VARIABLES_H
      13             : #define MCRL2_PBES_DETAIL_INSTANTIATE_GLOBAL_VARIABLES_H
      14             : 
      15             : #include "mcrl2/data/representative_generator.h"
      16             : #include "mcrl2/pbes/replace.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace pbes_system
      22             : {
      23             : 
      24             : namespace detail
      25             : {
      26             : 
      27             : /// \brief Applies a global variable substitution to a PBES.
      28             : inline
      29           4 : void replace_global_variables(pbes& p, const data::mutable_map_substitution<>& sigma)
      30             : {
      31           4 :   pbes_system::replace_free_variables(p.equations(), sigma);
      32           4 :   p.initial_state() = pbes_system::replace_free_variables(p.initial_state(), sigma);
      33           4 :   p.global_variables().clear();
      34           4 : }
      35             : 
      36             : /// \brief Eliminates the global variables of a PBES, 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             : inline
      40         182 : data::mutable_map_substitution<> instantiate_global_variables(pbes& p)
      41             : {
      42         182 :   data::mutable_map_substitution<> sigma;
      43             : 
      44         182 :   if (p.global_variables().empty())
      45             :   {
      46         178 :     return sigma;
      47             :   }
      48             : 
      49           4 :   data::representative_generator default_expression_generator(p.data());
      50           4 :   std::set<data::variable> to_be_removed;
      51          45 :   for (const data::variable& v: p.global_variables())
      52             :   {
      53          41 :     data::data_expression d = default_expression_generator(v.sort());
      54          41 :     if (!d.defined())
      55             :     {
      56           0 :       throw mcrl2::runtime_error("Error in pbes::instantiate_global_variables: could not instantiate " + data::pp(v));
      57             :     }
      58          41 :     sigma[v] = d;
      59          41 :     to_be_removed.insert(v);
      60          41 :   }
      61             : 
      62           4 :   mCRL2log(log::debug) << "instantiating global PBES variables " << sigma << std::endl;
      63           4 :   replace_global_variables(p, sigma);
      64             : 
      65           4 :   return sigma;
      66           4 : }
      67             : 
      68             : } // namespace detail
      69             : 
      70             : } // namespace pbes_system
      71             : 
      72             : } // namespace mcrl2
      73             : 
      74             : #endif // MCRL2_PBES_DETAIL_INSTANTIATE_GLOBAL_VARIABLES_H