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 pbes_property_map_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE pbes_property_map_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : #include "mcrl2/pbes/detail/pbes_property_map.h"
      15             : #include "mcrl2/pbes/txt2pbes.h"
      16             : 
      17             : using namespace mcrl2;
      18             : using namespace mcrl2::pbes_system;
      19             : 
      20           2 : BOOST_AUTO_TEST_CASE(property_map_test)
      21             : {
      22             :   const std::string PBES_SPEC=
      23             :     "% This file contains PBES example 5, as described in:                       \n"
      24             :     "%                                                                           \n"
      25             :     "% A. van Dam, B. Ploeger and T.A.C. Willemse. Instantiation for             \n"
      26             :     "% Parameterised Boolean Equation Systems.  Computer Science Report          \n"
      27             :     "% 08-11, Eindhoven University of Technology (TU/e), 2008.                   \n"
      28             :     "                                                                            \n"
      29             :     "pbes mu X(b: Bool, n: Nat) = Y(b, n);                                       \n"
      30             :     "     nu Y(b: Bool, n: Nat) = (val(!b) || X(!b, n)) &&                       \n"
      31             :     "                             (val(!b) || Y(b, n+1)) &&                      \n"
      32             :     "                             (val(b) || val(n == 0) || Y(b, Int2Nat(n-1))); \n"
      33             :     "                                                                            \n"
      34           1 :     "init X(true, 0);                                                            \n"
      35             :   ;
      36             : 
      37             :   const std::string INFO =
      38             :     "binding_variable_names       = X, Y                                   \n"
      39             :     "binding_variables            = X(b: Bool, n: Nat), Y(b: Bool, n: Nat) \n"
      40             :     "declared_free_variable_names =                                        \n"
      41             :     "declared_free_variables      =                                        \n"
      42             :     "declared_variable_count      = 0                                      \n"
      43             :     "equation_count               = 2                                      \n"
      44             :     "mu_equation_count            = 1                                      \n"
      45             :     "nu_equation_count            = 1                                      \n"
      46             :     "occurring_variable_names     = X, Y                                   \n"
      47             :     "occurring_variables          = X(b: Bool, n: Nat), Y(b: Bool, n: Nat) \n"
      48             :     "used_free_variable_count     = 0                                      \n"
      49             :     "used_free_variables          =                                        \n"
      50           1 :     "used_free_variables_names    =                                        \n"
      51             :   ;
      52             : 
      53           1 :   pbes p = txt2pbes(PBES_SPEC);
      54           1 :   pbes_system::detail::pbes_property_map info1(p);
      55           1 :   std::cerr << info1.to_string() << std::endl;
      56           1 :   pbes_system::detail::pbes_property_map info2(INFO);
      57           1 :   std::string diff = info1.compare(info2);
      58           1 :   BOOST_CHECK(diff.empty());
      59           1 : }