LCOV - code coverage report
Current view: top level - modal_formula/test - monotonicity_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 50 50 100.0 %
Date: 2024-03-08 02:52:28 Functions: 5 5 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 monotonicity_test.cpp
      10             : /// \brief Tests for the is_monotonous function for state formulas.
      11             : 
      12             : #define BOOST_TEST_MODULE modal_formula_monotonicity_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             : 
      19             : using namespace mcrl2;
      20             : using namespace mcrl2::lps;
      21             : using namespace mcrl2::state_formulas;
      22             : 
      23          30 : void run_monotonicity_test_case(const std::string& formula, const specification& lpsspec, const bool expect_success = true)
      24             : {
      25          30 :   specification lpscopy(lpsspec);
      26             : 
      27          30 :   parse_state_formula_options options;
      28          30 :   options.check_monotonicity = false;
      29          30 :   options.resolve_name_clashes = false;
      30          30 :   state_formula f = parse_state_formula(formula, lpscopy, false, options);
      31          30 :   if (state_formulas::has_state_variable_name_clashes(f))
      32             :   {
      33           6 :     std::cerr << "Error: " << state_formulas::pp(f) << " has name clashes" << std::endl;
      34           6 :     f = state_formulas::resolve_state_variable_name_clashes(f);
      35           6 :     std::cerr << "resolved to " << state_formulas::pp(f) << std::endl;
      36             :   }
      37          30 :   BOOST_TEST(is_monotonous(f) == expect_success);
      38          30 : }
      39             : 
      40           2 : BOOST_AUTO_TEST_CASE(test_abp)
      41             : {
      42           1 :   std::string lpstext = lps::detail::ABP_SPECIFICATION();
      43           1 :   specification lpsspec = remove_stochastic_operators(linearise(lpstext));
      44             : 
      45           1 :   run_monotonicity_test_case("true", lpsspec, true);
      46           1 :   run_monotonicity_test_case("[true*]<true*>true", lpsspec, true);
      47           1 :   run_monotonicity_test_case("mu X. !!X", lpsspec, true);
      48           1 :   run_monotonicity_test_case("nu X. ([true]X && <true>true)", lpsspec, true);
      49           1 :   run_monotonicity_test_case("nu X. ([true]X && forall d:D. [r1(d)] mu Y. (<true>Y || <s4(d)>true))", lpsspec, true);
      50           1 :   run_monotonicity_test_case("forall d:D. nu X. (([!r1(d)]X && [s4(d)]false))", lpsspec, true);
      51           1 :   run_monotonicity_test_case("nu X. ([true]X && forall d:D. [r1(d)]nu Y. ([!r1(d) && !s4(d)]Y && [r1(d)]false))", lpsspec, true);
      52           1 :   run_monotonicity_test_case("mu X. !X", lpsspec, false);
      53           1 :   run_monotonicity_test_case("mu X. nu Y. (X => Y)", lpsspec, false);
      54           1 :   run_monotonicity_test_case("mu X. X || mu X. X", lpsspec, true);
      55           1 :   run_monotonicity_test_case("mu X. (X || mu X. X)", lpsspec, true);
      56           1 :   run_monotonicity_test_case("mu X. (X || mu Y. Y)", lpsspec, true);
      57           1 :   run_monotonicity_test_case("!(mu X. X || mu X. X)", lpsspec, true);
      58           1 :   run_monotonicity_test_case("!(mu X. (X || mu X. X))", lpsspec, true);
      59           1 :   run_monotonicity_test_case("!(mu X. (X || mu Y. Y))", lpsspec, true);
      60           1 : }
      61             : 
      62             : // Test case provided by Jeroen Keiren, 10-9-2010
      63           2 : BOOST_AUTO_TEST_CASE(test_elevator)
      64             : {
      65             :   std::string lpstext =
      66             : 
      67             :     "% Model of an elevator for n floors.                                                                                           \n"
      68             :     "% Originally described in 'Solving Parity Games in Practice' by Oliver                                                         \n"
      69             :     "% Friedmann and Martin Lange.                                                                                                  \n"
      70             :     "%                                                                                                                              \n"
      71             :     "% This is the version with a first in first out policy                                                                         \n"
      72             :     "                                                                                                                               \n"
      73             :     "sort Floor = Pos;                                                                                                              \n"
      74             :     "     DoorStatus = struct open | closed;                                                                                        \n"
      75             :     "     Requests = List(Floor);                                                                                                   \n"
      76             :     "                                                                                                                               \n"
      77             :     "map maxFloor: Floor;                                                                                                           \n"
      78             :     "eqn maxFloor = 3;                                                                                                              \n"
      79             :     "                                                                                                                               \n"
      80             :     "map addRequest : Requests # Floor -> Requests;                                                                                 \n"
      81             :     "                                                                                                                               \n"
      82             :     "var r: Requests;                                                                                                               \n"
      83             :     "    f,g: Floor;                                                                                                                \n"
      84             :     "    % FIFO behaviour!                                                                                                          \n"
      85             :     "eqn addRequest([], f) = [f];                                                                                                   \n"
      86             :     "    (f == g) -> addRequest(g |> r, f) = g |> r;                                                                                \n"
      87             :     "    (f != g) -> addRequest(g |> r, f) = g |> addRequest(r, f);                                                                 \n"
      88             :     "                                                                                                                               \n"
      89             :     "map removeRequest : Requests -> Requests;                                                                                      \n"
      90             :     "var r: Requests;                                                                                                               \n"
      91             :     "    f: Floor;                                                                                                                  \n"
      92             :     "eqn removeRequest(f |> r) = r;                                                                                                 \n"
      93             :     "                                                                                                                               \n"
      94             :     "map getNext : Requests -> Floor;                                                                                               \n"
      95             :     "var r: Requests;                                                                                                               \n"
      96             :     "    f: Floor;                                                                                                                  \n"
      97             :     "eqn getNext(f |> r) = f;                                                                                                       \n"
      98             :     "                                                                                                                               \n"
      99             :     "act isAt: Floor;                                                                                                               \n"
     100             :     "    request: Floor;                                                                                                            \n"
     101             :     "    close, open, up, down;                                                                                                     \n"
     102             :     "                                                                                                                               \n"
     103             :     "proc Elevator(at: Floor, status: DoorStatus, reqs: Requests, moving: Bool) =                                                   \n"
     104             :     "       isAt(at) . Elevator()                                                                                                   \n"
     105             :     "     + sum f: Floor. (f <= maxFloor) -> request(f) . Elevator(reqs = addRequest(reqs, f))                                      \n"
     106             :     "     + (status == open) -> close . Elevator(status = closed)                                                                   \n"
     107             :     "     + (status == closed && reqs != [] && getNext(reqs) > at) -> up . Elevator(at = at + 1, moving = true)                     \n"
     108             :     "     + (status == closed && reqs != [] && getNext(reqs) < at) -> down . Elevator(at = Int2Pos(at - 1), moving = true)          \n"
     109             :     "     + (status == closed && getNext(reqs) == at) -> open. Elevator(status = open, reqs = removeRequest(reqs), moving = false); \n"
     110             :     "                                                                                                                               \n"
     111           1 :     "init Elevator(1, open, [], false);                                                                                             \n"
     112             :     ;    
     113           1 :   specification lpsspec = remove_stochastic_operators(linearise(lpstext));
     114             : 
     115           1 :   run_monotonicity_test_case("nu U. [true] U && ((mu V . nu W. !([!request(maxFloor)]!W && [request(maxFloor)]!V)) || (nu X . mu Y. [!isAt(maxFloor)] Y &&  [isAt(maxFloor)]X))", lpsspec, true);
     116           1 :   run_monotonicity_test_case("nu U. [true] U && ((nu V . mu W. ([!request(maxFloor)]W && [request(maxFloor)]V)) => (nu X . mu Y. [!isAt(maxFloor)] Y &&  [isAt(maxFloor)]X))", lpsspec, true);
     117           1 :   run_monotonicity_test_case("nu U. [true] U && (!(nu V . mu W. ([!request(maxFloor)]W && [request(maxFloor)]V)) || (nu X . mu Y. [!isAt(maxFloor)] Y &&  [isAt(maxFloor)]X))", lpsspec, true);
     118           1 :   run_monotonicity_test_case("(nu X . mu Y. X) => true", lpsspec, true);
     119           1 :   run_monotonicity_test_case("!(nu X . mu Y. X)", lpsspec, true);
     120           1 :   run_monotonicity_test_case("mu X . X", lpsspec, true);
     121           1 :   run_monotonicity_test_case("nu X . X", lpsspec, true);
     122           1 :   run_monotonicity_test_case("mu X . !X", lpsspec, false);
     123           1 :   run_monotonicity_test_case("nu X . !X", lpsspec, false);
     124           1 :   run_monotonicity_test_case("!(mu X . X)", lpsspec, true);
     125           1 :   run_monotonicity_test_case("!(nu X . X)", lpsspec, true);
     126           1 :   run_monotonicity_test_case("(mu X . X) => true", lpsspec, true);
     127           1 :   run_monotonicity_test_case("(nu X . X) => true", lpsspec, true);
     128           1 :   run_monotonicity_test_case("!(mu X. (mu X. X))", lpsspec, true);
     129             :   // trac ticket #1320
     130           1 :   run_monotonicity_test_case("!mu X. [true]X && mu X. [true]X", lpsspec, true);
     131           1 : }

Generated by: LCOV version 1.14