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 bag_test.cpp
      10             : // / \brief Basic regression test for bag expressions.
      11             : 
      12             : #define BOOST_TEST_MODULE bag_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/data/bag.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             : 
      23             : // test whether parsing s returns an expression matching predicate p.
      24             : // Furthermore check whether the expression does not satisfy q.
      25             : template <typename Predicate, typename NegativePredicate>
      26          10 : void test_data_expression(const std::string& s, const variable_vector& v, Predicate p, NegativePredicate q)
      27             : {
      28          10 :   std::cerr << "testing data expression " << s << std::endl;
      29          10 :   data_expression e = parse_data_expression(s, v);
      30          10 :   std::cerr << "parsed expression " << e << "\n";
      31          10 :   BOOST_CHECK(p(e));
      32          10 :   BOOST_CHECK(!q(e));
      33          10 : }
      34             : 
      35          71 : void test_expression(const std::string& evaluate, const std::string& expected, data::rewriter r)
      36             : {
      37          71 :   data_expression d1 = parse_data_expression(evaluate);
      38          71 :   data_expression d2 = parse_data_expression(expected);
      39          71 :   if (r(d1)!=r(d2))
      40             :   {
      41           0 :     std::cerr << "Evaluating: " << evaluate << "\n";
      42           0 :     std::cerr << "Result: " << d1 << "\n";
      43           0 :     std::cerr << "Expected result: " << expected << "\n";
      44           0 :     BOOST_CHECK(r(d1) == r(d2));
      45           0 :     std::cerr << "------------------------------------------------------\n";
      46             :   }
      47          71 : }
      48             : 
      49             : 
      50           1 : void bag_expression_test()
      51             : {
      52           1 :   data::data_specification specification;
      53             : 
      54           1 :   specification.add_context_sort(sort_bag::bag(sort_pos::pos()));
      55           1 :   specification.add_context_sort(sort_bag::bag(sort_bool::bool_()));
      56             : 
      57           1 :   data::rewriter normaliser(specification);
      58             : 
      59           1 :   variable_vector v;
      60           1 :   v.push_back(parse_variable("b:Bag(Nat)"));
      61             : 
      62           1 :   BOOST_CHECK(sort_bag::is_bag(sort_bag::bag(sort_nat::nat())));
      63           1 :   BOOST_CHECK(!sort_bag::is_bag(sort_nat::nat()));
      64             : 
      65           1 :   test_data_expression("{x : Nat | x}", v, sort_bag::is_constructor_application, sort_bag::is_in_application);
      66           1 :   test_data_expression("1 in b", v, sort_bag::is_in_application, sort_bag::is_union_application);
      67           1 :   test_data_expression("{:} + b", v, sort_bag::is_union_application, sort_bag::is_intersection_application);
      68           1 :   test_data_expression("(({:} + b) - {20:1}) * {40:5}", v, sort_bag::is_intersection_application, is_less_application<data_expression>);
      69           1 :   test_data_expression("{10:count(20,b)} < b", v, is_less_application<data_expression>, sort_bag::is_bag_comprehension_application);
      70           1 :   test_data_expression("b <= {20:2}", v, is_less_equal_application<data_expression>, sort_bag::is_set2bag_application);
      71           1 :   test_data_expression("Set2Bag({20,30,40})", v, sort_bag::is_set2bag_application, sort_bag::is_union_application);
      72           1 :   test_data_expression("{20:2} + Set2Bag({20,30,40})", v, sort_bag::is_union_application, is_less_equal_application<data_expression>);
      73           1 :   test_data_expression("b <= Set2Bag({20,30,40})", v, is_less_equal_application<data_expression>, sort_bag::is_constructor_application);
      74             : 
      75           1 :   test_data_expression("b <= {20:2} + Set2Bag({20,30,40})", v, is_less_equal_application<data_expression>, sort_bag::is_constructor_application);
      76             : 
      77           2 :   data_expression e = parse_data_expression("{20:1}", v);
      78           1 :   BOOST_CHECK(sort_fbag::is_cons_application(normaliser(e)));
      79             : 
      80           1 :   e = parse_data_expression("{20:4, 30:3, 40:2}", v);
      81           1 :   BOOST_CHECK(sort_fbag::is_cons_application(normaliser(e)));
      82             : 
      83           1 :   e = parse_data_expression("{10:count(20,b)}", v);
      84           1 :   BOOST_CHECK(sort_fbag::is_cinsert_application(normaliser(e)));
      85             : 
      86             :   // Chect the operation == on bags
      87           1 :   test_expression("{:} == ({true:2} - {true:2})","true",normaliser);  // {true}-{true} is a trick to type {:} == {:}. 
      88           1 :   test_expression("{:} == {false:2}", "false",normaliser);
      89           1 :   test_expression("{:} == {true:2}", "false",normaliser);
      90           1 :   test_expression("{true:2} == {true:3}", "false",normaliser);
      91           1 :   test_expression("{false:2} == {false:2}", "true",normaliser);
      92           1 :   test_expression("{true:2} == {false:2, true:2}", "false",normaliser);
      93           1 :   test_expression("{false:2, true:2} == {false:2}", "false",normaliser);
      94           1 :   test_expression("{false:2, true:2} == {true:2, false:2}", "true",normaliser);
      95             : 
      96             :   // Check the operation < on bags.
      97           1 :   test_expression("{:} < ({true:2} - {true:2})","false",normaliser);  // {true}-{true} is a trick to type {:} == {:}. 
      98           1 :   test_expression("{true:2} < {false:4}", "false",normaliser);
      99           1 :   test_expression("{true:2} < {false:2}", "false",normaliser);
     100           1 :   test_expression("{false:2} < {true:4}", "false",normaliser);
     101           1 :   test_expression("{true:2} < {true:3}", "true",normaliser);
     102           1 :   test_expression("{false:2} < {false:1}", "false",normaliser);
     103           1 :   test_expression("{true:2} < {false:4, true:2}", "true",normaliser);
     104           1 :   test_expression("{false:2} < {false:1, true:2}", "false",normaliser);
     105           1 :   test_expression("{true:2} < {true:4, false:2}", "true",normaliser);
     106           1 :   test_expression("{false:2} < {true:4, false:2}", "true",normaliser);
     107           1 :   test_expression("{true:2, false:4} < {true:4}", "false",normaliser);
     108           1 :   test_expression("{true:2, false:4} < {false:2}", "false",normaliser);
     109           1 :   test_expression("{false:2, true:4} < {true:2}", "false",normaliser);
     110           1 :   test_expression("{false:2, true:4} < {false:5}", "false",normaliser);
     111           1 :   test_expression("{true:2, false:4} < {false:2, true:2}", "false",normaliser);
     112           1 :   test_expression("{true:2, false:4} < {true:2, false:2}", "false",normaliser);
     113           1 :   test_expression("{false:2, true:1} < {false:2, true:2}", "true",normaliser);
     114           1 :   test_expression("{false:2, true:4} < {true:7, false:2}", "true",normaliser);
     115           1 :   test_expression("{false:1, false:1} < {false:2}", "false",normaliser);
     116             :   
     117             :   // Check the operation <= on bags.
     118           1 :   test_expression("{:} <= ({true:2}-{true:2})","true",normaliser);  // {true} - {true} is a trick to type {:} == {:}.
     119           1 :   test_expression("{true:2} <= {false:2}", "false",normaliser);
     120           1 :   test_expression("{false:2} <= {true:2}", "false",normaliser);
     121           1 :   test_expression("{true:2} <= {true:2}", "true",normaliser);
     122           1 :   test_expression("{true:3} <= {true:2}", "false",normaliser);
     123           1 :   test_expression("{false:2} <= {false:1}", "false",normaliser);
     124           1 :   test_expression("{false:2} <= {false:7}", "true",normaliser);
     125           1 :   test_expression("{true:2} <= {false:2, true:2}", "true",normaliser);
     126           1 :   test_expression("{false:2} <= {false:4, true:2}", "true",normaliser);
     127           1 :   test_expression("{true:2} <= {true:1, false:2}", "false",normaliser);
     128           1 :   test_expression("{false:2} <= {true:2, false:2}", "true",normaliser);
     129           1 :   test_expression("{true:2, false:2} <= {true:3}", "false",normaliser);
     130           1 :   test_expression("{true:2, false:2} <= {false:1}", "false",normaliser);
     131           1 :   test_expression("{false:2, true:2} <= {true:2}", "false",normaliser);
     132           1 :   test_expression("{false:2, true:2} <= {false:2}", "false",normaliser);
     133           1 :   test_expression("{true:2, false:2} <= {false:2, true:2}", "true",normaliser);
     134           1 :   test_expression("{true:2, false:2} <= {true:2, false:2}", "true",normaliser);
     135           1 :   test_expression("{false:2, true:2} <= {false:2, true:2}", "true",normaliser);
     136           1 :   test_expression("{false:2, true:2} <= {true:2, false:2}", "true",normaliser);
     137           1 :   test_expression("{false:1, false:2} <= {false:2}", "false", normaliser);
     138             : 
     139             :   // Test the operation - on bags.
     140           1 :   test_expression("{true:0} - {:}", "{true:0}", normaliser);
     141           1 :   test_expression("{:} - {true:1}", "{true:0}", normaliser);
     142           1 :   test_expression("{true:1} - {:}", "{true:1}", normaliser);
     143           1 :   test_expression("{:} - {true:2}", "{true:0}", normaliser);
     144           1 :   test_expression("{true:2} - {:}", "{true:2}", normaliser);
     145           1 :   test_expression("{true:1} - {true:1}", "{true:0}", normaliser);
     146           1 :   test_expression("{true:2} - {true:1}", "{true:1}", normaliser);
     147           1 :   test_expression("{true:1} - {true:2}", "{true:0}", normaliser);
     148           1 :   test_expression("{true:1} - {false:1}", "{true:1}", normaliser);
     149           1 :   test_expression("{false:1} - {true:1}", "{false:1}", normaliser);
     150           1 :   test_expression("{true:2} - {false:1}", "{true:2}", normaliser);
     151           1 :   test_expression("{false:2} - {true:1}", "{false:2}", normaliser);
     152           1 :   test_expression("{true:1} - {false:2}", "{true:1}", normaliser);
     153           1 :   test_expression("{false:1} - {true:2}", "{false:1}", normaliser);
     154           1 :   test_expression("{true:1, false:1} - {false:1}", "{true:1}", normaliser);
     155           1 :   test_expression("{true:1, false:1} - {true:1}", "{false:1}", normaliser);
     156           1 :   test_expression("{true:1, false:1} - {true:1, false:1}", "{true:0}",
     157             :                   normaliser);
     158           1 :   test_expression("{true:1, false:1} - {false:1, true:1}", "{true:0}",
     159             :                   normaliser);
     160           1 :   test_expression("{true:2, false:2} - {false:1}", "{true:2, false:1}",
     161             :                   normaliser);
     162           1 :   test_expression("{true:2, false:2} - {true:1}", "{true:1, false:2}",
     163             :                   normaliser);
     164           1 :   test_expression("{true:2, false:2} - {true:1,false:1}", "{true:1, false:1}",
     165             :                   normaliser);
     166           1 :   test_expression("{true:2, false:2} - {false:1,true:1}", "{true:1, false:1}",
     167             :                   normaliser);
     168           1 :   test_expression("{true:2, false:2} - {false:2}", "{true:2}", normaliser);
     169           1 :   test_expression("{true:2, false:2} - {false:2}", "{true:2}", normaliser);
     170           1 : }
     171             : 
     172           2 : BOOST_AUTO_TEST_CASE(test_main)
     173             : {
     174           1 :   bag_expression_test();
     175           1 : }
     176             :