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/consistency.h"
      16             : #include "mcrl2/lps/find.h"
      17             : #include "mcrl2/lps/parse.h"
      18             : 
      19             : using namespace mcrl2;
      20             : using namespace mcrl2::lps;
      21             : 
      22             : inline
      23             : data::variable nat(const std::string& name)
      24             : {
      25             :   return data::variable(core::identifier_string(name), data::sort_nat::nat());
      26             : }
      27             : 
      28             : inline
      29             : data::variable pos(const std::string& name)
      30             : {
      31             :   return data::variable(core::identifier_string(name), data::sort_pos::pos());
      32             : }
      33             : 
      34             : inline
      35             : data::variable bool_(const std::string& name)
      36             : {
      37             :   return data::variable(core::identifier_string(name), data::bool_());
      38             : }
      39             : 
      40             : template <typename T>
      41           2 : std::string print_set(const std::set<T>& v)
      42             : {
      43           2 :   std::set<std::string> s;
      44           5 :   for (const T& v_i: v)
      45             :   {
      46           3 :     s.insert(data::pp(v_i));
      47             :   }
      48           4 :   return core::detail::print_set(s);
      49           2 : }
      50             : 
      51           2 : BOOST_AUTO_TEST_CASE(test_find)
      52             : {
      53             :   using utilities::detail::contains;
      54             : 
      55             :   std::string SPEC =
      56             :     "glob                      \n"
      57             :     "  m: Nat;                 \n"
      58             :     "                          \n"
      59             :     "act                       \n"
      60             :     "  a: Nat;                 \n"
      61             :     "                          \n"
      62             :     "proc                      \n"
      63             :     "  P(n:Nat) = a(m).P(n+1); \n"
      64             :     "                          \n"
      65           1 :     "init P(0);                \n"
      66             :   ;
      67             : 
      68           1 :   specification lpsspec = parse_linear_process_specification(SPEC);
      69           1 :   action_summand s = lpsspec.process().action_summands().front();
      70           1 :   process::action a = s.multi_action().actions().front();
      71             : 
      72           1 :   BOOST_CHECK_EQUAL(print_set(lps::find_all_variables(s)), "{ m, n }");
      73           1 :   BOOST_CHECK_EQUAL(print_set(lps::find_sort_expressions(a)), "{ Nat }");
      74           1 : }
      75             : 
      76           2 : BOOST_AUTO_TEST_CASE(test_free_variables)
      77             : {
      78           1 :   std::set<data::variable> free_variables;
      79             : 
      80             :   lps::specification specification(parse_linear_process_specification(
      81             :                                      "act a : Bool;\n"
      82             :                                      "proc X = a((forall x : Nat. exists y : Nat. x < y)).X;\n"
      83             :                                      "init X;\n"
      84           2 :                                    ));
      85             : 
      86           1 :   free_variables = find_free_variables(specification.process());
      87           1 :   BOOST_CHECK(free_variables.find(data::variable("x", data::sort_nat::nat())) == free_variables.end());
      88           1 :   BOOST_CHECK(free_variables.find(data::variable("y", data::sort_nat::nat())) == free_variables.end());
      89             : 
      90           2 :   specification = parse_linear_process_specification(
      91             :                     "act a;\n"
      92             :                     "proc X(z : Bool) = (z && (forall x : Nat. exists y : Nat. x < y)) -> a.X(!z);\n"
      93             :                     "init X(true);\n"
      94           1 :                   );
      95           1 :   free_variables = find_free_variables(specification);
      96           1 :   BOOST_CHECK(free_variables.empty());
      97             : 
      98           1 :   free_variables = find_free_variables(specification.process());
      99           1 :   BOOST_CHECK(free_variables.empty());
     100             : 
     101           1 :   free_variables = find_free_variables(specification.process().action_summands().front());
     102           1 :   BOOST_CHECK(free_variables.size() == 1);
     103           1 :   BOOST_CHECK(free_variables.find(data::variable("z", data::bool_())) != free_variables.end());
     104             : 
     105           1 :   BOOST_CHECK(check_well_typedness(specification));
     106           1 : }
     107             : 
     108           2 : BOOST_AUTO_TEST_CASE(test_search)
     109             : {
     110             :   lps::specification spec(parse_linear_process_specification(
     111             :                             "glob dc: Nat;\n"
     112             :                             "act a : Bool;\n"
     113             :                             "proc X = a((forall x : Nat. exists y : Nat. (x < y) && (y < dc))).X;\n"
     114             :                             "init X;\n"
     115           2 :                           ));
     116           2 :   data::variable x("x", data::sort_nat::nat());
     117           1 :   BOOST_CHECK(!lps::search_free_variable(spec.process().action_summands(), x));
     118             : 
     119           2 :   data::variable y("y", data::sort_nat::nat());
     120           1 :   BOOST_CHECK(!lps::search_free_variable(spec.process().action_summands(), y));
     121             : 
     122           2 :   data::variable dc("dc", data::sort_nat::nat());
     123           1 :   BOOST_CHECK(lps::search_free_variable(spec.process().action_summands(), dc));
     124           1 : }
     125             : 
     126           2 : BOOST_AUTO_TEST_CASE(test_search_sort_expression)
     127             : {
     128             :   std::string text =
     129             :     "act a: List(Bool);                   \n"
     130             :     "proc X(x: List(Bool)) = a(x) . X(x); \n"
     131           1 :     "init X([true]);                      \n"
     132             :     ;
     133           1 :   lps::specification spec = parse_linear_process_specification(text);
     134           2 :   data::sort_expression s = data::parse_sort_expression("List(Bool)");
     135           1 :   BOOST_CHECK(data::search_sort_expression(spec.data().sorts(), s));
     136           1 : }