LCOV - code coverage report
Current view: top level - bes/test - normal_form_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 19 19 100.0 %
Date: 2019-09-14 00:54:39 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 normal_form_test.cpp
      10             : /// \brief Tests for transformations into normal form.
      11             : 
      12             : #define BOOST_TEST_MODULE normal_form_test
      13             : #include "mcrl2/bes/boolean_equation_system.h"
      14             : #include "mcrl2/bes/normal_forms.h"
      15             : #include "mcrl2/bes/parse.h"
      16             : #include "mcrl2/bes/print.h"
      17             : #include <boost/test/included/unit_test_framework.hpp>
      18             : #include <sstream>
      19             : #include <string>
      20             : 
      21             : using namespace mcrl2;
      22             : using namespace mcrl2::bes;
      23             : 
      24           4 : void test_standard_recursive_form(const std::string& bes_spec, bool recursive_form = false)
      25             : {
      26           8 :   boolean_equation_system b;
      27           8 :   std::stringstream from(bes_spec);
      28           4 :   from >> b;
      29           4 :   std::cout << "before\n" << bes::pp(b) << std::endl;
      30             : 
      31           4 :   make_standard_form(b, recursive_form);
      32           4 :   std::cout << "after\n" << bes::pp(b) << std::endl;
      33           4 : }
      34             : 
      35           1 : void test_standard_recursive_form()
      36             : {
      37             :   std::string bes1 =
      38             :     "pbes              \n"
      39             :     "                  \n"
      40             :     "nu X1 = X2 && X1; \n"
      41             :     "mu X2 = X1 || X2; \n"
      42             :     "                  \n"
      43           2 :     "init X1;          \n"
      44             :     ;
      45           1 :   test_standard_recursive_form(bes1, false);
      46           1 :   test_standard_recursive_form(bes1, true);
      47             : 
      48             :   std::string bes2 =
      49             :     "pbes                    \n"
      50             :     "                        \n"
      51             :     "nu X1 = X2 && true;     \n"
      52             :     "mu X2 = X1 || X2 && X1; \n"
      53             :     "                        \n"
      54           2 :     "init X1;                \n"
      55             :     ;
      56             : 
      57           1 :   test_standard_recursive_form(bes2, false);
      58           1 :   test_standard_recursive_form(bes2, true);
      59             : 
      60           1 : }
      61             : 
      62           3 : BOOST_AUTO_TEST_CASE(test_main)
      63             : {
      64           1 :   test_standard_recursive_form();
      65           4 : }

Generated by: LCOV version 1.12