LCOV - code coverage report
Current view: top level - modal_formula/test - state_formula_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 201 210 95.7 %
Date: 2020-02-28 00:44:21 Functions: 39 39 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 rename_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define MCRL2_STATE_FORMULA_BUILDER_DEBUG
      13             : 
      14             : #define BOOST_TEST_MODULE state_formula
      15             : #include <boost/test/included/unit_test_framework.hpp>
      16             : 
      17             : #include "mcrl2/lps/linearise.h"
      18             : #include "mcrl2/modal_formula/count_fixpoints.h"
      19             : #include "mcrl2/modal_formula/maximal_closed_subformula.h"
      20             : #include "mcrl2/modal_formula/parse.h"
      21             : #include "mcrl2/modal_formula/preprocess_state_formula.h"
      22             : 
      23             : using namespace std;
      24             : using namespace mcrl2;
      25             : using namespace mcrl2::core;
      26             : using namespace mcrl2::lps;
      27             : using namespace mcrl2::lps::detail;
      28             : using namespace mcrl2::state_formulas;
      29             : 
      30           3 : BOOST_AUTO_TEST_CASE(test_rename)
      31             : {
      32             :   const std::string SPECIFICATION =
      33             :     "act a:Nat;                              \n"
      34             :     "                                        \n"
      35             :     "map smaller: Nat#Nat -> Bool;           \n"
      36             :     "                                        \n"
      37             :     "var x,y : Nat;                          \n"
      38             :     "                                        \n"
      39             :     "eqn smaller(x,y) = x < y;               \n"
      40             :     "                                        \n"
      41             :     "proc P(n:Nat) = sum m: Nat. a(m). P(m); \n"
      42             :     "                                        \n"
      43           2 :     "init P(0);                              \n"
      44             :     ;
      45             : 
      46             :   using mcrl2::state_formulas::pp;
      47           2 :   specification lpsspec = remove_stochastic_operators(linearise(SPECIFICATION));
      48             : 
      49           2 :   state_formula formula = parse_state_formula("(mu X. X) && (mu X. X)", lpsspec);
      50             : 
      51           2 :   data::set_identifier_generator generator;
      52           1 :   generator.add_identifiers(lps::find_identifiers(lpsspec));
      53           1 :   formula = rename_predicate_variables(formula, generator);
      54             : 
      55           1 :   std::cout << "pp(formula) == " << pp(formula) << std::endl;
      56           1 :   BOOST_CHECK(pp(formula) == "(mu X1. X1) && (mu X. X)" || pp(formula) == "(mu X. X) && (mu X1. X1)");
      57             : 
      58           1 :   generator = data::set_identifier_generator();
      59           1 :   generator.add_identifiers(lps::find_identifiers(lpsspec));
      60           1 :   parse_state_formula_options options;
      61           1 :   options.check_monotonicity = false;
      62           1 :   options.resolve_name_clashes = false;
      63           1 :   formula = parse_state_formula("mu X. mu X. X", lpsspec, options);
      64           1 :   std::cout << "formula: " << pp(formula) << std::endl;
      65           1 :   formula = rename_predicate_variables(formula, generator);
      66           1 :   std::cout << "formula: " << pp(formula) << std::endl;
      67           1 :   BOOST_CHECK_EQUAL(pp(formula), "mu X. mu X1. X1");
      68           1 : }
      69             : 
      70           3 : BOOST_AUTO_TEST_CASE(test_normalize)
      71             : {
      72           2 :   state_formula x = state_formulas::variable(identifier_string("X"), data::data_expression_list());
      73           2 :   state_formula y = state_formulas::variable(identifier_string("Y"), data::data_expression_list());
      74           2 :   state_formula f;
      75           2 :   state_formula f1;
      76           2 :   state_formula f2;
      77             : 
      78           1 :   f = imp(not_(x), y);
      79           1 :   f1 = normalize(f);
      80           1 :   f2 = or_(x, y);
      81           1 :   std::cout << "f  = " << state_formulas::pp(f) << std::endl;
      82           1 :   std::cout << "f1 = " << state_formulas::pp(f1) << std::endl;
      83           1 :   std::cout << "f2 = " << state_formulas::pp(f2) << std::endl;
      84           1 :   BOOST_CHECK_EQUAL(f1, f2);
      85             : 
      86           1 :   f  = not_(and_(not_(x), not_(y)));
      87           1 :   f1 = normalize(f);
      88           1 :   f2 = or_(x, y);
      89           1 :   std::cout << "f  = " << state_formulas::pp(f) << std::endl;
      90           1 :   std::cout << "f1 = " << state_formulas::pp(f1) << std::endl;
      91           1 :   std::cout << "f2 = " << state_formulas::pp(f2) << std::endl;
      92           1 :   BOOST_CHECK_EQUAL(f1, f2);
      93           1 : }
      94             : 
      95           3 : BOOST_AUTO_TEST_CASE(test_type_checking)
      96             : {
      97           2 :   specification lpsspec = remove_stochastic_operators(linearise(
      98             :                             "sort CPU = struct p1;"
      99             :                             "sort CPUs = Set(CPU);"
     100           2 :                             "init delta;"));
     101             : 
     102           1 :   state_formula formula = parse_state_formula("nu X (P : CPUs = {p1}) . val(P != {})", lpsspec);
     103           1 : }
     104             : 
     105           3 : BOOST_AUTO_TEST_CASE(test_type_checking_conversion_of_arguments)
     106             : {
     107           2 :   specification lpsspec = remove_stochastic_operators(linearise(
     108             :                             "sort B = struct d;"
     109             :                             "act a: List(B);"
     110             :                             "init a([d]);"
     111           2 :                           ));
     112             : 
     113           2 :   state_formula formula = parse_state_formula("<a([d])>true", lpsspec);
     114             : 
     115           1 :   BOOST_CHECK(is_may(formula));
     116           1 :   const state_formulas::may& f = atermpp::down_cast<state_formulas::may>(formula);
     117           1 :   BOOST_CHECK(is_regular_formula(f.formula()));
     118           1 : }
     119             : 
     120             : 
     121             : static inline
     122           1 : state_formula negate_variable(const variable& x)
     123             : {
     124           1 :   return state_formulas::not_(x);
     125             : }
     126             : 
     127           3 : BOOST_AUTO_TEST_CASE(test_not)
     128             : {
     129           2 :   data::data_expression_list args;
     130           2 :   variable v(core::identifier_string("v"), args);
     131           2 :   state_formula s = not_(v);
     132           1 :   BOOST_CHECK(is_not(s));
     133             : 
     134           2 :   state_formula t = negate_variable(v);
     135           1 :   BOOST_CHECK_EQUAL(s, t);
     136             : 
     137             :   // The following is expected to trigger an assertion failure
     138             :   // aterm_appl a = v;
     139             :   // state_formula t = not_(a);
     140           1 : }
     141             : 
     142             : // test case supplied by Jan Friso, 4-1-2011
     143           3 : BOOST_AUTO_TEST_CASE(test_parse)
     144             : {
     145             :   std::string spec_text =
     146             :     "act a:Nat; \n"
     147           2 :     "init a(1); \n"
     148             :     ;
     149             : 
     150           2 :   std::string formula_text = "<a(1)>true";
     151             : 
     152           2 :   lps::specification lpsspec = remove_stochastic_operators(lps::linearise(spec_text));
     153           2 :   state_formulas::state_formula f = state_formulas::parse_state_formula(formula_text, lpsspec);
     154             : 
     155           1 :   std::cerr << "--- f ---\n" << state_formulas::pp(f) << "\n\n" << f << std::endl;
     156           2 :   std::set<core::identifier_string> ids = state_formulas::find_identifiers(f);
     157           1 :   BOOST_CHECK(ids.find(core::identifier_string("1")) == ids.end());
     158           1 :   BOOST_CHECK(ids.find(core::identifier_string("@c1")) != ids.end());
     159           1 : }
     160             : 
     161           3 : BOOST_AUTO_TEST_CASE(test_count_fixpoints)
     162             : {
     163           2 :   state_formula formula;
     164           2 :   specification lpsspec;
     165             : 
     166           1 :   formula = parse_state_formula("(mu X. X) && (mu X. X)", lpsspec);
     167           1 :   BOOST_CHECK_EQUAL(count_fixpoints(formula), 2u);
     168             : 
     169           1 :   formula = parse_state_formula("exists b:Bool. (mu X. X) || forall b:Bool. (nu X. mu Y. (X || Y))", lpsspec);
     170           1 :   BOOST_CHECK_EQUAL(count_fixpoints(formula), 3u);
     171           1 : }
     172             : 
     173             : // Test case for bug #1094.
     174             : // This is expected to fail, due to the occurrence of an unbound variable Y
     175             : // in the formula.
     176           3 : BOOST_AUTO_TEST_CASE(test_1094)
     177             : {
     178             :   const std::string SPEC =
     179             :       "act  a,b,c,d;\n"
     180             :       "\n"
     181             :       "proc P(s3_X: Pos) =\n"
     182             :       "       (s3_X == 1) ->\n"
     183             :       "         a .\n"
     184             :       "         P(s3_X = 2)\n"
     185             :       "     + (s3_X == 2) ->\n"
     186             :       "         b .\n"
     187             :       "         P(s3_X = 3)\n"
     188             :       "     + (s3_X == 3) ->\n"
     189             :       "         a .\n"
     190             :       "         P(s3_X = 4)\n"
     191             :       "     + (s3_X == 3) ->\n"
     192             :       "         a .\n"
     193             :       "         P(s3_X = 5)\n"
     194             :       "     + (s3_X == 4) ->\n"
     195             :       "         c .\n"
     196             :       "         P(s3_X = 1)\n"
     197             :       "     + (s3_X == 5) ->\n"
     198             :       "         d .\n"
     199             :       "         P(s3_X = 1)\n"
     200             :       "     + delta;\n"
     201             :       "\n"
     202           2 :       "init P(1);\n"
     203             :     ;
     204           2 :   specification s(parse_linear_process_specification(SPEC));
     205             : 
     206           2 :   const std::string FORMULA = "[true*]([b] nu X. mu X.( [!c]X && [!c]Y))";
     207             : 
     208           1 :   BOOST_CHECK_THROW(parse_state_formula(FORMULA, s), mcrl2::runtime_error);
     209           1 : }
     210             : 
     211             : inline
     212           5 : state_formula sigma(const state_formula& x)
     213             : {
     214          10 :   variable X("X", data::data_expression_list());
     215          10 :   return x == X ? false_() : x;
     216             : }
     217             : 
     218           3 : BOOST_AUTO_TEST_CASE(test_replace_state_formulas)
     219             : {
     220           2 :   specification lpsspec;
     221           2 :   state_formula f = parse_state_formula("(mu X. X) && (mu X. X)", lpsspec);
     222           2 :   state_formula result = replace_state_formulas(f, sigma);
     223           2 :   state_formula expected_result = parse_state_formula("(mu X. false) && (mu X. false)", lpsspec);
     224           1 :   if (!(result == expected_result))
     225             :   {
     226           0 :     std::cout << "error: " << state_formulas::pp(result) << " != " << state_formulas::pp(expected_result) << std::endl;
     227             :   }
     228           1 :   BOOST_CHECK(result == expected_result);
     229           1 : }
     230             : 
     231           3 : BOOST_AUTO_TEST_CASE(test_find_state_variables)
     232             : {
     233           2 :   specification lpsspec;
     234             : 
     235           2 :   state_formula f = parse_state_formula("(mu X. nu Y. true && mu Z. X && Z)", lpsspec);
     236           2 :   std::set<state_formulas::variable> v = state_formulas::find_state_variables(f);
     237           1 :   BOOST_CHECK(v.size() == 2);
     238             : 
     239           1 :   f = parse_state_formula("mu X. nu Y. (true && mu Z. (X && Y || Z))", lpsspec);
     240           1 :   v = find_state_variables(f);
     241           1 :   BOOST_CHECK(v.size() == 3);
     242             : 
     243           2 :   state_formulas::variable X("X", data::data_expression_list());
     244           2 :   state_formulas::variable Y("Y", data::data_expression_list());
     245           2 :   state_formulas::variable Z("Z", data::data_expression_list());
     246           2 :   state_formula phi = state_formulas::and_(X, Y);
     247           1 :   v = find_state_variables(phi);
     248           1 :   BOOST_CHECK(v.size() == 2);
     249           1 :   v = find_free_state_variables(phi);
     250           1 :   BOOST_CHECK(v.size() == 2);
     251           2 :   state_formula psi = state_formulas::mu("X", data::assignment_list(), phi);
     252           1 :   v = find_state_variables(psi);
     253           1 :   BOOST_CHECK(v.size() == 2);
     254           1 :   v = find_free_state_variables(psi);
     255           1 :   BOOST_CHECK(v.size() == 1);
     256           1 : }
     257             : 
     258             : inline
     259           4 : bool contains(const std::set<state_formulas::state_formula>& v, const std::string& s)
     260             : {
     261           6 :   for (const state_formulas::state_formula& f: v)
     262             :   {
     263           6 :     if (state_formulas::pp(f) == s)
     264             :     {
     265           4 :       return true;
     266             :     }
     267             :   }
     268           0 :   return false;
     269             : }
     270             : 
     271           3 : BOOST_AUTO_TEST_CASE(test_maximal_closed_subformulas)
     272             : {
     273           1 :   mcrl2::log::mcrl2_logger::set_reporting_level(mcrl2::log::debug, "state_formulas");
     274             : 
     275           2 :   specification lpsspec;
     276           2 :   state_formula f = parse_state_formula("(mu X. nu Y. true && mu Z. X && Z)", lpsspec);
     277           2 :   std::set<state_formulas::state_formula> v = maximal_closed_subformulas(f);
     278           1 :   BOOST_CHECK(v.size() == 1);
     279             : 
     280           1 :   f = parse_state_formula("exists b: Bool. forall c: Bool. val(b) && (val(c) || true) && false", lpsspec);
     281           1 :   v = maximal_closed_subformulas(f);
     282           1 :   BOOST_CHECK(v.size() == 1);
     283             : 
     284           2 :   state_formula g = exists(f).body();
     285           1 :   std::cout << "g = " << state_formulas::pp(g) << std::endl;
     286           1 :   v = maximal_closed_subformulas(g);
     287           3 :   for (const state_formula& f: v)
     288             :   {
     289           2 :     std::cout << "element " << f << std::endl;
     290             :   }
     291           1 :   BOOST_CHECK(v.size() == 2);
     292           1 :   BOOST_CHECK(contains(v, "true"));
     293           1 :   BOOST_CHECK(contains(v, "false"));
     294             : 
     295           2 :   state_formula h = forall(g).body();
     296           1 :   v = maximal_closed_subformulas(h);
     297           1 :   std::cout << "h = " << state_formulas::pp(h) << std::endl;
     298           3 :   for (const state_formula& f: v)
     299             :   {
     300           2 :     std::cout << "element " << f << std::endl;
     301             :   }
     302           1 :   BOOST_CHECK(v.size() == 2);
     303           1 :   BOOST_CHECK(contains(v, "true"));
     304           1 :   BOOST_CHECK(contains(v, "false"));
     305           1 : }
     306             : 
     307           4 : void test_has_unscoped_modal_formulas(const std::string& text, lps::specification& lpsspec, bool expected_result)
     308             : {
     309           8 :   state_formula x = parse_state_formula(text, lpsspec);
     310           4 :   bool result = state_formulas::detail::has_unscoped_modal_formulas(x);
     311           4 :   if (result != expected_result)
     312             :   {
     313           0 :     std::cout << "--- has_unscoped_modal_formulas failure ---" << std::endl;
     314           0 :     std::cout << "formula = " << text << std::endl;
     315           0 :     std::cout << "result  = " << result << std::endl;
     316             :   }
     317           4 :   BOOST_CHECK_EQUAL(result, expected_result);
     318           4 : }
     319             : 
     320           3 : BOOST_AUTO_TEST_CASE(has_unscoped_modal_formulas_test)
     321             : {
     322             :   const std::string text =
     323             :     "act a, b, c;                  \n"
     324             :     "                              \n"
     325             :     "proc P = delta;               \n"
     326             :     "                              \n"
     327           2 :     "init P;                       \n"
     328             :     ;
     329           2 :   lps::specification lpsspec = lps::parse_linear_process_specification(text);
     330             : 
     331           1 :   test_has_unscoped_modal_formulas("[a]true", lpsspec, true);
     332           1 :   test_has_unscoped_modal_formulas("mu X. X", lpsspec, false);
     333           1 :   test_has_unscoped_modal_formulas("true => [a]true", lpsspec, true);
     334           1 :   test_has_unscoped_modal_formulas("true => mu X. [a]<b>true", lpsspec, false);
     335           1 : }
     336             : 
     337           4 : void test_preprocess_nested_modal_operators(const std::string& text, lps::specification& lpsspec, const std::string& expected_result_text)
     338             : {
     339           8 :   state_formula x = parse_state_formula(text, lpsspec);
     340           8 :   state_formula expected_result = parse_state_formula(expected_result_text, lpsspec);
     341           8 :   state_formula result = state_formulas::preprocess_nested_modal_operators(x);
     342           4 :   if (result != expected_result)
     343             :   {
     344           0 :     std::cout << "--- preprocess_nested_modal_operators failure ---" << std::endl;
     345           0 :     std::cout << "formula          = " << text << std::endl;
     346           0 :     std::cout << "result           = " << state_formulas::pp(result) << std::endl;
     347           0 :     std::cout << "expected result  = " << expected_result_text << std::endl;
     348             :   }
     349           4 :   BOOST_CHECK_EQUAL(result, expected_result);
     350           4 : }
     351             : 
     352           3 : BOOST_AUTO_TEST_CASE(preprocess_nested_modal_operators_test)
     353             : {
     354             :   const std::string text =
     355             :     "act a, b, c;                  \n"
     356             :     "                              \n"
     357             :     "proc P = delta;               \n"
     358             :     "                              \n"
     359           2 :     "init P;                       \n"
     360             :     ;
     361           2 :   lps::specification lpsspec = lps::parse_linear_process_specification(text);
     362             : 
     363           1 :   test_preprocess_nested_modal_operators("[a]true", lpsspec, "[a]true");
     364           1 :   test_preprocess_nested_modal_operators("[a]<b>true", lpsspec, "[a]mu X. <b>true");
     365           1 :   test_preprocess_nested_modal_operators("true && <a><a>true", lpsspec, "true && <a>mu X. <a>true");
     366           1 :   test_preprocess_nested_modal_operators("true => mu X. [a]<b>true", lpsspec, "true => mu X. [a]mu X1. <b>true");
     367           1 : }
     368             : 
     369           3 : BOOST_AUTO_TEST_CASE(parse_modal_formula_test)
     370             : {
     371             :   const std::string text =
     372             :     "act a, b, c;                  \n"
     373             :     "                              \n"
     374             :     "proc P = delta;               \n"
     375             :     "                              \n"
     376           2 :     "init P;                       \n"
     377             :     ;
     378           2 :   lps::specification lpsspec = lps::parse_linear_process_specification(text);
     379             : 
     380           2 :   const std::string formula_text = "nu X(n: Nat = 0, b: Bool = false). X(n, b)";
     381           2 :   state_formula x = parse_state_formula(formula_text, lpsspec);
     382           2 :   std::string s = state_formulas::pp(x);
     383           1 :   BOOST_CHECK_EQUAL(s, formula_text);
     384           1 : }
     385             : 
     386           3 : BOOST_AUTO_TEST_CASE(check_parameter_name_clashes_test)
     387             : {
     388             :   const std::string text =
     389             :     "act a, b, c;                  \n"
     390             :     "                              \n"
     391             :     "proc P = delta;               \n"
     392             :     "                              \n"
     393           2 :     "init P;                       \n"
     394             :     ;
     395           2 :   lps::specification lpsspec = lps::parse_linear_process_specification(text);
     396             : 
     397           1 :   BOOST_CHECK(has_data_variable_name_clashes(parse_state_formula("nu X(n: Nat = 0). mu Y(n: Nat = 1). val(n == 0)", lpsspec)));
     398           1 :   BOOST_CHECK(!has_data_variable_name_clashes(parse_state_formula("nu X(n: Nat = 0). mu Y(m: Nat = 1). val(n == 0)", lpsspec)));
     399           1 : }
     400             : 
     401           3 : BOOST_AUTO_TEST_CASE(parse_state_formula_specification_test)
     402             : {
     403             :   const std::string text =
     404             :     "sort S;                       \n"
     405             :     "cons s0: S;                   \n"
     406             :     "act a: S;                     \n"
     407           2 :     "form forall s: S. [a(s)]true; \n"
     408             :     ;
     409           2 :   state_formula_specification x = parse_state_formula_specification(text);
     410           2 :   std::string text1 = state_formulas::pp(x);
     411           1 :   std::cout << text1 << std::endl;
     412           1 :   BOOST_CHECK_EQUAL(utilities::remove_whitespace(text), utilities::remove_whitespace(text1));
     413           4 : }

Generated by: LCOV version 1.13