Line data Source code
1 : // Author(s): Aad Mathijssen, 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 typecheck_test.cpp 10 : /// \brief Add your file description here. 11 : 12 : #define BOOST_TEST_MODULE typecheck_test 13 : #include <boost/test/included/unit_test.hpp> 14 : #include "mcrl2/core/parse.h" 15 : #include "mcrl2/pbes/parse.h" 16 : 17 : using namespace mcrl2; 18 : 19 2 : void test_pbes_specification(const std::string& pbes_in, bool test_type_checker = true) 20 : { 21 2 : pbes_system::pbes p = pbes_system::detail::parse_pbes_new(pbes_in).construct_pbes(); 22 2 : if (test_type_checker) 23 : { 24 2 : pbes_system::typecheck_pbes(p); 25 2 : std::string pbes_out = pbes_system::pp(p); 26 : 27 2 : if (pbes_in!=pbes_out) 28 : { 29 0 : std::cerr << "PBES IN AND PBES OUT ARE DIFFERENT (with typechecking).\n"; 30 0 : std::cerr << "PBES IN: " << pbes_in << "\n"; 31 0 : std::cerr << "PBES OUT: " << pbes_out << "\n"; 32 : } 33 2 : BOOST_CHECK(pbes_in == pbes_out); 34 2 : } 35 2 : } 36 : 37 2 : BOOST_AUTO_TEST_CASE(test_pbes_specification1) 38 : { 39 : //test PBES specification involving global variables 40 1 : test_pbes_specification( 41 : "glob dc: Bool;\n" 42 : "\n" 43 : "pbes nu X(b: Bool) =\n" 44 : " val(b) && X(dc);\n" 45 : "\n" 46 : "init X(dc);\n" 47 : ); 48 1 : } 49 : 50 2 : BOOST_AUTO_TEST_CASE(test_pbes_specification2) 51 : { 52 : //test PBES specification where the type of [10,m] should become List(Nat), not List(Pos). 53 : //This failed in revision 10180 and before. 54 1 : test_pbes_specification( 55 : "pbes nu X0(m: Nat) =\n" 56 : " forall i: Nat. val(!(i < 2)) || X0([10, m] . i);\n" 57 : "\n" 58 : "init X0(0);\n" 59 : ); 60 1 : }