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 one_point_rewriter_test.cpp
      10             : /// \brief Test for PBES rewriters.
      11             : 
      12             : #define BOOST_TEST_MODULE find_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : #include "mcrl2/data/rewriter.h"
      15             : #include "mcrl2/pbes/detail/parse.h"
      16             : #include "mcrl2/pbes/rewrite.h"
      17             : #include "mcrl2/pbes/rewriters/one_point_rule_rewriter.h"
      18             : #include "mcrl2/pbes/rewriters/simplify_rewriter.h"
      19             : #include "mcrl2/pbes/txt2pbes.h"
      20             : #include "mcrl2/utilities/detail/test_operation.h"
      21             : 
      22             : using namespace mcrl2;
      23             : using namespace mcrl2::pbes_system;
      24             : 
      25             : const std::string VARIABLE_SPECIFICATION =
      26             :   "datavar         \n"
      27             :   "  b:  Bool;     \n"
      28             :   "  b1: Bool;     \n"
      29             :   "  b2: Bool;     \n"
      30             :   "  b3: Bool;     \n"
      31             :   "                \n"
      32             :   "  n:  Nat;      \n"
      33             :   "  n1: Nat;      \n"
      34             :   "  n2: Nat;      \n"
      35             :   "  n3: Nat;      \n"
      36             :   "                \n"
      37             :   "  p:  Pos;      \n"
      38             :   "  p1: Pos;      \n"
      39             :   "  p2: Pos;      \n"
      40             :   "  p3: Pos;      \n"
      41             :   "                \n"
      42             :   "predvar         \n"
      43             :   "  X;            \n"
      44             :   "  Y: Nat;       \n"
      45             :   "  W: Bool;      \n"
      46             :   "  Z: Bool, Nat; \n"
      47             :   "  X0;           \n"
      48             :   "  X1: Bool;     \n"
      49             :   "  X2: Nat, Nat; \n"
      50             :   "  X3: Bool, Nat;\n"
      51             :   "  X4: Nat, Bool;\n"
      52             :   ;
      53             : 
      54             : // PBES expression parser
      55             : class parser
      56             : {
      57             :   protected:
      58             :     std::string m_var_decl;
      59             :     std::string m_data_spec;
      60             : 
      61             :   public:
      62          12 :     explicit parser(const std::string& var_decl = VARIABLE_SPECIFICATION, const std::string& data_spec = "")
      63          12 :       : m_var_decl(var_decl),
      64          12 :         m_data_spec(data_spec)
      65          12 :     {}
      66             : 
      67          24 :     pbes_expression operator()(const std::string& expr)
      68             :     {
      69          24 :       return pbes_system::parse_pbes_expression(expr, m_var_decl, m_data_spec);
      70             :     }
      71             : };
      72             : 
      73          12 : void test_one_point_rule_rewriter(const std::string& expr1, const std::string& expr2)
      74             : {
      75             :   one_point_rule_rewriter R;
      76          12 :   data::data_specification dataspec;
      77          12 :   dataspec.add_context_sort(data::sort_nat::nat()); // TODO: is there a more elegant way to achieve this?
      78          12 :   data::rewriter r(dataspec);
      79          12 :   simplify_data_rewriter<data::rewriter> S(r);
      80          36 :   BOOST_CHECK(utilities::detail::test_operation(
      81             :     expr1,
      82             :     expr2,
      83             :     parser(),
      84             :     std::equal_to<pbes_expression>(),
      85             :     [&](const pbes_expression& x) { return S(R(x)); },
      86             :     "R1",
      87             :     S,
      88             :     "R2"
      89             :   ));
      90          12 : }
      91             : 
      92           2 : BOOST_AUTO_TEST_CASE(one_point_rule_rewriter_test)
      93             : {
      94           1 :   std::cout << "<test_one_point_rule_rewriter>" << std::endl;
      95           1 :   test_one_point_rule_rewriter("forall n: Nat. val(n != 3) || val(n == 5)", "val(false)");
      96           1 :   test_one_point_rule_rewriter("exists n: Nat. val(n == 3) && val(n == 5)", "val(false)");
      97           1 :   test_one_point_rule_rewriter("forall c: Bool. forall b: Bool. val(b) => val(b || c)", "val(!false)");
      98           1 :   test_one_point_rule_rewriter("forall d:Nat. val(d == 1) => Y(d)", "Y(1)");
      99           1 :   test_one_point_rule_rewriter("forall m:Nat. exists n:Nat. val(m == n) && Y(n)", "forall m: Nat. Y(m)");
     100           1 :   test_one_point_rule_rewriter("forall m:Nat. exists n:Nat. val(n == m) && Y(n)", "forall m: Nat. Y(m)");
     101           1 :   test_one_point_rule_rewriter("exists m:Nat. forall n:Nat. val(m != n) || Y(n)", "exists m: Nat. Y(m)");
     102           1 :   test_one_point_rule_rewriter("exists m:Nat. forall n:Nat. val(n != m) || Y(n)", "exists m: Nat. Y(m)");
     103           1 :   test_one_point_rule_rewriter("forall p: Bool, q: Bool. val(!(p == q)) || val(!q) || val(!(p == true))", "val(false)");
     104           1 :   test_one_point_rule_rewriter("exists m:Nat. (val(m == 3) || val(false)) && Y(m)", "Y(3)");
     105           1 :   test_one_point_rule_rewriter("forall m:Nat. val(m != 3) && val(true)", "val(false)");
     106           1 :   test_one_point_rule_rewriter("exists k,l,m:Nat. val(k == l && k == m) && val(l == m)", "val(true)");
     107           1 : }
     108             : 
     109           2 : BOOST_AUTO_TEST_CASE(ticket_1388)
     110             : {
     111           1 :   std::string text;
     112           1 :   bool normalize = false;
     113           1 :   pbes p;
     114             :   one_point_rule_rewriter R;
     115             : 
     116             :   text =
     117             :     "pbes mu X = exists e: Bool. exists b: Bool, d: Bool. val(b == e) && val(d == b);\n"
     118           1 :     "init X;\n"
     119             :     ;
     120           1 :   p = txt2pbes(text, normalize);
     121           1 :   replace_pbes_expressions(p, R, false);
     122           1 :   BOOST_CHECK(p.is_closed() && p.is_well_typed());
     123             : 
     124             :   text =
     125             :     "pbes nu X = forall b,c: Bool. !val(b == false) || !val(c == b);\n"
     126           1 :     "init X;"
     127             :     ;
     128           1 :   p = txt2pbes(text, normalize);
     129           1 :   replace_pbes_expressions(p, R, false);
     130           1 :   BOOST_CHECK(p.is_closed() && p.is_well_typed());
     131           1 : }