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 print_test.cpp
      10             : /// \brief Regression test for parsing process expressions
      11             : 
      12             : #define BOOST_TEST_MODULE print_test
      13             : 
      14             : #include <boost/test/included/unit_test.hpp>
      15             : 
      16             : #include "mcrl2/process/parse.h"
      17             : #include "mcrl2/process/print.h"
      18             : 
      19             : using namespace mcrl2;
      20             : using namespace mcrl2::process;
      21             : 
      22           1 : void test_comm()
      23             : {
      24             :   std::string text =
      25             :     "act  a,b,c;\n"
      26             :     "\n"
      27           1 :     "init comm({a | b -> c}, c);\n"
      28             :     ;
      29             : 
      30           1 :   process_specification p = parse_process_specification(text);
      31           1 :   std::string text1 = process::pp(p);
      32           1 :   std::cout << text << std::endl;
      33           1 :   std::cout << "---" << std::endl;
      34           1 :   std::cout << text1 << std::endl;
      35           1 :   std::cout << "---" << std::endl;
      36           1 :   BOOST_CHECK(text == text1);
      37           1 : }
      38             : 
      39           1 : void test_procinst()
      40             : {
      41             :   std::string text =
      42             :     "act  a,b;\n"
      43             :     "\n"
      44             :     "proc P = delta;\n"
      45             :     "\n"
      46           1 :     "init a . P + b . P;\n"
      47             :     ;
      48             : 
      49           1 :   process_specification p = parse_process_specification(text);
      50           1 :   std::string text1 = process::pp(p);
      51           1 :   std::cout << text << std::endl;
      52           1 :   std::cout << "---" << std::endl;
      53           1 :   std::cout << text1 << std::endl;
      54           1 :   std::cout << "---" << std::endl;
      55           1 :   BOOST_CHECK(text == text1);
      56           1 : }
      57             : 
      58           1 : void test_action_name_multiset()
      59             : {
      60           1 :   std::vector<core::identifier_string> v;
      61           1 :   v.push_back(core::identifier_string("a"));
      62           1 :   v.push_back(core::identifier_string("b"));
      63           1 :   v.push_back(core::identifier_string("c"));
      64           1 :   core::identifier_string_list l(v.begin(), v.end());
      65           1 :   action_name_multiset A(l);
      66           1 :   std::string text = process::pp(A);
      67           1 :   BOOST_CHECK(text == "a | b | c");
      68             : 
      69           1 :   atermpp::term_list<action_name_multiset> w;
      70           1 :   w.push_front(A);
      71           1 :   w.push_front(A);
      72           1 :   text = process::pp(w);
      73           1 :   BOOST_CHECK(text == "a | b | c, a | b | c");
      74           1 : }
      75             : 
      76           3 : void check_result(const std::string& expression, const std::string& result, const std::string& expected_result, const std::string& title)
      77             : {
      78           3 :   if (result != expected_result)
      79             :   {
      80           0 :     std::cout << "--- failure in " << title << " ---" << std::endl;
      81           0 :     std::cout << "expression      = " << expression << std::endl;
      82           0 :     std::cout << "result          = " << result << std::endl;
      83           0 :     std::cout << "expected result = " << expected_result << std::endl;
      84           0 :     BOOST_CHECK(result == expected_result);
      85             :   }
      86           3 : }
      87             : 
      88           3 : void test_process_expression(const std::string& expression, const std::string& expected_result)
      89             : {
      90           3 :   std::string text = "act a, b, c, d;\ninit " + expression + ";\n";
      91           3 :   process_specification procspec = parse_process_specification(text);
      92           3 :   std::string result = process::pp(procspec.init());
      93           3 :   check_result(expression, result, expected_result, "process::pp");
      94           3 : }
      95             : 
      96           1 : void test_process_expressions()
      97             : {
      98           1 :   std::string SPEC = "act c; init true -> c;";
      99           1 :   process_specification procspec = parse_process_specification(SPEC);
     100           1 :   BOOST_CHECK(process::pp(procspec.init()) == "true -> c");
     101             : 
     102           1 :   test_process_expression("false -> (true -> tau) <> delta", "false -> (true -> tau) <> delta");
     103           1 :   test_process_expression("false -> true -> tau <> delta", "false -> true -> tau <> delta");
     104           1 :   test_process_expression("false -> true -> a <> b <> c", "false -> (true -> a <> b) <> c");
     105           1 : }
     106             : 
     107           2 : BOOST_AUTO_TEST_CASE(test_main)
     108             : {
     109           1 :   test_comm();
     110           1 :   test_procinst();
     111           1 :   test_action_name_multiset();
     112           1 :   test_process_expressions();
     113           1 : }