Line data    Source code

       1             : // Author(s): Jeroen van der Wulp
       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 representative_generator_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE representative_generator_test
      13             : 
      14             : #include <boost/test/included/unit_test.hpp>
      15             : 
      16             : #include "mcrl2/data/list.h"
      17             : #include "mcrl2/data/parse.h"
      18             : #include "mcrl2/data/representative_generator.h"
      19             : #include "mcrl2/data/set.h"
      20             : 
      21             : using namespace mcrl2;
      22             : using namespace mcrl2::data;
      23             : 
      24           1 : void test_representative_generator()
      25             : {
      26             :   data_specification specification=parse_data_specification
      27             :                                    ("map f__:Nat; \n"
      28             :                                     "    g__:List(Bool);\n"
      29             :                                     "    h__:Set(Real);\n"
      30           2 :                                    );
      31             : 
      32           1 :   std::vector< data::structured_sort_constructor_argument > arguments;
      33           1 :   arguments.push_back(structured_sort_constructor_argument("s", basic_sort("E")));
      34           1 :   arguments.push_back(structured_sort_constructor_argument("n", sort_nat::nat()));
      35             : 
      36           1 :   std::vector< structured_sort_constructor > constructors;
      37           1 :   constructors.push_back(structured_sort_constructor("d", structured_sort_constructor_argument_list(arguments.begin(), arguments.begin() + 1)));
      38           1 :   constructors.push_back(structured_sort_constructor("e", structured_sort_constructor_argument_list(arguments.begin() + 1, arguments.begin() + 2)));
      39             : 
      40           1 :   specification.add_alias(alias(basic_sort("D"), structured_sort(structured_sort_constructor_list(constructors.begin(), constructors.begin() + 1))));
      41           1 :   specification.add_alias(alias(basic_sort("E"), structured_sort(structured_sort_constructor_list(constructors.begin() + 1, constructors.begin() + 2))));
      42             : 
      43           1 :   representative_generator default_expression_generator(specification);
      44             : 
      45             :   // Should be true or false, since constants are preferred to other constructors or mappings
      46           1 :   BOOST_CHECK(default_expression_generator(sort_bool::bool_()) == sort_bool::true_() ||
      47             :               default_expression_generator(sort_bool::bool_()) == sort_bool::false_());
      48             : 
      49             :   // Should be c0, since constants are preferred to other constructors or mappings
      50           1 :   BOOST_CHECK(default_expression_generator(sort_nat::nat()) == sort_nat::c0());
      51             : 
      52             :   // Should be empty, since constants are preferred to other constructors or mappings
      53           1 :   BOOST_CHECK(default_expression_generator(sort_list::list(sort_bool::bool_())) == sort_list::empty(sort_bool::bool_()));
      54             : 
      55             :   // Should be e(0), since constants are preferred to other constructors or mappings
      56           1 :   BOOST_CHECK(default_expression_generator(basic_sort("E")) ==
      57             :               constructors[1].constructor_function(basic_sort("E"))(default_expression_generator(sort_nat::nat())));
      58             : 
      59             :   // Should be d(e(0)), since constants are preferred to other constructors or mappings
      60           1 :   BOOST_CHECK(default_expression_generator(basic_sort("D")) ==
      61             :               constructors[0].constructor_function(basic_sort("D"))(default_expression_generator(basic_sort("E"))));
      62             : 
      63             :   // Check whether the representative of the set of reals is the empty set of reals, or the set of all reals.
      64             :   // The answer depends on the relative ordering of the false_function and true_function in sets of function symbols.
      65             :   // This in turns depends on the place where these functions end up in the memory. 
      66           2 :   const data_expression t=default_expression_generator(container_sort(set_container(),data::sort_real::real_()));
      67           1 :   BOOST_CHECK(t == data::sort_set::constructor(data::sort_real::real_(),
      68             :                                                data::sort_set::false_function(data::sort_real::real_()),
      69             :                                                data::sort_fset::empty(data::sort_real::real_()))  ||
      70             :               t == data::sort_set::constructor(data::sort_real::real_(),
      71             :                                                data::sort_set::true_function(data::sort_real::real_()),
      72             :                                                data::sort_fset::empty(data::sort_real::real_())));
      73             : 
      74             :    // Check whether a proper representative term is generated for a function sort.
      75           4 :    const sort_expression s1=function_sort({ basic_sort("Nat")}, basic_sort("Nat"));
      76           1 :    BOOST_CHECK(default_expression_generator(s1).sort() == s1);
      77           5 :    const sort_expression s2=function_sort({ basic_sort("Nat"), basic_sort("Real")}, basic_sort("Nat"));
      78           1 :    BOOST_CHECK(default_expression_generator(s2).sort() == s2);
      79           1 : }
      80             : 
      81           2 : BOOST_AUTO_TEST_CASE(test_main)
      82             : {
      83           1 :   test_representative_generator();
      84           1 : }