LCOV - code coverage report
Current view: top level - data/test - normalize_sorts_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 29 31 93.5 %
Date: 2024-03-08 02:52:28 Functions: 5 5 100.0 %
Legend: Lines: hit not hit

          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 : }

Generated by: LCOV version 1.14