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             : #define BOOST_TEST_MODULE modal_formula_print_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/lps/detail/test_input.h"
      16             : #include "mcrl2/lps/linearise.h"
      17             : #include "mcrl2/modal_formula/parse.h"
      18             : #include "mcrl2/modal_formula/print.h"
      19             : 
      20             : using namespace mcrl2;
      21             : using namespace mcrl2::lps;
      22             : using namespace mcrl2::state_formulas;
      23             : 
      24          22 : void run_test_case(const std::string& formula, const specification& lpsspec)
      25             : {
      26          22 :   specification lpscopy(lpsspec);
      27             : 
      28          22 :   parse_state_formula_options options;
      29          22 :   options.check_monotonicity = false;
      30          22 :   options.translate_regular_formulas = false;
      31          22 :   options.resolve_name_clashes = false;
      32          22 :   state_formula f = parse_state_formula(formula, lpscopy, false, options);
      33          22 :   std::string pp_formula = state_formulas::pp(f);
      34          22 :   if (formula != pp_formula)
      35             :   {
      36           0 :     std::cerr << "Error: " << formula << " is printed as " << pp_formula << std::endl;
      37             :   }
      38          22 :   BOOST_TEST(formula == pp_formula);
      39          22 : }
      40             : 
      41           2 : BOOST_AUTO_TEST_CASE(test_abp)
      42             : {
      43           1 :   std::string lpstext = lps::detail::ABP_SPECIFICATION();
      44           1 :   specification lpsspec = remove_stochastic_operators(linearise(lpstext));
      45             : 
      46           1 :   run_test_case("delay @ 1", lpsspec);
      47           1 :   run_test_case("true", lpsspec);
      48           1 :   run_test_case("[true*]<true*>true", lpsspec);
      49           1 :   run_test_case("mu X. !!X", lpsspec);
      50           1 :   run_test_case("nu X. [true]X && <true>true", lpsspec);
      51           1 :   run_test_case("nu X. [true]X && (forall d: D. [r1(d)](mu Y. <true>Y || <s4(d)>true))", lpsspec);
      52           1 :   run_test_case("forall d: D. nu X. [!r1(d)]X && [s4(d)]false", lpsspec);
      53           1 :   run_test_case("nu X. [true]X && (forall d: D. [r1(d)](nu Y. [!r1(d) && !s4(d)]Y && [r1(d)]false))", lpsspec);
      54           1 :   run_test_case("mu X. !X", lpsspec);
      55           1 :   run_test_case("mu X. nu Y. X => Y", lpsspec);
      56           1 :   run_test_case("mu X. X || (mu X. X)", lpsspec);
      57           1 :   run_test_case("(mu X. X) || (mu Y. Y)", lpsspec);
      58           1 :   run_test_case("!(mu X. X || (mu X. X))", lpsspec);
      59           1 :   run_test_case("(forall d: D. nu X. X) && false", lpsspec);
      60           1 :   run_test_case("val(true)", lpsspec);
      61           1 :   run_test_case("delay @ 4", lpsspec);
      62           1 :   run_test_case("nu Z(i: Nat = 0). Z(2)", lpsspec);
      63           1 :   run_test_case("[true]true", lpsspec);
      64           1 :   run_test_case("[true]val(true)", lpsspec);
      65           1 :   run_test_case("exists d: Nat. val(d < 0)", lpsspec);
      66           1 :   run_test_case("exists d: Nat. val(d < 0) || val(d + 1 == 5)", lpsspec);
      67           1 :   run_test_case("mu X. X || val(3 > 2)", lpsspec);  // Check whether val is printed properly after a fixed point without parameters. 
      68           1 : }