Line data Source code
1 : // Author(s): Jeroen Keiren 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 print_test.cpp 10 : /// \brief Add your file description here. 11 : 12 : #define BOOST_TEST_MODULE print_test 13 : #include <boost/test/included/unit_test.hpp> 14 : 15 : #include "mcrl2/pbes/print.h" 16 : #include "mcrl2/pbes/txt2pbes.h" 17 : 18 : using namespace mcrl2; 19 : using namespace mcrl2::pbes_system; 20 : 21 2 : BOOST_AUTO_TEST_CASE(pbes_with_reals) 22 : { 23 : std::string input( 24 : "pbes nu X(T: Real) =\n" 25 : " (((true && val(true)) && val(1 > T)) && true) && ((false || val(!true)) || val(!(1 > T))) || X(1);\n" 26 : "\n" 27 : "init X(0);\n" 28 1 : ); 29 : 30 1 : pbes p; 31 1 : p = txt2pbes(input); 32 : 33 1 : std::string output; 34 1 : output = pbes_system::pp(p); 35 : 36 1 : BOOST_CHECK(output.find("Real;") == std::string::npos); 37 : 38 1 : } 39 : 40 2 : BOOST_AUTO_TEST_CASE(pbes_print) 41 : { 42 : std::string PBES = 43 : "pbes nu X = true; \n" 44 1 : "init X; \n" 45 : ; 46 : 47 1 : pbes p; 48 1 : p = txt2pbes(PBES); 49 1 : pbes_system::pp(p); 50 1 : } 51 : 52 2 : BOOST_AUTO_TEST_CASE(pbes_val) 53 : { 54 : std::string PBES = 55 : "pbes mu X(d: Pos) = val(d > 0); \n" 56 1 : "init X(1); \n" 57 : ; 58 : 59 : std::string expected_result = 60 : "pbes mu X(d: Pos) =\n" 61 : " val(d > 0);\n" 62 : "\n" 63 1 : "init X(1);\n" 64 : ; 65 : 66 1 : pbes p; 67 1 : p = txt2pbes(PBES); 68 1 : std::string result = pbes_system::pp(p); 69 1 : BOOST_CHECK(result == expected_result); 70 1 : }