Line data    Source code

       1             : // Author(s): Wieger Wesselink
       2             : // Copyright: see the accompanying file COPYING.
       3             : //
       4             : // Distributed under the Boost Software License, Version 1.0.
       5             : // (See accompanying file LICENSE_1_0.txt or copy at
       6             : // http://www.boost.org/LICENSE_1_0.txt)
       7             : //
       8             : /// \file test_utility.h
       9             : /// \brief Utility functions for testing.
      10             : 
      11             : #ifndef MCRL2_PBES_DETAIL_TEST_UTILITY_H
      12             : #define MCRL2_PBES_DETAIL_TEST_UTILITY_H
      13             : 
      14             : #include "mcrl2/pbes/pbes.h"
      15             : 
      16             : namespace mcrl2
      17             : {
      18             : 
      19             : namespace pbes_system
      20             : {
      21             : 
      22             : namespace detail
      23             : {
      24             : 
      25             : /// \brief Returns a data variable of type Nat with a given name
      26             : /// \param name A string
      27             : /// \return A data variable of type Nat with a given name
      28          15 : data::variable nat(const std::string& name)
      29             : {
      30          30 :   return data::variable(core::identifier_string(name), data::sort_nat::nat());
      31             : }
      32             : 
      33             : /// \brief Returns a data variable of type Pos with a given name
      34             : /// \param name A string
      35             : /// \return A data variable of type Pos with a given name
      36           2 : data::variable pos(const std::string& name)
      37             : {
      38           4 :   return data::variable(core::identifier_string(name), data::sort_pos::pos());
      39             : }
      40             : 
      41             : /// \brief Returns a data variable of type Bool with a given name
      42             : /// \param name A string
      43             : /// \return A data variable of type Bool with a given name
      44          12 : data::variable bool_(const std::string& name)
      45             : {
      46          24 :   return data::variable(core::identifier_string(name), data::sort_bool::bool_());
      47             : }
      48             : 
      49             : /// \brief Returns a propositional variable declaration with the given name and parameters
      50             : /// \param name A string
      51             : /// \param parameters A sequence of data variables
      52             : /// \return A propositional variable declaration with the given name and parameters
      53           6 : propositional_variable propvar(const std::string& name, const data::variable_list& parameters)
      54             : {
      55          12 :   return propositional_variable(core::identifier_string(name), parameters);
      56             : }
      57             : 
      58             : /// \brief Returns a propositional variable instantiation with the given name and parameters
      59             : /// \param name A string
      60             : /// \param parameters A sequence of data expressions
      61             : /// \return A propositional variable instantiation with the given name and parameters
      62           6 : propositional_variable_instantiation propvarinst(const std::string& name, const data::data_expression_list& parameters)
      63             : {
      64          12 :   return propositional_variable_instantiation(core::identifier_string(name), parameters);
      65             : }
      66             : 
      67             : } // namespace detail
      68             : 
      69             : } // namespace pbes_system
      70             : 
      71             : } // namespace mcrl2
      72             : 
      73             : #endif // MCRL2_PBES_DETAIL_TEST_UTILITY_H