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 parser_test.cpp
      10             : /// \brief Regression test for parsing a data specification.
      11             : 
      12             : #define BOOST_TEST_MODULE parser_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/data/parse.h"
      16             : 
      17             : using namespace mcrl2;
      18             : 
      19           1 : void parser_test()
      20             : {
      21             :   const std::string text(
      22             :     "sort S;\n"
      23             :     "cons s:S;\n"
      24             :     "map f:S -> List(S);\n"
      25           1 :   );
      26             : 
      27           1 :   data::data_specification spec(data::parse_data_specification(text));
      28             : 
      29           1 :   std::cerr << "number of sorts " << spec.sorts().size() << "\n";
      30           1 :   BOOST_CHECK(spec.sorts().size() == 7); // Bool, Pos, S, List(S), S->List(S), Nat, @NatPair.
      31           1 :   BOOST_CHECK(spec.constructors(data::basic_sort("S")).size() == 1);
      32           1 :   std::cerr << "number of functions " << spec.mappings().size() << "\n";
      33           1 :   BOOST_CHECK(spec.mappings().size() == 107);
      34             : 
      35           1 :   BOOST_CHECK(data::parse_data_expression("2") == data::sort_pos::pos(2));
      36           1 :   BOOST_CHECK(data::parse_data_expression("0") == data::sort_nat::nat(0));
      37           1 :   BOOST_CHECK(data::parse_sort_expression("Nat") == data::sort_nat::nat());
      38             : //  BOOST_CHECK(data::parse_data_expression("-1") == data::sort_int::int_(-1));
      39             : //  BOOST_CHECK(data::parse_data_expression("1/2") == data::sort_real::real_(1, 2));
      40           1 : }
      41             : 
      42             : // This test triggers a sort normalization problem.
      43           1 : void test_user_defined_sort()
      44             : {
      45             :   using namespace data;
      46             : 
      47           1 :   std::string text = "sort D = struct d1 | d2;\n";
      48           1 :   data_specification data_spec = parse_data_specification(text);
      49           2 :   sort_expression s = parse_sort_expression("D", data_spec);
      50           1 : }
      51             : 
      52           1 : void test_whr()
      53             : {
      54             :   using namespace data;
      55           2 :   data_expression x = parse_data_expression("exists n: Pos . n == 0 whr n = 1 end");
      56           1 : }
      57             : 
      58             : // returns true if parsing succeeded
      59          16 : bool parse_sort(const data::data_specification& data_spec, const std::string& text)
      60             : {
      61             :   try
      62             :   {
      63          16 :     data::sort_expression s = data::parse_sort_expression(text, data_spec);
      64          12 :   }
      65           4 :   catch (mcrl2::runtime_error&)
      66             :   {
      67           4 :     return false;
      68           4 :   }
      69          12 :   return true;
      70             : }
      71             : 
      72             : // if expected_result is false, parsing is expected to fail
      73          16 : void test_sort_expression(const data::data_specification& data_spec, const std::string& text, bool expected_result)
      74             : {
      75          16 :   bool result = parse_sort(data_spec, text);
      76          16 :   if (result != expected_result)
      77             :   {
      78           0 :     std::cout << "ERROR: parsing the sort expression '" << text << "' produced the result " << std::boolalpha << result << std::endl;
      79             :   }
      80          16 :   BOOST_CHECK(result == expected_result);
      81          16 : }
      82             : 
      83           1 : void test_ticket_1267()
      84             : {
      85           2 :   data::data_specification data_spec = data::parse_data_specification("sort A;");
      86           1 :   test_sort_expression(data_spec, "A -> A # A", false);
      87           1 :   test_sort_expression(data_spec, "(A -> A) # A", false);
      88           1 :   test_sort_expression(data_spec, "A # A", false);
      89           1 :   test_sort_expression(data_spec, "(A # A)", false);
      90             : 
      91           1 :   test_sort_expression(data_spec, "(A # A) -> A", true);
      92           1 :   test_sort_expression(data_spec, "A -> ((A # A) -> (A -> A))", true);
      93           1 :   test_sort_expression(data_spec, "A", true);
      94           1 :   test_sort_expression(data_spec, "A # A -> A", true);
      95           1 :   test_sort_expression(data_spec, "A -> A # A -> A -> A", true);
      96           1 :   test_sort_expression(data_spec, "A -> (A -> A)", true);
      97           1 :   test_sort_expression(data_spec, "(A -> A) -> A", true);
      98           1 :   test_sort_expression(data_spec, "A # A -> (A -> A)", true);
      99           1 :   test_sort_expression(data_spec, "A # (A -> A) -> (A -> A)", true);
     100           1 :   test_sort_expression(data_spec, "(A -> A) # A -> (A -> A)", true);
     101           1 :   test_sort_expression(data_spec, "A # A # A -> A", true);
     102           1 :   test_sort_expression(data_spec, "A -> A -> A -> A", true);
     103           1 : }
     104             : 
     105           2 : BOOST_AUTO_TEST_CASE(test_main)
     106             : {
     107           1 :   parser_test();
     108           1 :   test_user_defined_sort();
     109           1 :   test_whr();
     110           1 :   test_ticket_1267();
     111           1 : }