Line data    Source code

       1             : // Author(s): Jeroen Keiren, 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 parse_test.cpp
      10             : /// \brief Regression test for parsing process expressions
      11             : 
      12             : #define BOOST_TEST_MODULE parse_test
      13             : 
      14             : #include "mcrl2/process/parse.h"
      15             : 
      16             : #include <boost/test/included/unit_test.hpp>
      17             : 
      18             : using namespace mcrl2;
      19             : using namespace mcrl2::process;
      20             : 
      21             : std::string DATA_DECL =
      22             :   "glob                   \n"
      23             :   "  m: Nat;              \n"
      24             :   "                       \n"
      25             :   "act                    \n"
      26             :   "  a: Nat;              \n"
      27             :   ;
      28             : 
      29             : std::string PROC_DECL =
      30             :   "proc P(n:Nat);         \n"
      31             :   ;
      32             : 
      33           2 : BOOST_AUTO_TEST_CASE(test_parse_process_specification)
      34             : {
      35             :   std::string text =
      36             :     "act  a: Nat;                     \n"
      37             :     "                                 \n"
      38             :     "glob v: Nat;                     \n"
      39             :     "                                 \n"
      40             :     "proc P(i,j: Nat) = a(i).P(1, 1); \n"
      41             :     "                                 \n"
      42           1 :     "init P(i = 1, j = v);            \n"
      43             :     ;
      44             : 
      45           1 :   process_specification p = parse_process_specification(text);
      46           1 :   std::cout << p << std::endl;
      47           1 : }
      48             : 
      49           2 : BOOST_AUTO_TEST_CASE(test_parse)
      50             : {
      51           2 :   process_expression x = parse_process_expression("a(m).P(0)", DATA_DECL, PROC_DECL);
      52           1 :   BOOST_CHECK(process::pp(x) == "a(m) . P(0)");
      53             :   test_parse_process_specification();
      54           1 : }
      55             : 
      56           2 : BOOST_AUTO_TEST_CASE(test_actdecl)
      57             : {
      58           1 :   std::string text = "a: Bool -> Bool;";
      59           1 :   action_label_list l = parse_action_declaration(text);
      60           1 : }
      61             : 
      62           2 : BOOST_AUTO_TEST_CASE(test_stochastic_operator)
      63             : {
      64             :   std::string text =
      65             :     "act  throw: Bool;                   \n"
      66             :     "                                    \n"
      67             :     "proc P = dist b:Bool[1/2].throw(b); \n"
      68             :     "                                    \n"
      69           1 :     "init P;                             \n"
      70             :     ;
      71           1 :   process_specification p = parse_process_specification(text);
      72           1 :   std::cout << p << std::endl;
      73             : 
      74             :   text =
      75             :     "proc P = sum x:Real.(x==x) -> tau.P;\n"
      76           1 :     "init P;\n"
      77             :     ;
      78           1 :   p = parse_process_specification(text);
      79           1 :   std::cout << p << std::endl;
      80           1 : }
      81             : 
      82             : template <typename VariableContainer, typename ActionLabelContainer, typename ProcessIdentifierContainer>
      83           3 : void test_parse_process_expression(const std::string& text,
      84             :                                    const VariableContainer& variables = VariableContainer(),
      85             :                                    const data::data_specification& dataspec = data::data_specification(),
      86             :                                    const ActionLabelContainer& action_labels = std::vector<action_label>(),
      87             :                                    const ProcessIdentifierContainer& process_identifiers = ProcessIdentifierContainer()
      88             :                                   )
      89             : {
      90           3 :   process_expression x = parse_process_expression(text, variables, dataspec, action_labels, process_identifiers);
      91           3 :   std::string text1 = process::pp(x);
      92           3 :   BOOST_CHECK_EQUAL(text, text1);
      93           3 : }
      94             : 
      95           2 : BOOST_AUTO_TEST_CASE(parse_process_expression_test)
      96             : {
      97             :   std::string text =
      98             :     "act  a, b, c;                    \n"
      99             :     "                                 \n"
     100             :     "glob n: Nat;                     \n"
     101             :     "                                 \n"
     102             :     "proc P(b: Bool) = delta;         \n"
     103             :     "proc Q(m: Nat) = delta;          \n"
     104             :     "                                 \n"
     105           1 :     "init delta;                      \n"
     106             :     ;
     107           1 :   process_specification procspec = parse_process_specification(text);
     108           1 :   std::vector<process_identifier> process_identifiers;
     109           3 :   for (const process_equation& eqn: procspec.equations())
     110             :   {
     111           2 :     process_identifiers.push_back(eqn.identifier());
     112             :   }
     113           1 :   test_parse_process_expression("a", procspec.global_variables(), procspec.data(), procspec.action_labels(), process_identifiers);
     114           1 :   test_parse_process_expression("a . P(true)", procspec.global_variables(), procspec.data(), procspec.action_labels(), process_identifiers);
     115           1 :   test_parse_process_expression("a . Q(n)", procspec.global_variables(), procspec.data(), procspec.action_labels(), process_identifiers);
     116           1 : }
     117             :