LCOV - code coverage report
Current view: top level - bes/test - solve_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 24 24 100.0 %
Date: 2019-06-20 00:49:45 Functions: 10 10 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 solve_test.cpp
      10             : /// \brief Test for BES solvers.
      11             : 
      12             : #include "mcrl2/bes/gauss_elimination.h"
      13             : #include "mcrl2/bes/parse.h"
      14             : #include "mcrl2/bes/print.h"
      15             : #include "mcrl2/bes/small_progress_measures.h"
      16             : #include <boost/test/included/unit_test_framework.hpp>
      17             : #include <sstream>
      18             : #include <string>
      19             : 
      20             : using namespace mcrl2;
      21             : using namespace mcrl2::bes;
      22             : 
      23           3 : void run_all_algorithms(std::string const& b, bool expected_outcome)
      24             : {
      25           6 :   boolean_equation_system b1;
      26           6 :   std::stringstream from;
      27           3 :   from << "pbes\n" << b << std::endl;
      28           3 :   from >> b1;
      29             : 
      30           3 :   std::clog << "solving the following input bes: \n" << bes::pp(b1) << std::endl;
      31             : 
      32           3 :   BOOST_CHECK_EQUAL(small_progress_measures(b1), expected_outcome);
      33           3 :   BOOST_CHECK_EQUAL(gauss_elimination(b1), expected_outcome);
      34           3 : }
      35             : 
      36           3 : BOOST_AUTO_TEST_CASE(test_simple_nu_mu)
      37             : {
      38             :   std::string b(
      39             :     "mu X1 = X2;\n"
      40             :     "nu X2 = X1;\n"
      41             :     "init X1;\n"
      42           2 :   );
      43           1 :   run_all_algorithms(b, false);
      44           1 : }
      45             : 
      46           3 : BOOST_AUTO_TEST_CASE(test_simple_mu_nu)
      47             : {
      48             :   std::string b(
      49             :     "nu X1 = X2;\n"
      50             :     "mu X2 = X1;\n"
      51             :     "init X1;\n"
      52           2 :   );
      53           1 :   run_all_algorithms(b, true);
      54           1 : }
      55             : 
      56           3 : BOOST_AUTO_TEST_CASE(test_simple)
      57             : {
      58             :   std::string b(
      59             :     "mu X1 = X2 && X1; \n"
      60             :     "nu X2 = X1 || X3; \n"
      61             :     "mu X3 = X1 || X2; \n"
      62             :     "                  \n"
      63             :     "init X1;          \n"
      64           2 :   );
      65           1 :   run_all_algorithms(b, false);
      66           1 : }
      67             : 
      68           1 : boost::unit_test::test_suite* init_unit_test_suite(int argc, char* argv[])
      69             : {
      70           1 :   return nullptr;
      71           3 : }

Generated by: LCOV version 1.12