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 find_test.cpp
      10             : /// \brief Test for find functions.
      11             : 
      12             : #define BOOST_TEST_MODULE find_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/data/detail/print_utility.h"
      16             : #include "mcrl2/process/find.h"
      17             : #include "mcrl2/process/parse.h"
      18             : 
      19             : using namespace mcrl2;
      20             : using namespace mcrl2::process;
      21             : 
      22             : std::string DATA_DECL =
      23             :   "glob                   \n"
      24             :   "  m: Nat;              \n"
      25             :   "                       \n"
      26             :   "act                    \n"
      27             :   "  a: Nat;              \n"
      28             :   ;
      29             : 
      30             : std::string PROC_DECL =
      31             :   "proc P(n:Nat);         \n"
      32             :   ;
      33             : 
      34             : inline
      35           1 : data::variable nat(const std::string& name)
      36             : {
      37           2 :   return data::variable(core::identifier_string(name), data::sort_nat::nat());
      38             : }
      39             : 
      40             : inline
      41             : data::variable pos(const std::string& name)
      42             : {
      43             :   return data::variable(core::identifier_string(name), data::sort_pos::pos());
      44             : }
      45             : 
      46             : inline
      47           1 : data::variable bool_(const std::string& name)
      48             : {
      49           2 :   return data::variable(core::identifier_string(name), data::sort_bool::bool_());
      50             : }
      51             : 
      52           1 : void test_find()
      53             : {
      54           2 :   process_expression x = parse_process_expression("a(m).P(0)", DATA_DECL, PROC_DECL);
      55             : 
      56             :   //--- find_all_variables ---//
      57           2 :   data::variable m = nat("m");
      58           1 :   std::set<data::variable> v = process::find_all_variables(x);
      59           1 :   BOOST_CHECK(v.find(m) != v.end());
      60             : 
      61             :   //--- find_sort_expressions ---//
      62           1 :   std::set<data::sort_expression> e = process::find_sort_expressions(x);
      63           1 :   BOOST_CHECK(std::find(e.begin(), e.end(), data::sort_nat::nat()) != e.end());
      64           1 :   BOOST_CHECK(std::find(e.begin(), e.end(), data::sort_pos::pos()) == e.end());
      65             : 
      66           1 : }
      67             : 
      68           1 : void test_free_variables()
      69             : {
      70           2 :   data::variable b = bool_("b");
      71           2 :   data::data_expression_list d = { b };
      72           3 :   process_identifier P(core::identifier_string("P"), { b });
      73           1 :   process_instance pi(P, d);
      74             : 
      75           1 :   std::set<data::variable> free_variables = process::find_free_variables(pi);
      76           1 :   std::cout << "free variables: " << core::detail::print_set(free_variables) << std::endl;
      77           1 :   BOOST_CHECK(free_variables.find(b) != free_variables.end());
      78           1 : }
      79             : 
      80           2 : BOOST_AUTO_TEST_CASE(test_main)
      81             : {
      82           1 :   test_find();
      83           1 :   test_free_variables();
      84           1 : }