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 parse_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE parse_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : #include "mcrl2/pbes/detail/parse.h"
      15             : 
      16             : using namespace mcrl2;
      17             : using namespace mcrl2::pbes_system;
      18             : 
      19           2 : BOOST_AUTO_TEST_CASE(test_parse)
      20             : {
      21             :   const std::string PBESSPEC =
      22             :     "pbes nu X(b: Bool) = exists n: Nat. Y(n) && val(b); \n"
      23             :     "     mu Y(n: Nat)  = X(n >= 10);                    \n"
      24             :     "                                                    \n"
      25           1 :     "init X(true);                                       \n"
      26             :   ;
      27             : 
      28             :   const std::string VARSPEC =
      29             :     "datavar         \n"
      30             :     "  n: Nat;       \n"
      31             :     "                \n"
      32             :     "predvar         \n"
      33             :     "  X: Bool, Pos; \n"
      34           1 :     "  Y: Nat;       \n"
      35             :   ;
      36             : 
      37           1 :   pbes p;
      38           1 :   std::stringstream s(PBESSPEC);
      39           1 :   s >> p;
      40             : 
      41           2 :   pbes_expression x = parse_pbes_expression("X(true, 2) && Y(n+1)", VARSPEC);
      42           1 :   std::cout << "x = " << pbes_system::pp(x) << std::endl;
      43           1 : }
      44             : 
      45           2 : BOOST_AUTO_TEST_CASE(test_parse_pbes_expression)
      46             : {
      47           1 :   data::variable_vector vardecl;
      48           1 :   data::parse_variables("b: Bool; n: Nat;", std::back_inserter(vardecl));
      49           1 :   std::vector<propositional_variable> propvardecl;
      50           2 :   propositional_variable X = parse_propositional_variable("X(b: Bool, n: Nat)", vardecl);
      51           2 :   propositional_variable Y = parse_propositional_variable("Y(n: Nat)", vardecl);
      52           1 :   propvardecl.push_back(X);
      53           1 :   propvardecl.push_back(Y);
      54           2 :   pbes_expression x = parse_pbes_expression("X(true, 2) && Y(n+1)", data::data_specification(), vardecl, propvardecl);
      55           1 :   BOOST_CHECK(pbes_system::pp(x) == "X(true, 2) && Y(n + 1)");
      56           1 : }