LCOV - code coverage report
Current view: top level - modal_formula/test - print_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 38 39 97.4 %
Date: 2020-02-29 00:53:40 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 print_test.cpp
      10             : /// \brief Tests pretty printing of state formulas.
      11             : 
      12             : #include <boost/test/included/unit_test_framework.hpp>
      13             : 
      14             : #include "mcrl2/lps/detail/test_input.h"
      15             : #include "mcrl2/lps/linearise.h"
      16             : #include "mcrl2/modal_formula/parse.h"
      17             : #include "mcrl2/modal_formula/print.h"
      18             : 
      19             : using namespace mcrl2;
      20             : using namespace mcrl2::lps;
      21             : using namespace mcrl2::state_formulas;
      22             : 
      23          21 : void run_test_case(const std::string& formula, const std::string& lpstext)
      24             : {
      25          42 :   specification lpsspec = remove_stochastic_operators(linearise(lpstext));
      26          21 :   parse_state_formula_options options;
      27          21 :   options.check_monotonicity = false;
      28          21 :   options.translate_regular_formulas = false;
      29          21 :   options.resolve_name_clashes = false;
      30          42 :   state_formula f = parse_state_formula(formula, lpsspec, options);
      31          42 :   std::string pp_formula = state_formulas::pp(f);
      32          21 :   if (formula != pp_formula)
      33             :   {
      34           0 :     std::cerr << "Error: " << formula << " is printed as " << pp_formula << std::endl;
      35             :   }
      36          21 :   BOOST_CHECK(formula == pp_formula);
      37          21 : }
      38             : 
      39           3 : BOOST_AUTO_TEST_CASE(test_abp)
      40             : {
      41           2 :   std::string lpstext = lps::detail::ABP_SPECIFICATION();
      42             : 
      43           1 :   run_test_case("delay @ 1", lpstext);
      44           1 :   run_test_case("true", lpstext);
      45           1 :   run_test_case("[true*]<true*>true", lpstext);
      46           1 :   run_test_case("mu X. !!X", lpstext);
      47           1 :   run_test_case("nu X. [true]X && <true>true", lpstext);
      48           1 :   run_test_case("nu X. [true]X && (forall d: D. [r1(d)](mu Y. <true>Y || <s4(d)>true))", lpstext);
      49           1 :   run_test_case("forall d: D. nu X. [!r1(d)]X && [s4(d)]false", lpstext);
      50           1 :   run_test_case("nu X. [true]X && (forall d: D. [r1(d)](nu Y. [!r1(d) && !s4(d)]Y && [r1(d)]false))", lpstext);
      51           1 :   run_test_case("mu X. !X", lpstext);
      52           1 :   run_test_case("mu X. nu Y. X => Y", lpstext);
      53           1 :   run_test_case("mu X. X || (mu X. X)", lpstext);
      54           1 :   run_test_case("(mu X. X) || (mu Y. Y)", lpstext);
      55           1 :   run_test_case("!(mu X. X || (mu X. X))", lpstext);
      56           1 :   run_test_case("(forall d: D. nu X. X) && false", lpstext);
      57           1 :   run_test_case("val(true)", lpstext);
      58           1 :   run_test_case("delay @ 4", lpstext);
      59           1 :   run_test_case("nu Z(i: Nat = 0). Z(2)", lpstext);
      60           1 :   run_test_case("[true]true", lpstext);
      61           1 :   run_test_case("[true]val(true)", lpstext);
      62           1 :   run_test_case("exists d: Nat. val(d < 0)", lpstext);
      63           1 :   run_test_case("exists d: Nat. val(d < 0) || val(d + 1 == 5)", lpstext);
      64           1 : }
      65             : 
      66           1 : boost::unit_test::test_suite* init_unit_test_suite(int argc, char* argv[])
      67             : {
      68           1 :   return nullptr;
      69           3 : }

Generated by: LCOV version 1.13