LCOV - code coverage report
Current view: top level - pbes/test - find_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 38 38 100.0 %
Date: 2024-03-08 02:52:28 Functions: 7 7 100.0 %
Legend: Lines: hit not hit

          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 Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE find_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/pbes/find.h"
      16             : #include "mcrl2/pbes/detail/parse.h"
      17             : #include "mcrl2/pbes/print.h"
      18             : #include "mcrl2/pbes/txt2pbes.h"
      19             : 
      20             : using namespace mcrl2;
      21             : using namespace mcrl2::pbes_system;
      22             : 
      23             : inline
      24           4 : data::variable nat(const std::string& name)
      25             : {
      26           8 :   return data::variable(core::identifier_string(name), data::sort_nat::nat());
      27             : }
      28             : 
      29             : inline
      30             : data::variable pos(const std::string& name)
      31             : {
      32             :   return data::variable(core::identifier_string(name), data::sort_pos::pos());
      33             : }
      34             : 
      35             : inline
      36             : data::variable bool_(const std::string& name)
      37             : {
      38             :   return data::variable(core::identifier_string(name), data::bool_());
      39             : }
      40             : 
      41           2 : BOOST_AUTO_TEST_CASE(test_find)
      42             : {
      43             :   const std::string VARSPEC =
      44             :     "datavar         \n"
      45             :     "  m: Nat;       \n"
      46             :     "  n: Nat;       \n"
      47             :     "                \n"
      48             :     "predvar         \n"
      49             :     "  X: Bool, Pos; \n"
      50           1 :     "  Y: Nat;       \n"
      51             :     ;
      52             : 
      53           2 :   pbes_expression x = parse_pbes_expression("X(true, 2) && Y(n+1) && Y(m)", VARSPEC);
      54             : 
      55             :   //--- find_all_variables ---//
      56           2 :   data::variable m = nat("m");
      57           2 :   data::variable n = nat("n");
      58           1 :   std::set<data::variable> v = pbes_system::find_all_variables(x);
      59           5 :   std::set<data::variable> v_expected = { m, n };
      60           1 :   BOOST_CHECK(v == v_expected);
      61             : 
      62             :   //--- find_sort_expressions ---//
      63           1 :   std::set<data::sort_expression> s = pbes_system::find_sort_expressions(x);
      64           1 :   std::cout << "s = " << core::detail::print_set(s) << std::endl;
      65           5 :   std::set<data::sort_expression> s_expected = { data::sort_nat::nat(), data::sort_pos::pos() };
      66           1 :   BOOST_CHECK(std::includes(s.begin(), s.end(), s_expected.begin(), s_expected.end()));
      67           1 : }
      68             : 
      69           2 : BOOST_AUTO_TEST_CASE(test_free_variables)
      70             : {
      71             :   const std::string VARSPEC =
      72             :     "datavar         \n"
      73             :     "  n: Nat;       \n"
      74             :     "                \n"
      75             :     "predvar         \n"
      76             :     "  X: Bool, Pos; \n"
      77           1 :     "  Y: Nat;       \n"
      78             :     ;
      79             : 
      80           2 :   pbes_expression x = parse_pbes_expression("forall m:Nat.(X(true, 2) && Y(n+1) && Y(m))", VARSPEC);
      81           2 :   data::variable m = nat("m");
      82           2 :   data::variable n = nat("n");
      83             : 
      84           1 :   std::set<data::variable> v = pbes_system::find_free_variables(x);
      85           4 :   std::set<data::variable> v_expected = { n };
      86           1 :   BOOST_CHECK(v == v_expected);
      87           1 : }
      88             : 
      89           2 : BOOST_AUTO_TEST_CASE(test_find_free_variables)
      90             : {
      91             :   std::string test1 =
      92             :     "pbes                                                                   \n"
      93             :     "                                                                       \n"
      94             :     "nu X(b:Bool, n:Nat) = (val(b) => X(!b, n)) && (val(!b) => X(!b, n+1)); \n"
      95             :     "mu Y(c:Nat, d:Bool) = forall m:Nat. Y(c, true) || X(d, m);             \n"
      96             :     "                                                                       \n"
      97           1 :     "init X(true, 0);                                                       \n"
      98             :     ;
      99             : 
     100           1 :   pbes p = txt2pbes(test1);
     101             : 
     102           1 :   std::set<data::variable> v = find_free_variables(p);
     103           1 :   BOOST_CHECK(v.empty());
     104             : 
     105           1 :   v = find_free_variables(p.equations()[0]);
     106           1 :   BOOST_CHECK(v.empty());
     107             : 
     108           1 :   v = find_free_variables(p.equations()[1]);
     109           1 :   BOOST_CHECK(v.empty());
     110             : 
     111           1 :   v = find_free_variables(p.equations()[0].formula());
     112           1 :   BOOST_CHECK(v.size() == 2);
     113             : 
     114           1 :   v = find_free_variables(p.equations()[1].formula());
     115           1 :   BOOST_CHECK(v.size() == 2);
     116           1 : }

Generated by: LCOV version 1.14