Line data    Source code

       1             : // Author(s): Jeroen Keiren
       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 list_test.cpp
      10             : /// \brief Basic regression test for list expressions.
      11             : 
      12             : #define BOOST_TEST_MODULE list_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/data/list.h"
      16             : #include "mcrl2/data/parse.h"
      17             : #include "mcrl2/data/rewriter.h"
      18             : 
      19             : 
      20             : using namespace mcrl2;
      21             : using namespace mcrl2::data;
      22             : using namespace mcrl2::data::sort_list;
      23             : 
      24             : template <typename Predicate>
      25          10 : void test_data_expression(const std::string& s, const mcrl2::data::variable_vector& v, Predicate p)
      26             : {
      27          10 :   data_expression e = parse_data_expression(s, v);
      28          10 :   BOOST_CHECK(p(e));
      29          10 : }
      30             : 
      31             : /* Test case for various list expressions, based
      32             :    on the following specification:
      33             : 
      34             : proc P(l: List(Nat)) = (1 in l) -> tau . P(10 |> l ++ [#l] <| 100)
      35             :                      + (l.1 == 30) -> tau . P(tail(l))
      36             :                      + (head(l) == 20) -> tau . P([rhead(l)] ++ rtail(l));
      37             : 
      38             : init P([20, 30, 40]);
      39             : */
      40           1 : void list_expression_test()
      41             : {
      42           1 :   data::data_specification specification;
      43             : 
      44           1 :   specification.add_context_sort(sort_list::list(sort_pos::pos()));
      45             : 
      46             : 
      47           1 :   data::rewriter normaliser(specification);
      48             : 
      49           1 :   variable_vector v;
      50           1 :   v.push_back(parse_variable("l:List(Nat)"));
      51             : 
      52           1 :   test_data_expression("1 in l", v, is_in_application);
      53           1 :   test_data_expression("10 |> l", v, is_cons_application);
      54           1 :   test_data_expression("l <| 10", v, is_snoc_application);
      55           1 :   test_data_expression("#l", v, is_count_application);
      56           1 :   test_data_expression("l ++ [10]", v, is_concat_application);
      57           1 :   test_data_expression("l.1", v, is_element_at_application);
      58           1 :   test_data_expression("head(l)", v, is_head_application);
      59           1 :   test_data_expression("rhead(l)", v, is_rhead_application);
      60           1 :   test_data_expression("tail(l)", v, is_tail_application);
      61           1 :   test_data_expression("rtail(l)", v, is_rtail_application);
      62             : 
      63           2 :   data_expression e = parse_data_expression("[10]", v);
      64           1 :   BOOST_CHECK(is_cons_application(normaliser(e)));
      65           1 : }
      66             : 
      67           2 : BOOST_AUTO_TEST_CASE(test_main)
      68             : {
      69           1 :   list_expression_test();
      70           1 : }
      71             :