Line data    Source code

       1             : // Author(s): Gijs Kant
       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 bqnf_quantifier_rewriter_test.cpp
      10             : /// \brief Test for the bqnf_quantifier rewriter.
      11             : 
      12             : #define BOOST_TEST_MODULE bqnf_quantifier_rewriter_test
      13             : #include "mcrl2/pbes/normalize.h"
      14             : #include "mcrl2/pbes/rewrite.h"
      15             : #include "mcrl2/pbes/rewriter.h"
      16             : #include "mcrl2/pbes/txt2pbes.h"
      17             : 
      18             : #include <boost/test/included/unit_test.hpp>
      19             : 
      20             : using namespace mcrl2;
      21             : using namespace mcrl2::pbes_system;
      22             : 
      23             : 
      24           1 : void rewrite_bqnf_quantifier(const std::string& source_text, const std::string& target_text)
      25             : {
      26           1 :   pbes p = txt2pbes(source_text);
      27           1 :   bqnf_rewriter pbesr;
      28           1 :   pbes_rewrite(p, pbesr);
      29           1 :   normalize(p);
      30             :   //std::clog << pp(p);
      31           1 :   pbes target = txt2pbes(target_text);
      32           1 :   normalize(target);
      33           1 :   BOOST_CHECK(p==target);
      34           1 : }
      35             : 
      36             : 
      37           1 : void test_bqnf_quantifier_rewriter()
      38             : {
      39             :   // buffer.always_send_and_receive
      40             :   std::string source_text =
      41             :       "pbes nu X(n: Pos) =\n"
      42             :       "  forall d: Pos . (val(d < 3) => Y(d)) && (val(d > 5 && d < 7) => Z(d));\n"
      43             :       "mu Y(d: Pos) = true;\n"
      44             :       "mu Z(d: Pos) = true;\n"
      45           1 :       "init X(1);"
      46             :   ;
      47             :   std::string target_text =
      48             :       "pbes nu X(n: Pos) =\n"
      49             :       "  (forall d: Pos. val(!(d < 3)) || Y(d)) && (forall d: Pos. val(!(d > 5 && d < 7)) || Z(d));\n"
      50             :       "mu Y(d: Pos) = true;\n"
      51             :       "mu Z(d: Pos) = true;\n"
      52           1 :       "init X(1);"
      53             :   ;
      54           1 :   rewrite_bqnf_quantifier(source_text, target_text);
      55           1 : }
      56             : 
      57             : 
      58           2 : BOOST_AUTO_TEST_CASE(test_main)
      59             : {
      60           1 :   test_bqnf_quantifier_rewriter();
      61           1 : }