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 parity_game_test.cpp
      10             : /// \brief Test for parity game solver. N.B. Currently no real
      11             : /// testing is done. Instead graph representations are produced
      12             : /// in a format that can be read by a python script.
      13             : 
      14             : #define BOOST_TEST_MODULE parity_game_test
      15             : #include <boost/test/included/unit_test.hpp>
      16             : 
      17             : #include "mcrl2/lps/detail/test_input.h"
      18             : #include "mcrl2/modal_formula/detail/test_input.h"
      19             : #include "mcrl2/pbes/detail/parity_game_output.h"
      20             : #include "mcrl2/pbes/detail/pbessolve.h"
      21             : #include "mcrl2/pbes/lps2pbes.h"
      22             : #include "mcrl2/pbes/print.h"
      23             : #include "mcrl2/pbes/txt2pbes.h"
      24             : 
      25             : using namespace mcrl2;
      26             : 
      27          12 : void test_pbes(const std::string& pbes_spec, const bool expected_result)
      28             : {
      29             :   (void)expected_result;
      30             :   
      31          12 :   pbes_system::pbes p = pbes_system::txt2pbes(pbes_spec);
      32          12 :   pbes_system::detail::parity_game_output pgg(p);
      33          12 :   pgg.run();
      34             : 
      35             : // check the result
      36             : #ifdef MCRL2_PGSOLVER_ENABLED
      37             :   static int index;
      38             :   BOOST_CHECK(pbes_system::detail::pbessolve(p,expected_result));
      39             :   std::string name = "parity_game_test" + boost::lexical_cast<std::string>(++index);
      40             :   std::string output_file   = name + ".pg";
      41             :   std::string solution_file = name + ".solution";
      42             :   std::string text = pgg.pgsolver_graph();
      43             :   std::ofstream to(output_file.c_str());
      44             :   to << text << std::endl;
      45             :   std::string command = "pgsolver --recursive --solonly " + output_file + " > " + solution_file;
      46             :   std::cout << "executing: " << command << std::endl;
      47             :   int execution_result = std::system(command.c_str());
      48             :   BOOST_CHECK(execution_result == 0);
      49             :   std::string solution = utilities::read_text(solution_file);
      50             :   std::istringstream is(solution);
      51             : 
      52             :   // skip the first line
      53             :   std::string dummy;
      54             :   std::getline(is, dummy);
      55             : 
      56             :   int player;
      57             :   int winner;
      58             :   is >> player >> winner;
      59             :   std::cout << "player = " << player << std::endl;
      60             :   std::cout << "winner = " << winner << std::endl;
      61             :   BOOST_CHECK(player == 0);
      62             :   BOOST_CHECK(expected_result = (winner == 0));
      63             : #endif
      64          12 : }
      65             : 
      66             : // mimick the way parity_game_generator is used in parity game solver from Twente
      67           3 : void test_pbespgsolve(const std::string& pbes_spec)
      68             : {
      69           3 :   pbes_system::pbes p = pbes_system::txt2pbes(pbes_spec);
      70           3 :   pbes_system::parity_game_generator pgg(p, true, true);
      71           3 :   std::size_t begin = 0;
      72           3 :   std::size_t end = 3;
      73          12 :   for (std::size_t v = begin; v < end; ++v)
      74             :   {
      75           9 :     std::set<std::size_t> deps = pgg.get_dependencies(v);
      76          18 :     for (std::size_t w: deps)
      77             :     {
      78           9 :       assert(w >= begin);
      79           9 :       if (w >= end)
      80             :       {
      81           0 :         end = w + 1;
      82             :       }
      83             :       // edges.push_back(std::make_pair(v - begin, w - begin));
      84             :     }
      85             : 
      86           9 :     int max_prio = 0;
      87          36 :     for (std::size_t m = begin; m < end; ++m)
      88             :     {
      89          27 :       max_prio = (std::max)(max_prio, (int) pgg.get_priority(m));
      90             :     }
      91             : 
      92          36 :     for (std::size_t n = begin; n < end; ++n)
      93             :     {
      94          27 :       pgg.get_priority(n);
      95             :     }
      96           9 :   }
      97           3 : }
      98             : 
      99           1 : void test_lps(const std::string& lps_spec, const bool expected_result, const std::string& formula = lps::detail::NO_DEADLOCK())
     100             : {
     101             :   using namespace pbes_system;
     102           1 :   bool timed = false;
     103           1 :   pbes p = lps2pbes(lps_spec, formula, timed);
     104           1 :   std::string text = pbes_system::pp(p);
     105           1 :   test_pbes(text,expected_result);
     106           1 : }
     107             : 
     108           2 : BOOST_AUTO_TEST_CASE(abp_test)
     109             : {
     110           1 :   test_lps(lps::detail::ABP_SPECIFICATION(),true);
     111           1 : }
     112             : 
     113           2 : BOOST_AUTO_TEST_CASE(bes_test)
     114             : {
     115             :   std::string BES1 =
     116             :     "pbes mu X = X;                                           \n"
     117             :     "                                                         \n"
     118           1 :     "init X;                                                  \n"
     119             :   ;
     120             : 
     121             :   std::string BES2 =
     122             :     "pbes nu X = X;                                           \n"
     123             :     "                                                         \n"
     124           1 :     "init X;                                                  \n"
     125             :   ;
     126             : 
     127             :   std::string BES3 =
     128             :     "pbes mu X = Y;                                           \n"
     129             :     "     nu Y = X;                                           \n"
     130             :     "                                                         \n"
     131           1 :     "init X;                                                  \n"
     132             :   ;
     133             : 
     134             :   std::string BES4 =
     135             :     "pbes nu Y = X;                                           \n"
     136             :     "     mu X = Y;                                           \n"
     137             :     "                                                         \n"
     138           1 :     "init X;                                                  \n"
     139             :   ;
     140             : 
     141             :   std::string BES5 =
     142             :     "pbes mu X1 = X2;                                         \n"
     143             :     "     nu X2 = X1 || X3;                                   \n"
     144             :     "     mu X3 = X4 && X5;                                   \n"
     145             :     "     nu X4 = X1;                                         \n"
     146             :     "     nu X5 = X1 || X3;                                   \n"
     147             :     "                                                         \n"
     148           1 :     "init X1;                                                 \n"
     149             :   ;
     150             : 
     151             :   std::string BES6 =
     152             :     "pbes nu X1 = X2 && X1;                                   \n"
     153             :     "     mu X2 = X1 || X3;                                   \n"
     154             :     "     nu X3 = X3;                                         \n"
     155             :     "                                                         \n"
     156           1 :     "init X1;                                                 \n"
     157             :   ;
     158             : 
     159             :   std::string BES7 =
     160             :     "pbes nu X1 = X2 && X3;                                   \n"
     161             :     "     nu X2 = X4 && X5;                                   \n"
     162             :     "     nu X3 = true;                                       \n"
     163             :     "     nu X4 = false;                                      \n"
     164             :     "     nu X5 = X6;                                         \n"
     165             :     "     nu X6 = X5;                                         \n"
     166             :     "                                                         \n"
     167           1 :     "init X1;                                                 \n"
     168             :   ;
     169             : 
     170             :   std::string BES8 =
     171             :     "pbes nu X1 = X2 && X1;                                   \n"
     172             :     "     mu X2 = X1;                                         \n"
     173             :     "                                                         \n"
     174           1 :     "init X1;                                                 \n"
     175             :   ;
     176             : 
     177           1 :   test_pbes(BES1, false);
     178           1 :   test_pbes(BES2, true);
     179           1 :   test_pbes(BES3, false);
     180           1 :   test_pbes(BES4, true);
     181           1 :   test_pbes(BES5, true);
     182           1 :   test_pbes(BES6, false);
     183           1 :   test_pbes(BES7, false);
     184           1 :   test_pbes(BES8, true);
     185           1 : }
     186             : 
     187           2 : BOOST_AUTO_TEST_CASE(pbes_test)
     188             : {
     189             :   std::string PBES1 =
     190             :     "pbes mu X(m: Nat) =                          \n"
     191             :     "       forall n: Nat. val(!(n < 3)) && X(n); \n"
     192             :     "                                             \n"
     193           1 :     "init X(0);                                   \n"
     194             :   ;
     195             : 
     196             :   std::string PBES2 =
     197             :     "pbes                                                 \n"
     198             :     "mu X(m:Nat) = !(exists n:Nat.(val(n < 3) || !X(n))); \n"
     199             :     "                                                     \n"
     200           1 :     "init X(0);                                           \n"
     201             :   ;
     202             : 
     203             :   std::string PBES3 =
     204             :     "pbes                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          \n"
     205             :     "nu X0 = ((!(forall m:Nat.((val(m < 3)) && (!X2(m + 1, 0))))) || (((forall k:Nat.((val(k < 3)) && (val(k < 2)))) || (exists n:Nat.((val(n < 3)) || (val(n < 2))))) || ((val(true)) => (exists k:Nat.((val(k < 3)) || (exists m:Nat.((val(m < 3)) || (forall k:Nat.((val(k < 3)) && (X4(1, m + 1))))))))))) && ((!(exists n:Nat.((val(n < 3)) || (exists k:Nat.((val(k < 3)) || (val(false))))))) || (forall n:Nat.((val(n < 3)) && (exists n:Nat.((val(n < 3)) || (forall m:Nat.((val(m < 3)) && (exists k:Nat.((val(k < 3)) || (X3)))))))))); \n"
     206             :     "mu X1(b:Bool) = ((exists m:Nat.((val(m < 3)) || (val(b)))) => ((val(false)) || (X3))) && (forall k:Nat.((val(k < 3)) && ((((val(k > 1)) => (X1(k > 1))) && (val(false))) && (exists k:Nat.((val(k < 3)) || (X4(k + 1, k + 1)))))));                                                                                                                                                                                                                                                                                                           \n"
     207             :     "mu X2(n:Nat, m:Nat) = ((exists k:Nat.((val(k < 3)) || (!(val(n < 2))))) && ((X3) || ((forall k:Nat.((val(k < 3)) && (!((val(m < 3)) || (val(m == k)))))) || (!((X0) => (!X4(n + 1, 1))))))) && (exists n:Nat.((val(n < 3)) || (forall m:Nat.((val(m < 3)) && (exists k:Nat.((val(k < 3)) || (val(k < 3))))))));                                                                                                                                                                                                                               \n"
     208             :     "mu X3 = ((val(true)) || (X3)) || (!((forall n:Nat.((val(n < 3)) && (!((val(true)) || ((!(val(n > 1))) && ((X1(n < 3)) || (val(n > 1)))))))) && (forall n:Nat.((val(n < 3)) && (exists m:Nat.((val(m < 3)) || (!X0)))))));                                                                                                                                                                                                                                                                                                                     \n"
     209             :     "mu X4(n:Nat, m:Nat) = ((((forall m:Nat.((val(m < 3)) && ((val(m < 2)) || (val(n < 2))))) => (X1(true))) || (forall m:Nat.((val(m < 3)) && (exists m:Nat.((val(m < 3)) || (val(n > 0))))))) || (forall n:Nat.((val(n < 3)) && ((!(forall n:Nat.((val(n < 3)) && (!X4(0, 1))))) || (forall k:Nat.((val(k < 3)) && (val(true)))))))) || (exists m:Nat.((val(m < 3)) || (forall n:Nat.((val(n < 3)) && (!(!X0))))));                                                                                                                              \n"
     210             :     "                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              \n"
     211           1 :     "init X0;                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      \n"
     212             :   ;
     213             : 
     214           1 :   test_pbes(PBES1, false);
     215           1 :   test_pbes(PBES2, false);
     216           1 :   test_pbes(PBES3, true);
     217           1 :   test_pbespgsolve(PBES1);
     218           1 :   test_pbespgsolve(PBES2);
     219           1 :   test_pbespgsolve(PBES3);
     220           1 : }
     221             : 
     222             : #ifdef MCRL2_EXTENDED_TESTS
     223             : BOOST_AUTO_TEST_CASE(slow_tests)
     224             : {
     225             :   test_lps(lps::detail::DINING3_SPECIFICATION(),false);
     226             :   test_lps(lps::detail::ONE_BIT_SLIDING_WINDOW_SPECIFICATION(), true, "nu X. <true>true && [true]X");
     227             : }
     228             : #endif