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 remove_equations_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE remove_equations_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : #include "mcrl2/pbes/detail/pbes_property_map.h"
      15             : #include "mcrl2/pbes/remove_equations.h"
      16             : #include "mcrl2/pbes/txt2pbes.h"
      17             : 
      18             : using namespace mcrl2;
      19             : using namespace mcrl2::pbes_system;
      20             : 
      21           2 : void test_remove_unreachable_variables(const std::string& pbes_spec, const std::string& expected_result)
      22             : {
      23           2 :   pbes p = txt2pbes(pbes_spec);
      24           2 :   pbes q = p;
      25           2 :   remove_unreachable_variables(q);
      26           2 :   BOOST_CHECK(q.is_well_typed());
      27           2 :   pbes_system::detail::pbes_property_map info1(q);
      28           2 :   pbes_system::detail::pbes_property_map info2(expected_result);
      29           2 :   std::string diff = info1.compare(info2);
      30           2 :   if (!diff.empty())
      31             :   {
      32           0 :     std::cerr << "\n------ FAILED TEST ------" << std::endl;
      33           0 :     std::cerr << "--- expected result" << std::endl;
      34           0 :     std::cerr << expected_result << std::endl;
      35           0 :     std::cerr << "--- found result" << std::endl;
      36           0 :     std::cerr << info1.to_string() << std::endl;
      37           0 :     std::cerr << "--- differences" << std::endl;
      38           0 :     std::cerr << diff << std::endl;
      39             :   }
      40           2 :   BOOST_CHECK(diff.empty());
      41           2 : }
      42             : 
      43           2 : BOOST_AUTO_TEST_CASE(test_remove_unreachable_variables1)
      44             : {
      45             :   std::string pbesspec =
      46             :     "pbes nu X1 = X2 && X3;                                   \n"
      47             :     "     nu X2 = X4 && X1;                                   \n"
      48             :     "     nu X3 = true;                                       \n"
      49             :     "     nu X4 = false;                                      \n"
      50             :     "     nu X5 = X6;                                         \n"
      51             :     "     nu X6 = X5;                                         \n"
      52             :     "                                                         \n"
      53           1 :     "init X1;                                                 \n"
      54             :     ;
      55           1 :   std::string bnd = "binding_variable_names = X1, X2, X3, X4";
      56           1 :   test_remove_unreachable_variables(pbesspec, bnd);
      57           1 : }
      58             : 
      59           2 : BOOST_AUTO_TEST_CASE(test_remove_unreachable_variables2) {
      60             :     std::string pbesspec =
      61             :             "pbes                      \n"
      62             :             " nu X(n:Nat) = Y && X(n); \n"
      63             :             " mu Y = Z;                \n"
      64             :             " nu Z = Y;                \n"
      65             :             " nu U = U;                \n"
      66             :             "                          \n"
      67           1 :             " init X(0);               \n"
      68             :     ;
      69           1 :     std::string bnd = "binding_variable_names = X, Y, Z";
      70           1 :     test_remove_unreachable_variables(pbesspec, bnd);
      71           1 : }