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

Generated by: LCOV version 1.12