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 ppg_rewriter_test.cpp
      10             : /// \brief Test for the ppg rewriter.
      11             : 
      12             : #define BOOST_TEST_MODULE ppg_rewriter_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/pbes/detail/bqnf2ppg_rewriter.h"
      16             : #include "mcrl2/pbes/detail/bqnf_traverser.h"
      17             : #include "mcrl2/pbes/detail/ppg_rewriter.h"
      18             : #include "mcrl2/pbes/detail/ppg_traverser.h"
      19             : #include "mcrl2/pbes/detail/ppg_visitor.h"
      20             : #include "mcrl2/pbes/normalize.h"
      21             : #include "mcrl2/pbes/rewriter.h"
      22             : #include "mcrl2/pbes/txt2pbes.h"
      23             : 
      24             : 
      25             : using namespace mcrl2;
      26             : using namespace mcrl2::pbes_system;
      27             : 
      28             : 
      29           1 : void rewrite_ppg(const std::string& bqnf_text, const std::string& ppg_text)
      30             : {
      31           1 :   std::clog << "rewrite_ppg" << std::endl;
      32           1 :   std::clog << "Parsing text..." << std::endl;
      33             :   //std::clog << bqnf_text << std::endl;
      34           1 :   pbes p = txt2pbes(bqnf_text);
      35           1 :   std::clog << "done." << std::endl;
      36             : 
      37           1 :   bool is_bqnf = pbes_system::detail::is_bqnf(p);
      38           1 :   std::clog << "bqnf_traverser says: p is " << (is_bqnf ? "" : "NOT ") << "in BQNF." << std::endl;
      39           1 :   bool is_ppg = pbes_system::detail::is_ppg(p);
      40           1 :   std::clog << "ppg_traverser says: p is " << (is_ppg ? "" : "NOT ") << "a PPG." << std::endl;
      41           1 :   std::clog << "Try the new rewriter:" << std::endl;
      42           1 :   pbes q = pbes_system::detail::to_ppg(p);
      43           1 :   std::clog << "The new rewriter is done." << std::endl;
      44             :   //std::clog << "result:" << std::endl << pbes_system::pp(q) << std::endl << std::endl;
      45           1 :   is_ppg = pbes_system::detail::is_ppg(q);
      46           1 :   std::clog << "ppg_traverser says: result is " << (is_ppg ? "" : "NOT ") << "a PPG." << std::endl;
      47           1 :   p = q;
      48           1 :   normalize(p);
      49           1 :   std::clog << "Parsing text..." << std::endl;
      50           1 :   pbes ppg = txt2pbes(ppg_text);
      51           1 :   normalize(ppg);
      52           1 :   std::clog << "Checking for equality..." << std::endl;
      53           1 :   if (!(p==ppg))
      54             :   {
      55           0 :     std::clog << "target:" << std::endl << ppg_text << std::endl << std::endl;
      56           0 :     std::clog << "result:" << std::endl << pbes_system::pp(p) << std::endl;
      57             :   }
      58           1 :   BOOST_CHECK(p==ppg);
      59           1 :   std::clog << "done." << std::endl;
      60           1 : }
      61             : 
      62             : 
      63           1 : void test_ppg_rewriter()
      64             : {
      65             :   // buffer.always_send_and_receive
      66             :   std::string bqnf_text =
      67             :       "sort D = struct d1 | d2;\n"
      68             :       "map  N: Pos;\n"
      69             :       "eqn  N  =  2;\n"
      70             :       "pbes nu X(q_Buffer: List(D)) =\n"
      71             :       "  (exists d: D. (val(#q_Buffer < 2) && X(q_Buffer <| d))) && (exists d: D. val(head(q_Buffer) == d) && val(!(q_Buffer == [])) && X(tail(q_Buffer)));\n"
      72           1 :       "init X([]);"
      73             :   ;
      74             :   std::string ppg_text =
      75             :       "sort D = struct d1 | d2;\n"
      76             :       "map  N: Pos;\n"
      77             :       "eqn  N  =  2;\n"
      78             :       "pbes nu X_1(q_Buffer: List(D)) =\n"
      79             :       "  exists d: D. val(#q_Buffer < 2) && X(q_Buffer <| d);\n"
      80             :       "nu X_2(q_Buffer: List(D)) =\n"
      81             :       "  exists d: D. val(head(q_Buffer) == d) && val(!(q_Buffer == [])) && X(tail(q_Buffer));\n"
      82             :       "nu X(q_Buffer: List(D)) =\n"
      83             :       "  X_1(q_Buffer) && X_2(q_Buffer);\n"
      84           1 :       "init X([]);"
      85             :   ;
      86           1 :   rewrite_ppg(bqnf_text, ppg_text);
      87           1 : }
      88             : 
      89             : 
      90           2 : BOOST_AUTO_TEST_CASE(test_main)
      91             : {
      92           1 :   test_ppg_rewriter();
      93           1 : }