LCOV - code coverage report
Current view: top level - bes/test - boolean_expression_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 55 55 100.0 %
Date: 2019-09-14 00:54:39 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 boolean_expression_test.cpp
      10             : /// \brief Test for boolean expressions.
      11             : 
      12             : #define BOOST_TEST_MODULE boolean_expression_test
      13             : #include "mcrl2/bes/bes2pbes.h"
      14             : #include "mcrl2/bes/boolean_equation_system.h"
      15             : #include "mcrl2/bes/io.h"
      16             : #include "mcrl2/bes/print.h"
      17             : #include <boost/test/included/unit_test_framework.hpp>
      18             : #include <cstdio>
      19             : #include <iostream>
      20             : #include <string>
      21             : 
      22             : using namespace mcrl2;
      23             : 
      24           1 : void test_boolean_expressions()
      25             : {
      26             :   using namespace bes;
      27             :   typedef core::term_traits<boolean_expression> tr;
      28             : 
      29           2 :   boolean_variable X1("X1");
      30           2 :   boolean_variable X2("X2");
      31           2 :   boolean_expression t1 = tr::and_(X1, X2);
      32           2 :   boolean_equation e1(fixpoint_symbol::mu(), X1, tr::imp(X1, X2));
      33           2 :   boolean_equation e2(fixpoint_symbol::nu(), X2, tr::or_(X1, X2));
      34           1 :   std::cout << bes::pp(e1) << std::endl;
      35           1 :   std::cout << bes::pp(e2) << std::endl;
      36             : 
      37           2 :   boolean_equation_system p;
      38           1 :   p.equations().push_back(e1);
      39           1 :   p.equations().push_back(e2);
      40           1 :   p.initial_state() = X1;
      41           1 :   std::cout << "----------------" << std::endl;
      42           1 :   std::cout << bes::pp(p) << std::endl;
      43             : 
      44           2 :   std::string filename = "boolean_expression_test.out";
      45           1 :   save_bes(p, filename);
      46           2 :   boolean_equation_system q;
      47           1 :   load_bes(q, filename);
      48           1 :   BOOST_CHECK(p == q);
      49           1 :   remove(filename.c_str());
      50           1 : }
      51             : 
      52           1 : void test_bes2pbes()
      53             : {
      54             :   using namespace bes;
      55             :   typedef core::term_traits<boolean_expression> tr;
      56             : 
      57           2 :   boolean_variable X1("X1");
      58           2 :   boolean_variable X2("X2");
      59           2 :   boolean_variable X3("X3");
      60           2 :   boolean_expression t1 = tr::and_(X1, X2);
      61           2 :   boolean_equation e1(fixpoint_symbol::mu(), X1, tr::imp(X1, X2));
      62           2 :   boolean_equation e2(fixpoint_symbol::nu(), X2, tr::or_(X1, X2));
      63           2 :   boolean_equation e3(fixpoint_symbol::nu(), X3, tr::false_());
      64           1 :   std::cout << bes::pp(e1) << std::endl;
      65           1 :   std::cout << bes::pp(e2) << std::endl;
      66           1 :   std::cout << bes::pp(e3) << std::endl;
      67             : 
      68           2 :   boolean_equation_system p;
      69           1 :   p.equations().push_back(e1);
      70           1 :   p.equations().push_back(e2);
      71           1 :   p.equations().push_back(e3);
      72           1 :   p.initial_state() = X1;
      73           1 :   std::cout << "----------------" << std::endl;
      74           1 :   std::cout << bes::pp(p) << std::endl;
      75             : 
      76           2 :   pbes_system::pbes q = bes2pbes(p);
      77           1 :   std::cout << "----------------" << std::endl;
      78           1 :   std::cout << q << std::endl;
      79           1 : }
      80             : 
      81           1 : void test_precedence()
      82             : {
      83             :   using namespace bes;
      84             :   typedef core::term_traits<boolean_expression> tr;
      85           2 :   boolean_variable X1("X1");
      86           2 :   boolean_variable X2("X2");
      87           2 :   boolean_expression t = tr::and_(X1, X2);
      88           2 :   std::string s = bes::pp(t);
      89           1 :   BOOST_CHECK(s == "X1 && X2");
      90           1 : }
      91             : 
      92           3 : BOOST_AUTO_TEST_CASE(test_main)
      93             : {
      94           1 :   test_boolean_expressions();
      95           1 :   test_bes2pbes();
      96           1 :   test_precedence();
      97           4 : }

Generated by: LCOV version 1.12