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 normal_form_test.cpp 10 : /// \brief Tests for transformations into normal form. 11 : 12 : #define BOOST_TEST_MODULE normal_form_test 13 : #include "mcrl2/pbes/normal_forms.h" 14 : #include "mcrl2/pbes/parse.h" 15 : #include "mcrl2/pbes/print.h" 16 : 17 : #include <boost/test/included/unit_test.hpp> 18 : 19 : using namespace mcrl2; 20 : using namespace mcrl2::pbes_system; 21 : 22 4 : void test_standard_recursive_form(const std::string& bes_spec, bool recursive_form = false) 23 : { 24 4 : pbes b; 25 4 : std::stringstream from(bes_spec); 26 4 : from >> b; 27 4 : std::cout << "before\n" << pbes_system::pp(b) << std::endl; 28 : 29 4 : make_standard_form(b, recursive_form); 30 4 : std::cout << "after\n" << pbes_system::pp(b) << std::endl; 31 4 : } 32 : 33 1 : void test_standard_recursive_form() 34 : { 35 : std::string bes1 = 36 : "pbes \n" 37 : " \n" 38 : "nu X1 = X2 && X1; \n" 39 : "mu X2 = X1 || X2; \n" 40 : " \n" 41 1 : "init X1; \n" 42 : ; 43 1 : test_standard_recursive_form(bes1, false); 44 1 : test_standard_recursive_form(bes1, true); 45 : 46 : std::string bes2 = 47 : "pbes \n" 48 : " \n" 49 : "nu X1 = X2 && true; \n" 50 : "mu X2 = X1 || X2 && X1; \n" 51 : " \n" 52 1 : "init X1; \n" 53 : ; 54 : 55 1 : test_standard_recursive_form(bes2, false); 56 1 : test_standard_recursive_form(bes2, true); 57 : 58 1 : } 59 : 60 2 : BOOST_AUTO_TEST_CASE(test_main) 61 : { 62 1 : test_standard_recursive_form(); 63 1 : }