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 <boost/test/included/unit_test.hpp>
      14             : #include "mcrl2/pbes/find.h"
      15             : #include "mcrl2/pbes/join.h"
      16             : #include "mcrl2/pbes/print.h"
      17             : 
      18             : using namespace mcrl2;
      19             : using namespace mcrl2::pbes_system;
      20             : 
      21             : typedef core::term_traits<pbes_expression> tr;
      22             : 
      23           1 : void test_join()
      24             : {
      25           2 :   propositional_variable X("X");
      26           1 :   const pbes_expression& Z1 = propositional_variable_instantiation(X.name());
      27           1 :   const pbes_expression& Z2(propositional_variable_instantiation(X.name()));
      28           1 :   pbes_expression Z3;
      29           1 :   Z3 = propositional_variable_instantiation(X.name());
      30           1 :   Z3=Z2;
      31             : 
      32           1 :   std::set<pbes_expression> s;
      33           1 :   s.insert(propositional_variable_instantiation("X1"));
      34           1 :   s.insert(propositional_variable_instantiation("X2"));
      35           1 :   pbes_expression x = join_or(s.begin(), s.end());
      36           1 :   std::cout << "x = " << pbes_system::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 'pbes_expression(const mcrl2::pbes_system::propositional_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<propositional_variable> sv;
      49             :   sv.insert(propositional_variable("X1"));
      50             :   sv.insert(propositional_variable("X2"));
      51             :   x = join_or(sv.begin(), sv.end());
      52             :   std::cout << "x = " << pbes_system::pp(x) << std::endl;
      53             : #endif
      54             : 
      55           1 : }
      56             : 
      57           1 : void test_expressions()
      58             : {
      59           2 :   propositional_variable_instantiation X("X");
      60           2 :   propositional_variable_instantiation Y("Y");
      61             : 
      62           1 :   BOOST_CHECK(tr::is_prop_var(X));
      63           1 :   BOOST_CHECK(tr::is_prop_var(Y));
      64             : 
      65           1 :   pbes_expression true_(tr::true_());
      66           1 :   pbes_expression false_(tr::false_());
      67           1 :   pbes_expression not_(tr::not_(X));
      68           1 :   pbes_expression and_(tr::and_(X,Y));
      69           1 :   pbes_expression or_(tr::or_(X,Y));
      70           1 :   pbes_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 :   propositional_variable X("X");
     118           2 :   propositional_variable_instantiation Y("Y");
     119           2 :   propositional_variable_instantiation Z("Z");
     120             : 
     121           2 :   pbes_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           1 :   std::set<propositional_variable_instantiation> expected;
     128           1 :   expected.insert(Y);
     129           1 :   expected.insert(Z);
     130             : 
     131           1 :   std::set<propositional_variable_instantiation> found;
     132             : 
     133           1 :   find_propositional_variable_instantiations(Y, std::inserter(found, found.end()));
     134           1 :   find_propositional_variable_instantiations(Z, std::inserter(found, found.end()));
     135           1 :   BOOST_CHECK(found == expected);
     136             : 
     137           1 :   find_propositional_variable_instantiations(tr::and_(Y,Z), std::inserter(found, found.end()));
     138           1 :   BOOST_CHECK(found == expected);
     139             : 
     140           1 :   found.clear();
     141           1 :   find_propositional_variable_instantiations(e.formula(), std::inserter(found, found.end()));
     142           1 :   BOOST_CHECK(found == expected);
     143           1 : }
     144             : 
     145           1 : void test_bes()
     146             : {
     147           2 :   propositional_variable X("X");
     148           2 :   propositional_variable Y("Y");
     149           2 :   propositional_variable Z("Z");
     150             : 
     151           2 :   pbes_equation eqX(fixpoint_symbol::nu(), X, tr::and_(propositional_variable_instantiation(X.name()), tr::and_(propositional_variable_instantiation(Y.name()),propositional_variable_instantiation(Z.name()))));
     152           2 :   pbes_equation eqY(fixpoint_symbol::nu(), Y, tr::and_(propositional_variable_instantiation(X.name()), propositional_variable_instantiation(Y.name())));
     153           2 :   pbes_equation eqZ(fixpoint_symbol::mu(), Z, tr::or_(propositional_variable_instantiation(Z.name()), propositional_variable_instantiation(X.name())));
     154           1 :   std::vector<pbes_equation> eqns;
     155           1 :   eqns.push_back(eqX);
     156           1 :   eqns.push_back(eqY);
     157           1 :   eqns.push_back(eqZ);
     158             : 
     159           2 :   pbes_system::pbes bes(data::data_specification(), eqns, propositional_variable_instantiation(X.name()));
     160           1 :   BOOST_CHECK(bes.is_closed());
     161             : 
     162           1 :   pbes_system::pp(bes);
     163             : 
     164           1 :   std::set<propositional_variable> occurring_variables = bes.occurring_variables();
     165           1 :   BOOST_CHECK(occurring_variables.size() == 3);
     166           1 : }
     167             : 
     168           2 : BOOST_AUTO_TEST_CASE(test_main)
     169             : {
     170           1 :   test_expressions();
     171           1 :   test_boolean_equation();
     172           1 :   test_join();
     173           1 :   test_bes();
     174           1 : }