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 abstract_test.cpp
      10             : /// \brief Test the pbes abstract algorithm.
      11             : 
      12             : #define BOOST_TEST_MODULE abstract_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : #include "mcrl2/pbes/abstract.h"
      15             : #include "mcrl2/pbes/txt2pbes.h"
      16             : 
      17             : using namespace mcrl2;
      18             : using namespace mcrl2::pbes_system;
      19             : 
      20           3 : void test_pbesabstract(const std::string& pbes_spec, const std::string& variable_spec, bool value_true)
      21             : {
      22           3 :   pbes p = txt2pbes(pbes_spec);
      23           3 :   pbes_system::detail::pbes_parameter_map parameter_map = pbes_system::detail::parse_pbes_parameter_map(p, variable_spec);
      24             :   pbes_abstract_algorithm algorithm;
      25           3 :   algorithm.run(p, parameter_map, value_true);
      26           3 :   std::cout << "\n-------------------------------\n" << pbes_system::pp(p) << std::endl;
      27           3 : }
      28             : 
      29           2 : BOOST_AUTO_TEST_CASE(pbesabstract)
      30             : {
      31           1 :   test_pbesabstract(
      32             :     "pbes nu X(a: Bool, b: Nat) =  \n"
      33             :     "       val(a) || X(a, b + 1); \n"
      34             :     "                              \n"
      35             :     "init X(true, 0);              \n"
      36             :     ,
      37             :     "X(b:Nat)"
      38             :     ,
      39             :     true
      40             :   );
      41             : 
      42           1 :   test_pbesabstract(
      43             :     "pbes nu X1(b:Bool) = exists b:Bool.(X2 || val(b)); \n"
      44             :     "     mu X2 = X2;                                   \n"
      45             :     "                                                   \n"
      46             :     "init X1(true);                                     \n"
      47             :     ,
      48             :     "X1(b:Bool)"
      49             :     ,
      50             :     true
      51             :   );
      52             : 
      53           1 :   test_pbesabstract(
      54             :     "pbes nu X1(b:Bool) = X2 || val(b); \n"
      55             :     "     mu X2 = X2;                   \n"
      56             :     "                                   \n"
      57             :     "init X1(true);                     \n"
      58             :     ,
      59             :     "X1(b:Bool)"
      60             :     ,
      61             :     true
      62             :   );
      63           1 : }