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 boolean_operator.cpp 10 : /// \brief Test for boolean operators. 11 : 12 : #define BOOST_TEST_MODULE boolean_operator_test 13 : #include <boost/test/included/unit_test.hpp> 14 : 15 : #include "mcrl2/pbes/detail/parse.h" 16 : 17 : using namespace mcrl2; 18 : 19 : const std::string VARIABLE_SPECIFICATION = 20 : "datavar \n" 21 : " b: Bool; \n" 22 : " b1: Bool; \n" 23 : " b2: Bool; \n" 24 : " b3: Bool; \n" 25 : " \n" 26 : " n: Nat; \n" 27 : " n1: Nat; \n" 28 : " n2: Nat; \n" 29 : " n3: Nat; \n" 30 : " \n" 31 : " p: Pos; \n" 32 : " p1: Pos; \n" 33 : " p2: Pos; \n" 34 : " p3: Pos; \n" 35 : " \n" 36 : "predvar \n" 37 : " X; \n" 38 : " Y: Nat; \n" 39 : " Z: Bool, Pos; \n" 40 : ; 41 : 42 : inline 43 6 : pbes_system::pbes_expression expr(const std::string& text) 44 : { 45 6 : return pbes_system::parse_pbes_expression(text, VARIABLE_SPECIFICATION); 46 : } 47 : 48 2 : BOOST_AUTO_TEST_CASE(test_boolean_operators) 49 : { 50 1 : mcrl2::pbes_system::pbes_expression result; 51 1 : data::optimized_or(result, expr("false"), expr("X")); 52 1 : BOOST_CHECK(result == expr("X")); 53 1 : data::optimized_and(result, expr("false"), expr("X")); 54 1 : BOOST_CHECK(result == expr("false")); 55 1 : } 56 :