LCOV - code coverage report
Current view: top level - bes/test - bes_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 105 105 100.0 %
Date: 2019-09-14 00:54:39 Functions: 8 8 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Jeroen Keiren
       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 bes_test.cpp
      10             : /// \brief Some tests for BES.
      11             : 
      12             : #define BOOST_TEST_MODULE bes_test
      13             : #include "mcrl2/bes/boolean_equation_system.h"
      14             : #include "mcrl2/bes/find.h"
      15             : #include "mcrl2/bes/join.h"
      16             : #include "mcrl2/bes/print.h"
      17             : #include <boost/test/included/unit_test_framework.hpp>
      18             : 
      19             : using namespace mcrl2;
      20             : using namespace mcrl2::bes;
      21             : 
      22             : typedef core::term_traits<boolean_expression> tr;
      23             : 
      24           1 : void test_join()
      25             : {
      26           2 :   boolean_variable X("X");
      27           1 :   const boolean_expression& Z1 = X;
      28           1 :   const boolean_expression& Z2(X);
      29           2 :   boolean_expression Z3;
      30           1 :   Z3 = X;
      31           1 :   Z3=Z2;
      32             : 
      33           2 :   std::set<boolean_expression> s;
      34           1 :   s.insert(boolean_variable("X1"));
      35           1 :   s.insert(boolean_variable("X2"));
      36           2 :   boolean_expression x = join_or(s.begin(), s.end());
      37           1 :   std::cout << "x = " << bes::pp(x) << std::endl;
      38             : 
      39             : #ifdef MCRL2_JOIN_TEST
      40             : // The gcc compiler gives the following error:
      41             : //
      42             : // D:\mcrl2\libraries\core\include/mcrl2/utilities/detail/join.h:54:22: error: call
      43             : // of overloaded 'boolean_expression(const mcrl2::bes::boolean_variable&)' is
      44             : // ambiguous
      45             : //
      46             : // This seems to be triggered by an incorrect optimization, in which the return
      47             : // type of the function false_() is discarded.
      48             : //
      49             :   std::set<boolean_variable> sv;
      50             :   sv.insert(boolean_variable("X1"));
      51             :   sv.insert(boolean_variable("X2"));
      52             :   x = join_or(sv.begin(), sv.end());
      53             :   std::cout << "x = " << bes::pp(x) << std::endl;
      54             : #endif
      55             : 
      56           1 : }
      57             : 
      58           1 : void test_expressions()
      59             : {
      60           2 :   boolean_variable X("X");
      61           2 :   boolean_variable Y("Y");
      62             : 
      63           1 :   BOOST_CHECK(tr::is_prop_var(X));
      64           1 :   BOOST_CHECK(tr::is_prop_var(Y));
      65             : 
      66           2 :   boolean_expression true_(tr::true_());
      67           2 :   boolean_expression false_(tr::false_());
      68           2 :   boolean_expression not_(tr::not_(X));
      69           2 :   boolean_expression and_(tr::and_(X,Y));
      70           2 :   boolean_expression or_(tr::or_(X,Y));
      71           2 :   boolean_expression imp(tr::imp(X,Y));
      72             : 
      73           1 :   BOOST_CHECK(tr::is_true(true_));
      74           1 :   BOOST_CHECK(!tr::is_true(false_));
      75           1 :   BOOST_CHECK(!tr::is_true(not_));
      76           1 :   BOOST_CHECK(!tr::is_true(and_));
      77           1 :   BOOST_CHECK(!tr::is_true(or_));
      78           1 :   BOOST_CHECK(!tr::is_true(imp));
      79             : 
      80           1 :   BOOST_CHECK(!tr::is_false(true_));
      81           1 :   BOOST_CHECK(tr::is_false(false_));
      82           1 :   BOOST_CHECK(!tr::is_false(not_));
      83           1 :   BOOST_CHECK(!tr::is_false(and_));
      84           1 :   BOOST_CHECK(!tr::is_false(or_));
      85           1 :   BOOST_CHECK(!tr::is_false(imp));
      86             : 
      87           1 :   BOOST_CHECK(!tr::is_not(true_));
      88           1 :   BOOST_CHECK(!tr::is_not(false_));
      89           1 :   BOOST_CHECK(tr::is_not(not_));
      90           1 :   BOOST_CHECK(!tr::is_not(and_));
      91           1 :   BOOST_CHECK(!tr::is_not(or_));
      92           1 :   BOOST_CHECK(!tr::is_not(imp));
      93             : 
      94           1 :   BOOST_CHECK(!tr::is_and(true_));
      95           1 :   BOOST_CHECK(!tr::is_and(false_));
      96           1 :   BOOST_CHECK(!tr::is_and(not_));
      97           1 :   BOOST_CHECK(tr::is_and(and_));
      98           1 :   BOOST_CHECK(!tr::is_and(or_));
      99           1 :   BOOST_CHECK(!tr::is_and(imp));
     100             : 
     101           1 :   BOOST_CHECK(!tr::is_or(true_));
     102           1 :   BOOST_CHECK(!tr::is_or(false_));
     103           1 :   BOOST_CHECK(!tr::is_or(not_));
     104           1 :   BOOST_CHECK(!tr::is_or(and_));
     105           1 :   BOOST_CHECK(tr::is_or(or_));
     106           1 :   BOOST_CHECK(!tr::is_or(imp));
     107             : 
     108           1 :   BOOST_CHECK(!tr::is_imp(true_));
     109           1 :   BOOST_CHECK(!tr::is_imp(false_));
     110           1 :   BOOST_CHECK(!tr::is_imp(not_));
     111           1 :   BOOST_CHECK(!tr::is_imp(and_));
     112           1 :   BOOST_CHECK(!tr::is_imp(or_));
     113           1 :   BOOST_CHECK(tr::is_imp(imp));
     114           1 : }
     115             : 
     116           1 : void test_boolean_equation()
     117             : {
     118           2 :   boolean_variable X("X");
     119           2 :   boolean_variable Y("Y");
     120           2 :   boolean_variable Z("Z");
     121             : 
     122           2 :   boolean_equation e(fixpoint_symbol::nu(), X, tr::and_(Y,Z));
     123           1 :   BOOST_CHECK(e.symbol() == fixpoint_symbol::nu());
     124           1 :   BOOST_CHECK(e.variable() == X);
     125           1 :   BOOST_CHECK(e.formula() == tr::and_(Y,Z));
     126             : 
     127             :   // Check for finding variables in the right hand side
     128           2 :   std::set<boolean_variable> expected;
     129           1 :   expected.insert(Y);
     130           1 :   expected.insert(Z);
     131             : 
     132           2 :   std::set<boolean_variable> found;
     133             : 
     134           1 :   find_boolean_variables(Y, std::inserter(found, found.end()));
     135           1 :   find_boolean_variables(Z, std::inserter(found, found.end()));
     136           1 :   BOOST_CHECK(found == expected);
     137             : 
     138           1 :   find_boolean_variables(tr::and_(Y,Z), std::inserter(found, found.end()));
     139           1 :   BOOST_CHECK(found == expected);
     140             : 
     141           1 :   found.clear();
     142           1 :   find_boolean_variables(e.formula(), std::inserter(found, found.end()));
     143           1 :   BOOST_CHECK(found == expected);
     144           1 : }
     145             : 
     146           1 : void test_bes()
     147             : {
     148           2 :   boolean_variable X("X");
     149           2 :   boolean_variable Y("Y");
     150           2 :   boolean_variable Z("Z");
     151             : 
     152           2 :   boolean_equation eqX(fixpoint_symbol::nu(), X, tr::and_(X, tr::and_(Y,Z)));
     153           2 :   boolean_equation eqY(fixpoint_symbol::nu(), Y, tr::and_(X, Y));
     154           2 :   boolean_equation eqZ(fixpoint_symbol::mu(), Z, tr::or_(Z, X));
     155           2 :   std::vector<boolean_equation> eqns;
     156           1 :   eqns.push_back(eqX);
     157           1 :   eqns.push_back(eqY);
     158           1 :   eqns.push_back(eqZ);
     159             : 
     160           2 :   boolean_equation_system bes(eqns, X);
     161           1 :   BOOST_CHECK(bes.is_closed());
     162             : 
     163           1 :   bes::pp(bes);
     164             : 
     165           2 :   std::set<boolean_variable> occurring_variables = bes.occurring_variables();
     166           1 :   BOOST_CHECK(occurring_variables.size() == 3);
     167           1 : }
     168             : 
     169           3 : BOOST_AUTO_TEST_CASE(test_main)
     170             : {
     171           1 :   test_expressions();
     172           1 :   test_boolean_equation();
     173           1 :   test_join();
     174           1 :   test_bes();
     175           4 : }

Generated by: LCOV version 1.12