LCOV - code coverage report
Current view: top level - pbes/test - constelm_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 73 81 90.1 %
Date: 2020-09-16 00:45:56 Functions: 5 5 100.0 %
Legend: Lines: hit not hit

          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 constelm_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE constelm_test
      13             : #include <boost/test/included/unit_test_framework.hpp>
      14             : #include "mcrl2/pbes/constelm.h"
      15             : #include "mcrl2/pbes/detail/pbes_property_map.h"
      16             : #include "mcrl2/pbes/remove_equations.h"
      17             : #include "mcrl2/pbes/rewriter.h"
      18             : #include "mcrl2/pbes/txt2pbes.h"
      19             : 
      20             : using namespace mcrl2;
      21             : using namespace mcrl2::pbes_system;
      22             : 
      23           1 : std::string t1 =
      24             :   "% simple test, n is constant \n"
      25             :   "                             \n"
      26             :   "pbes nu X(n: Nat) =          \n"
      27             :   "       X(n);                 \n"
      28             :   "                             \n"
      29             :   "init X(0);                   \n"
      30             :   ;
      31           1 : std::string x1 = "binding_variables = X";
      32             : 
      33           1 : std::string t2 =
      34             :   "% simple test, n is NOT constant \n"
      35             :   "                                 \n"
      36             :   "pbes nu X(n: Nat) =              \n"
      37             :   "       X(n + 1);                 \n"
      38             :   "                                 \n"
      39             :   "init X(0);                       \n"
      40             :   ;
      41           1 : std::string x2 = "binding_variables = X(n: Nat)";
      42             : 
      43           1 : std::string t3 =
      44             :   "% multiple parameters: n1 is constant, n2 is not \n"
      45             :   "                                                 \n"
      46             :   "pbes nu X(n1,n2: Nat) =                          \n"
      47             :   "       X(n1, n2 + 1);                            \n"
      48             :   "                                                 \n"
      49             :   "init X(0, 1);                                    \n"
      50             :   ;
      51           1 : std::string x3 = "binding_variables = X(n2: Nat)";
      52             : 
      53           1 : std::string t4 =
      54             :   "% conditions: n is not constant, even if conditions are enabled\n"
      55             :   "                                                               \n"
      56             :   "pbes nu X(n: Nat) =                                            \n"
      57             :   "       val(2 < n) || X(n + 1);                                 \n"
      58             :   "                                                               \n"
      59             :   "init X(0);                                                     \n"
      60             :   ;
      61           1 : std::string x4 = "binding_variables = X(n: Nat)";
      62             : 
      63           1 : std::string t5 =
      64             :   "% conditions: n is constant if conditions are enabled \n"
      65             :   "                                                      \n"
      66             :   "pbes nu X(n: Nat) =                                   \n"
      67             :   "       val(2 < n) || X(n + 1);                        \n"
      68             :   "                                                      \n"
      69             :   "init X(5);                                            \n"
      70             :   ;
      71           1 : std::string x5 = "binding_variables = X";
      72             : 
      73           1 : std::string t6 =
      74             :   "% reachability: n1 is not constant, equation Y is not reachable and should be removed \n"
      75             :   "                                                                                      \n"
      76             :   "pbes nu X(n1: Nat) = X(n1+1);                                                         \n"
      77             :   "     mu Y(n2: Nat) = Y(n2+1);                                                         \n"
      78             :   "                                                                                      \n"
      79             :   "init X(5);                                                                            \n"
      80             :   ;
      81           1 : std::string x6 = "binding_variables = X(n1: Nat)";
      82             : 
      83           1 : std::string t7 =
      84             :   "% multiple edges from one vertex, one edge invalidates the assertion of the other: no constants should be found \n"
      85             :   "                                                                                                                \n"
      86             :   "pbes                                                                                                            \n"
      87             :   "   mu X1(n1,m1:Nat) = X2(n1) || X2(m1);                                                                         \n"
      88             :   "   mu X2(n2:Nat)     = X1(n2,n2);                                                                               \n"
      89             :   "init                                                                                                            \n"
      90             :   "   X1(2,1);                                                                                                     \n"
      91             :   ;
      92           1 : std::string x7 = "binding_variables = X1(n1,m1: Nat), X2(n2: Nat)";
      93             : 
      94           1 : std::string t8 =
      95             :   "% conditions: parameters b,c and d will always be removed, with conditions on, parameter \n"
      96             :   "% n will NOT be removed. changing b,c or d to false or n to a bigger number              \n"
      97             :   "% then 5 WILL result in the removal of n                                                 \n"
      98             :   "                                                                                         \n"
      99             :   "pbes nu X(b,c,d:Bool, n:Nat) =                                                           \n"
     100             :   "    val(b) || ( val(c) && ( val(d) && (val(n > 5) || X(b,c,d,n+1))));                    \n"
     101             :   "                                                                                         \n"
     102             :   "init                                                                                     \n"
     103             :   "X(false,true,true,5);                                                                    \n"
     104             :   ;
     105           1 : std::string x8 = "binding_variables = X(n: Nat)";
     106             : 
     107           1 : std::string t9 =
     108             :   "% conditions: universal quantification which can be solved, n1 and n2 are \n"
     109             :   "% constants if conditions are enabled                                     \n"
     110             :   "                                                                          \n"
     111             :   "pbes mu X(n1,n2:Nat) =                                                    \n"
     112             :   "    forall m:Nat. (val(n1>n2) && X(n1+1,n2+1));                           \n"
     113             :   "                                                                          \n"
     114             :   "init X(1,2);                                                              \n"
     115             :   ;
     116           1 : std::string x9 = "binding_variables = X";
     117             : 
     118           1 : std::string t10 =
     119             :   "% conditions: existential quantification which can be solved, n1 and n2 \n"
     120             :   "% are constants if conditions are enabled                               \n"
     121             :   "                                                                        \n"
     122             :   "pbes mu X(n1,n2:Nat) =                                                  \n"
     123             :   "    exists m:Nat. (val(n1>n2) && X(n1+1,n2+1));                         \n"
     124             :   "                                                                        \n"
     125             :   "init X(1,2);                                                            \n"
     126             :   ;
     127           1 : std::string x10 = "binding_variables = X";
     128             : 
     129           1 : std::string t11 =
     130             :   "pbes mu X(n1,n2:Nat) =                                        \n"
     131             :   "    forall m:Nat. (val(m>n2) && X(n1+1,n2+1));                \n"
     132             :   "                                                              \n"
     133             :   "init X(1,2);                                                  \n"
     134             :   ;
     135           1 : std::string x11 = "binding_variables = X";
     136             : 
     137           1 : std::string t12 =
     138             :   "% example 4.2.1 from \"Tools for PBES\" report                                     \n"
     139             :   "% constants without conditions: o4, n2, n4, o4                                     \n"
     140             :   "% constants with conditions: everything (equations X1,X2,X3 and X4 are removed)    \n"
     141             :   "                                                                                   \n"
     142             :   "pbes                                                                               \n"
     143             :   "   mu X1(n1,m1,o1,p1:Nat) = (val(n1<m1) || X2(o1,p1)) && X3(n1) && X1(n1,m1,4,p1); \n"
     144             :   "   mu X2(n2,m2:Nat)       = X5(n2,m2) || X5(m2,n2);                                \n"
     145             :   "   nu X3(n3:Nat)          = val(n3<3) || X1(n3,n3,4,n3+1);                         \n"
     146             :   "   nu X4(n4,m4,o4:Nat)    = val(n4 <= m4+o4) || (X3(n4) && X4(n4,m4+1,n4));        \n"
     147             :   "   mu X5(n5,m5:Nat)       = val(n5>m5) || X3(n5);                                  \n"
     148             :   "                                                                                   \n"
     149             :   "init                                                                               \n"
     150             :   "   X4(0,0,0);                                                                      \n"
     151             :   ;
     152           1 : std::string x12 = "binding_variables = X1(n1,m1,p1: Nat), X2(m2: Nat), X3(n3: Nat), X4(m4: Nat), X5(n5,m5: Nat)";
     153             : 
     154           1 : std::string t13 =
     155             :   "pbes nu X =           \n"
     156             :   "        Y(true);      \n"
     157             :   "      mu Y(b: Bool) = \n"
     158             :   "        X;            \n"
     159             :   "                      \n"
     160             :   "init X;               \n"
     161             :   ;
     162           1 : std::string x13 = "binding_variables = X, Y";
     163             : 
     164           1 : std::string t14 =
     165             :   "pbes nu X(m:Nat) =           \n"
     166             :   "        forall n:Nat . X(n); \n"
     167             :   "                             \n"
     168             :   "init X(0);                   \n"
     169             :   ;
     170           1 : std::string x14 = "binding_variables = X(m: Nat)";
     171             : 
     172           1 : std::string t15 =
     173             :   "pbes                 \n"
     174             :   "nu X0(n:Nat) = X1;   \n"
     175             :   "mu X1 = X0(0) || X1; \n"
     176             :   "                     \n"
     177             :   "init X0(0);          \n"
     178             :   ;
     179           1 : std::string x15 = "binding_variables = X0, X1";
     180             : 
     181           1 : std::string t16 =
     182             :   "pbes                      \n"
     183             :   " nu X(n:Nat) = Y && X(n); \n"
     184             :   " mu Y = Z;                \n"
     185             :   " nu Z = Y;                \n"
     186             :   "                          \n"
     187             :   " init X(0);               \n"
     188             :   ;
     189           1 : std::string x16 = "binding_variables = X, Y, Z";
     190             : 
     191           1 : std::string t17 =
     192             :   "sort D = struct d1 | d2 | d3 | d4;\n"
     193             :   "pbes nu X1 =\n"
     194             :   "       X(2);\n"
     195             :   "     mu X(s3_X: Pos) =\n"
     196             :   "       val(s3_X == 4) || val(s3_X == 2) && X(3) || val(s3_X == 2) && X(4) || val(s3_X == 3) && X(1) || val(s3_X == 4) && X(1);\n"
     197             :   "init X1;\n";
     198             : 
     199           1 : std::string x17 = "binding_variables = X1, X(s3_X: Pos)";
     200             : 
     201           1 : std::string t18 =
     202             :   "% conditions: quantifications which cannot be solved, n1 and n2 are *not* \n"
     203             :   "% constants even if conditions are enabled.                               \n"
     204             :   "                                                                          \n"
     205             :   "pbes mu X(n1,n2:Nat) =                                                    \n"
     206             :   "    forall m1:Nat. exists m2:Nat. (val(m2 > n2 + m1) && X(n1+1,n2+1));    \n"
     207             :   "                                                                          \n"
     208             :   "init X(1,2);                                                              \n"
     209             :   ;
     210             : 
     211           1 : std::string x18 = "binding_variables = X(n1,n2: Nat)";
     212             : 
     213          18 : void test_pbes(const std::string& pbes_spec, const std::string& expected_result, bool compute_conditions, bool remove_equations = true)
     214             : {
     215             :   typedef simplify_data_rewriter<data::rewriter> my_pbes_rewriter;
     216             : 
     217          36 :   pbes p = txt2pbes(pbes_spec);
     218          36 :   pbes q = p;
     219             : 
     220             :   // data rewriter
     221          36 :   data::rewriter datar(q.data());
     222             : 
     223             :   // pbes rewriter
     224          18 :   my_pbes_rewriter pbesr(datar);
     225             : 
     226             :   // constelm algorithm
     227          36 :   pbes_constelm_algorithm<data::rewriter, my_pbes_rewriter> algorithm(datar, pbesr);
     228             : 
     229             :   // run the algorithm
     230          18 :   algorithm.run(q, compute_conditions);
     231          18 :   if (remove_equations)
     232             :   {
     233          18 :     remove_unreachable_variables(q);
     234             :   }
     235          18 :   BOOST_CHECK(q.is_well_typed());
     236          18 :   std::cout << "\n--- q ---\n" << pbes_system::pp(q) << std::endl;
     237             : 
     238          36 :   pbes_system::detail::pbes_property_map info1(q);
     239          36 :   pbes_system::detail::pbes_property_map info2(expected_result);
     240          36 :   std::string diff = info1.compare(info2);
     241          18 :   if (!diff.empty())
     242             :   {
     243           0 :     std::cerr << "\n------ FAILED TEST ------" << std::endl;
     244           0 :     std::cout << pbes_spec << std::endl;
     245           0 :     std::cerr << "--- expected result" << std::endl;
     246           0 :     std::cerr << expected_result << std::endl;
     247           0 :     std::cerr << "--- found result" << std::endl;
     248           0 :     std::cerr << info1.to_string() << std::endl;
     249           0 :     std::cerr << "--- differences" << std::endl;
     250           0 :     std::cerr << diff << std::endl;
     251             :   }
     252          18 :   BOOST_CHECK(diff.empty());
     253             : 
     254          18 : }
     255             : 
     256           3 : BOOST_AUTO_TEST_CASE(test_constelm)
     257             : {
     258           1 :   test_pbes(t1 , x1 , false);
     259           1 :   test_pbes(t2 , x2 , false);
     260           1 :   test_pbes(t3 , x3 , false);
     261           1 :   test_pbes(t4 , x4 , true);
     262           1 :   test_pbes(t5 , x5 , true);
     263           1 :   test_pbes(t6 , x6 , false);
     264           1 :   test_pbes(t7 , x7 , false);
     265           1 :   test_pbes(t8 , x8 , true);
     266           1 :   test_pbes(t9 , x9 , true);
     267           1 :   test_pbes(t10, x10, true);
     268           1 :   test_pbes(t11, x11, true);
     269           1 :   test_pbes(t12, x12, false);
     270           1 :   test_pbes(t13, x13, false);
     271           1 :   test_pbes(t14, x14, false);
     272           1 :   test_pbes(t15, x15, false);
     273           1 :   test_pbes(t16, x16, true);
     274           1 :   test_pbes(t17, x17, false);
     275           1 :   test_pbes(t18, x18, true);
     276           4 : }

Generated by: LCOV version 1.13