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 monotonicity_test.cpp
      10             : /// \brief Tests for the is_monotonous function for pbes expressions.
      11             : 
      12             : #define BOOST_TEST_MODULE monotonicity_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/pbes/is_monotonous.h"
      16             : #include "mcrl2/pbes/txt2pbes.h"
      17             : 
      18             : using namespace mcrl2;
      19             : using namespace mcrl2::pbes_system;
      20             : 
      21           6 : void run_monotonicity_test_case(const pbes_expression& x, bool expected_result)
      22             : {
      23           6 :   bool result = is_monotonous(x);
      24           6 :   if (result != expected_result)
      25             :   {
      26           0 :     std::cerr << "--- Failing monotonicity test case ---\n";
      27           0 :     std::cerr << " x = " << pbes_system::pp(x) << std::endl;
      28           0 :     std::cerr << " expected_result = " << std::boolalpha << expected_result << std::endl;
      29             :   }
      30           6 :   BOOST_CHECK(result == expected_result);
      31           6 : }
      32             : 
      33           2 : BOOST_AUTO_TEST_CASE(test_monotonicity)
      34             : {
      35             :   std::string text =
      36             :     "pbes                                                 \n"
      37             :     " nu X0(m, n: Nat) = val(n == m) && X0(m + 1, n + 1); \n"
      38             :     " nu X1            = !X1;                             \n"
      39             :     " nu X2            = !!X2;                            \n"
      40             :     " nu X3            = !X2 => X1;                       \n"
      41             :     " nu X4            = !(forall n:Nat . (X2 => !X1));   \n"
      42             :     " nu X5            = !(forall n:Nat . (X2 || !X1));   \n"
      43             :     "                                                     \n"
      44           1 :     " init X0(0, 0);                                      \n"
      45             :     ;
      46           1 :   bool normalize = false;
      47           1 :   pbes p = txt2pbes(text, normalize);
      48           1 :   std::vector<pbes_equation> eqn = p.equations();
      49             : 
      50           1 :   std::vector<bool> expected_results(eqn.size(), true);
      51           1 :   expected_results[0] = true;
      52           1 :   expected_results[1] = false;
      53           1 :   expected_results[2] = true;
      54           1 :   expected_results[3] = true;
      55           1 :   expected_results[4] = true;
      56           1 :   expected_results[5] = false;
      57             : 
      58           7 :   for (std::size_t i = 0; i < eqn.size(); ++i)
      59             :   {
      60           6 :     run_monotonicity_test_case(eqn[i].formula(), expected_results[i]);
      61             :   }
      62           1 : }