LCOV - code coverage report
Current view: top level - pbes/test - eqelm_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 39 47 83.0 %
Date: 2020-09-22 00:46:14 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 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 eqelm_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE eqelm_test
      13             : #include <boost/test/included/unit_test_framework.hpp>
      14             : #include "mcrl2/pbes/detail/pbessolve.h"
      15             : #include "mcrl2/pbes/detail/pbes_property_map.h"
      16             : #include "mcrl2/pbes/eqelm.h"
      17             : #include "mcrl2/pbes/rewriter.h"
      18             : #include "mcrl2/pbes/txt2pbes.h"
      19             : 
      20             : using namespace mcrl2;
      21             : using namespace mcrl2::pbes_system;
      22             : 
      23             : // Example provided by Frank Stappers
      24           1 : std::string t1 =
      25             :   "pbes nu X(m, n: Nat) =                  \n"
      26             :   "        val(n == m) && X(m + 1, n + 1); \n"
      27             :   "                                        \n"
      28             :   " init X(0, 0);                          \n"
      29             :   ;
      30           1 : std::string x1 = "binding_variables = X(m: Nat)";
      31             : 
      32             : // Example provided by Tim Willemse.
      33             : // The parameters n and m are not equivalent, and thus should not
      34             : // be removed.
      35           1 : std::string t2 =
      36             :   "pbes nu X(n,m: Nat) =          \n"
      37             :   "       forall p: Nat. X(m, p); \n"
      38             :   "                               \n"
      39             :   "init X(0, 0);                  \n"
      40             :   ;
      41           1 : std::string x2 = "binding_variables = X(n,m: Nat)";
      42             : 
      43           2 : void test_pbes(const std::string& pbes_spec,
      44             :                const std::string& expected_result,
      45             :                bool /* compute_conditions */,
      46             :                bool /* remove_equations = true */,
      47             :                const std::string& msg = "")
      48             : {
      49             :   typedef simplify_data_rewriter<data::rewriter> my_pbes_rewriter;
      50             : 
      51           4 :   pbes p = txt2pbes(pbes_spec);
      52           4 :   pbes q = p;
      53             : 
      54             :   // data rewriter
      55           4 :   data::rewriter datar(q.data());
      56             : 
      57             :   // pbes rewriter
      58           2 :   my_pbes_rewriter pbesr(datar);
      59             : 
      60             :   // constelm algorithm
      61           4 :   pbes_eqelm_algorithm<pbes_expression, data::rewriter, my_pbes_rewriter> algorithm(datar, pbesr);
      62             : 
      63             :   // run the algorithm
      64           2 :   algorithm.run(q);
      65           2 :   BOOST_CHECK(q.is_well_typed());
      66           2 :   if (!q.is_well_typed())
      67             :   {
      68           0 :     std::cerr << pbes_system::pp(q) << std::endl;
      69             :   }
      70             : 
      71           4 :   pbes_system::detail::pbes_property_map info1(q);
      72           4 :   pbes_system::detail::pbes_property_map info2(expected_result);
      73           4 :   std::string diff = info1.compare(info2);
      74           2 :   if (!diff.empty())
      75             :   {
      76           0 :     std::cerr << "\n------ FAILED TEST ------ " << msg << std::endl;
      77           0 :     std::cerr << "--- expected result" << std::endl;
      78           0 :     std::cerr << expected_result << std::endl;
      79           0 :     std::cerr << "--- found result" << std::endl;
      80           0 :     std::cerr << info1.to_string() << std::endl;
      81           0 :     std::cerr << "--- differences" << std::endl;
      82           0 :     std::cerr << diff << std::endl;
      83             :   }
      84           2 :   BOOST_CHECK(diff.empty());
      85             : 
      86           2 : }
      87             : 
      88           1 : void test_eqelm(const std::string& pbes_spec, const bool expected_outcome)
      89             : {
      90             :   typedef simplify_data_rewriter<data::rewriter> my_pbes_rewriter;
      91             : 
      92           2 :   pbes p = txt2pbes(pbes_spec);
      93           2 :   pbes q = p;
      94             : 
      95           2 :   data::rewriter datar(q.data());
      96           1 :   my_pbes_rewriter pbesr(datar);
      97           2 :   pbes_eqelm_algorithm<pbes_expression, data::rewriter, my_pbes_rewriter> algorithm(datar, pbesr);
      98           1 :   algorithm.run(q);
      99             : 
     100           1 :   bool solution_p = pbes_system::detail::pbessolve(p);
     101           1 :   bool solution_q = pbes_system::detail::pbessolve(q);
     102           1 :   BOOST_CHECK(solution_p == expected_outcome);
     103           1 :   BOOST_CHECK(solution_q == expected_outcome);
     104           1 : }
     105             : 
     106           1 : std::string random1 =
     107             :   "pbes mu X0(b: Bool) =                            \n"
     108             :   "       (X1(0, 0) || false) && true;              \n"
     109             :   "     mu X1(n,m: Nat) =                           \n"
     110             :   "       (X1(m + 1, 0) || false) || val(!(n < 2)); \n"
     111             :   "                                                 \n"
     112             :   "init X0(true);                                   \n"
     113             :   ;
     114             : 
     115           3 : BOOST_AUTO_TEST_CASE(eqelm_test1)
     116             : {
     117           1 :   bool compute_conditions = false;
     118           1 :   bool remove_equations = true;
     119           1 :   test_pbes(t1, x1, compute_conditions, remove_equations, "test 1");
     120           1 :   test_pbes(t2, x2, compute_conditions, remove_equations, "test 2");
     121           1 :   test_eqelm(random1, false);
     122           4 : }

Generated by: LCOV version 1.13