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 pbesrewr_test.cpp
      10             : /// \brief Test for the pbes rewriters.
      11             : 
      12             : #define BOOST_TEST_MODULE pbesrewr_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/lps/detail/test_input.h"
      16             : #include "mcrl2/modal_formula/detail/test_input.h"
      17             : #include "mcrl2/modal_formula/parse.h"
      18             : #include "mcrl2/pbes/lps2pbes.h"
      19             : #include "mcrl2/pbes/rewrite.h"
      20             : #include "mcrl2/pbes/rewriter.h"
      21             : #include "mcrl2/pbes/txt2pbes.h"
      22             : 
      23             : using namespace mcrl2;
      24             : using namespace mcrl2::pbes_system;
      25             : 
      26           2 : BOOST_AUTO_TEST_CASE(test_pbesrewr1)
      27             : {
      28             :   std::string pbes_text =
      29             :     "sort Enum = struct e1 | e2;                           \n"
      30             :     "pbes mu X(n:Enum)=exists m1,m2:Enum.(X(m1) || X(m2)); \n"
      31           1 :     "init X(e1);                                           \n"
      32             :     ;
      33           1 :   pbes p = txt2pbes(pbes_text);
      34           1 :   data::rewriter datar(p.data(), data::jitty);
      35           1 :   bool enumerate_infinite_sorts = true;
      36           1 :   enumerate_quantifiers_rewriter pbesr(datar, p.data(), enumerate_infinite_sorts);
      37           1 :   pbes_rewrite(p, pbesr);
      38           1 :   BOOST_CHECK(p.is_well_typed());
      39           1 : }
      40             : 
      41           2 : BOOST_AUTO_TEST_CASE(test_pbesrewr2)
      42             : {
      43           2 :   lps::specification spec = remove_stochastic_operators(lps::linearise(lps::detail::ABP_SPECIFICATION()));
      44           1 :   state_formulas::state_formula formula = state_formulas::parse_state_formula(lps::detail::NO_DEADLOCK(), spec, false);
      45           1 :   bool timed = false;
      46           1 :   pbes p = lps2pbes(spec, formula, timed);
      47           1 :   BOOST_CHECK(p.is_well_typed());
      48             : 
      49           1 :   data::rewriter datar(p.data(), data::jitty);
      50           1 :   bool enumerate_infinite_sorts = true;
      51           1 :   enumerate_quantifiers_rewriter pbesr(datar, p.data(), enumerate_infinite_sorts);
      52           1 :   pbes_rewrite(p, pbesr);
      53           1 :   BOOST_CHECK(p.is_well_typed());
      54           1 : }