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

Generated by: LCOV version 1.12