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 normalize_sorts_test.cpp 10 : /// \brief Test for normalizing sorts. 11 : 12 : #define BOOST_TEST_MODULE normalize_sorts_test 13 : #include "mcrl2/data/normalize_sorts.h" 14 : #include "mcrl2/data/parse.h" 15 : 16 : #include <boost/test/included/unit_test.hpp> 17 : 18 : using namespace mcrl2; 19 : using namespace mcrl2::data; 20 : 21 1 : void test_normalize_sorts() 22 : { 23 : std::string DATASPEC = 24 : "sort Bit = struct e0 | e1; \n" 25 : " AbsBit = struct arbitrary; \n" 26 : " \n" 27 : "map inv: Bit -> Bit; \n" 28 : " h: Bit -> AbsBit; \n" 29 : " \n" 30 : "eqn inv(e0) = e1; \n" 31 1 : " inv(e1) = e0; \n" 32 : ; 33 : 34 1 : data_specification dataspec = parse_data_specification(DATASPEC); 35 : 36 1 : data::function_symbol f; 37 1 : f = parse_function_symbol("abseq : AbsBit # AbsBit -> Set(Bool)", DATASPEC); 38 1 : dataspec.add_mapping(f); 39 1 : f = parse_function_symbol("absinv : AbsBit -> Set(AbsBit)", DATASPEC); 40 1 : dataspec.add_mapping(f); 41 : 42 1 : data_equation_vector equations = dataspec.user_defined_equations(); 43 1 : data::normalize_sorts(equations, dataspec); 44 1 : } 45 : 46 : // The test below checks whether the calculation of a confluent and terminating rewrite system for types using 47 : // Knuth-Bendix completion is efficient. Aleksi Peltonen showed in the spring of 2018 that Knuth-Bendix completion 48 : // was exponential, causing the example below not to terminate within reasonable time. 49 1 : void test_apply_knuth_bendix_completion_on_sorts() 50 : { 51 : std::string DATASPEC = 52 : "sort A_t = Nat; B_t = Nat; C_t = Nat; D_t = Nat; E_t = Nat; F_t = Nat; G_t = Nat; H_t = Nat; I_t = Nat; J_t=Nat; K_t=Nat; \n" 53 : " L_t = Nat; M_t = Nat; N_t = Nat; O_t = Nat;\n" 54 1 : " S_t = struct s( A:A_t, B:B_t, C:C_t, D:D_t, E:E_t, F:F_t, G:G_t, H:H_t, I:I_t, J:J_t, K:K_t, L:L_t, M:M_t, N:N_t, O:O_t); \n"; 55 : 56 1 : data_specification dataspec = parse_data_specification(DATASPEC); 57 : 58 1 : data_equation_vector equations = dataspec.user_defined_equations(); 59 1 : data::normalize_sorts(equations, dataspec); 60 1 : } 61 : 62 : // The specification below led to an infinite loop in January 2019 when applying Knuth-Bendix completion. 63 : // The reason was a missing normalisation of the rhs of type equations, leading to a loop. front_doorstate was 64 : // mapped to rear_doorstate and vice versa. 65 : // The specification is not well typed, as there are constants with different types. This test is to 66 : // check whether there is no loop, and typechecking never finishes. 67 1 : void test_loop_free_knuth_bendix_completion() 68 : { 69 : std::string DATASPEC = 70 : "sort front_doorstate = struct open | closed; \n" 71 1 : " rear_doorstate = struct open | closed;\n" 72 : ; 73 : 74 : try 75 : { 76 1 : data_specification dataspec = parse_data_specification(DATASPEC); 77 0 : } 78 1 : catch (mcrl2::runtime_error& e) 79 : { 80 : // This is ok. A runtime exception is expected. 81 1 : return; 82 1 : } 83 0 : BOOST_CHECK(false); // No exception is not ok. 84 1 : } 85 : 86 2 : BOOST_AUTO_TEST_CASE(test_main) 87 : { 88 1 : test_normalize_sorts(); 89 1 : test_apply_knuth_bendix_completion_on_sorts(); 90 1 : test_loop_free_knuth_bendix_completion(); 91 1 : }