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

          Line data    Source code
       1             : // Author(s): Wieger Wesselink
       2             : // Copyright: see the accompanying file COPYING.
       3             : //
       4             : // Distributed under the Boost Software License, Version 1.0.
       5             : // (See accompanying file LICENSE_1_0.txt or copy at
       6             : // http://www.boost.org/LICENSE_1_0.txt)
       7             : //
       8             : /// \file remove_parameters_test.cpp
       9             : /// \brief Tests for removing parameters.
      10             : 
      11             : #define BOOST_TEST_MODULE remove_parameters_test
      12             : #include <boost/test/included/unit_test.hpp>
      13             : 
      14             : #include "mcrl2/pbes/detail/test_utility.h"
      15             : #include "mcrl2/pbes/remove_parameters.h"
      16             : 
      17             : using namespace mcrl2;
      18             : using namespace mcrl2::pbes_system;
      19             : using namespace mcrl2::pbes_system::detail;
      20             : 
      21           2 : BOOST_AUTO_TEST_CASE(test_propositional_variable)
      22             : {
      23           6 :   data::variable_list d = { nat("n"), pos("p"), bool_("b"), bool_("c") } ;
      24           2 :   propositional_variable X = propvar("X", d);
      25           1 :   std::vector<std::size_t> v;
      26           1 :   v.push_back(1);
      27           1 :   v.push_back(3);
      28           1 :   propositional_variable X1 = pbes_system::remove_parameters(X, v);
      29           4 :   data::variable_list d1 = { nat("n"), bool_("b") };
      30           1 :   BOOST_CHECK(X1 == propvar("X", d1));
      31           1 : }
      32             : 
      33           2 : BOOST_AUTO_TEST_CASE(test_propositional_variable_instantiation)
      34             : {
      35           6 :   data::data_expression_list d = { nat("n"), pos("p"), bool_("b"), bool_("c") } ;
      36           2 :   propositional_variable_instantiation X = propvarinst("X", d);
      37           1 :   std::vector<std::size_t> v;
      38           1 :   v.push_back(1);
      39           1 :   v.push_back(3);
      40           1 :   propositional_variable_instantiation X1 = pbes_system::remove_parameters(X, v);
      41           4 :   data::data_expression_list d1 = { nat("n"), bool_("b") };
      42           1 :   BOOST_CHECK(X1 == propvarinst("X", d1));
      43           1 : }
      44             : 
      45           2 : BOOST_AUTO_TEST_CASE(test_pbes_expression)
      46             : {
      47           4 :   data::variable_list d1 = { nat("m"), bool_("b") };
      48           5 :   data::variable_list d2 = { nat("m"), bool_("b"), nat("p") } ;
      49           2 :   propositional_variable X1 = propvar("X1", d1);
      50           2 :   propositional_variable X2 = propvar("X2", d2);
      51             : 
      52           4 :   data::data_expression_list e1 = { data::sort_nat::plus(nat("m"), nat("n")), bool_("b") };
      53           5 :   data::data_expression_list e2 = { data::sort_nat::times(nat("m"), nat("n")), bool_("b"), nat("p") };
      54           2 :   propositional_variable_instantiation x1 = propvarinst("X1", e1);
      55           2 :   propositional_variable_instantiation x2 = propvarinst("X2", e2);
      56             : 
      57           1 :   pbes_expression p = and_(x1, x2);
      58             : 
      59           1 :   std::map<core::identifier_string, std::vector<std::size_t> > to_be_removed;
      60           1 :   std::vector<std::size_t> v1;
      61           1 :   v1.push_back(1);
      62           1 :   to_be_removed[X1.name()] = v1;
      63           1 :   std::vector<std::size_t> v2;
      64           1 :   v2.push_back(0);
      65           1 :   v2.push_back(2);
      66           1 :   to_be_removed[X2.name()] = v2;
      67             : 
      68           1 :   pbes_expression q = pbes_system::remove_parameters(p, to_be_removed);
      69             : 
      70           1 :   pbes_expression r;
      71             :   {
      72           3 :     data::variable_list d1 = { nat("m") };
      73           3 :     data::variable_list d2 = { bool_("b") };
      74           2 :     propositional_variable X1 = propvar("X1", d1);
      75           2 :     propositional_variable X2 = propvar("X2", d2);
      76             : 
      77           3 :     data::data_expression_list e1 = { data::data_expression(data::sort_nat::plus(nat("m"), nat("n"))) };
      78           3 :     data::data_expression_list e2 = { data::data_expression(bool_("b")) };
      79           2 :     propositional_variable_instantiation x1 = propvarinst("X1", e1);
      80           2 :     propositional_variable_instantiation x2 = propvarinst("X2", e2);
      81             : 
      82           1 :     r = and_(x1, x2);
      83           1 :   }
      84           1 :   BOOST_CHECK(q == r);
      85           1 : }

Generated by: LCOV version 1.14