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 modal_formula_find_test.cpp
      10             : /// \brief Test for find functions.
      11             : 
      12             : #define BOOST_TEST_MODULE modal_formula_find_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/modal_formula/find.h"
      16             : #include "mcrl2/modal_formula/parse.h"
      17             : 
      18             : using namespace mcrl2;
      19             : using namespace mcrl2::state_formulas;
      20             : 
      21             : std::string SPEC =
      22             :   "glob                      \n"
      23             :   "  m: Nat;                 \n"
      24             :   "                          \n"
      25             :   "act                       \n"
      26             :   "  a: Nat;                 \n"
      27             :   "                          \n"
      28             :   "proc                      \n"
      29             :   "  P(n:Nat) = a(m).P(n+1); \n"
      30             :   "                          \n"
      31             :   "init P(0);                \n"
      32             :   ;
      33             : 
      34             : inline
      35             : data::variable nat(const std::string& name)
      36             : {
      37             :   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           3 : data::variable bool_(const std::string& name)
      48             : {
      49           6 :   return data::variable(core::identifier_string(name), data::sort_bool::bool_());
      50             : }
      51             : 
      52           2 : BOOST_AUTO_TEST_CASE(test_find)
      53             : {
      54           1 :   lps::stochastic_specification spec = lps::stochastic_specification(lps::parse_linear_process_specification(SPEC));
      55           2 :   state_formula f = parse_state_formula("(mu X. X) && (forall b:Bool. true)", spec, false);
      56             : 
      57             :   //--- find_all_variables ---//
      58           2 :   data::variable b = bool_("b");
      59           1 :   std::set<data::variable> v = state_formulas::find_all_variables(f);
      60           1 :   BOOST_CHECK(v.find(b) != v.end());
      61             : 
      62             :   //--- find_sort_expressions ---//
      63           1 :   std::set<data::sort_expression> e = state_formulas::find_sort_expressions(f);
      64           1 :   std::cout << "e.size() = " << e.size() << std::endl;
      65           1 :   BOOST_CHECK(std::find(e.begin(), e.end(), data::sort_bool::bool_()) != e.end());
      66           1 : }
      67             : 
      68           2 : BOOST_AUTO_TEST_CASE(test_free_variables)
      69             : {
      70           2 :   variable X("X", data::data_expression_list());
      71           2 :   data::variable b = bool_("b");
      72           2 :   data::variable c = bool_("c");
      73           1 :   data::data_expression phi = data::equal_to(b, c);
      74           2 :   data::variable_list v { b };
      75           2 :   state_formula f = forall(v, phi);
      76           1 :   std::set<data::variable> free_variables = state_formulas::find_free_variables(f);
      77           1 :   std::cout << "free variables: " << core::detail::print_set(free_variables) << std::endl;
      78           1 :   BOOST_CHECK(free_variables.find(b) == free_variables.end());
      79           1 :   BOOST_CHECK(free_variables.find(c) != free_variables.end());
      80           1 : }