LCOV - code coverage report
Current view: top level - lps/test - confcheck_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 38 38 100.0 %
Date: 2024-03-08 02:52:28 Functions: 12 12 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Unknown
       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 confcheck_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE confcheck_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/lps/confluence_checker.h"
      16             : #include "mcrl2/lps/parse.h"
      17             : 
      18             : 
      19             : using namespace mcrl2;
      20             : using namespace mcrl2::data;
      21             : using namespace mcrl2::core;
      22             : using namespace mcrl2::lps;
      23             : using namespace mcrl2::lps::detail;
      24             : 
      25             : //static bool check_for_ctau(lps::specification const& s) .
      26           5 : static std::size_t count_ctau(specification const& s)
      27             : {
      28           5 :   std::size_t result = 0;
      29           5 :   auto const& v_summands = s.process().action_summands();
      30             : 
      31          25 :   for (const auto & v_summand : v_summands)
      32             :   {
      33          20 :     const process::action_list al=v_summand.multi_action().actions();
      34          20 :     if (al.size()==1)
      35             :     {
      36          17 :       const process::action_label lab=al.front().label();
      37          17 :       if (pp(lab.name())=="ctau")
      38             :       {
      39           6 :         ++result;
      40             :       }
      41          17 :     }
      42          20 :   }
      43           5 :   return result;
      44             : }
      45             : 
      46             : static
      47           5 : void run_confluence_test_case(const std::string& s, const std::size_t ctau_count)
      48             : {
      49             :   using namespace mcrl2::lps;
      50             : 
      51           5 :   specification s0 = parse_linear_process_specification(s);
      52          10 :   Confluence_Checker<specification> checker1(s0);
      53             :   // Check confluence for all summands and
      54             :   // replace confluents tau's by ctau's.
      55           5 :   checker1.check_confluence_and_mark(data::sort_bool::true_(),0);
      56             : 
      57           5 :   BOOST_CHECK_EQUAL(count_ctau(s0), ctau_count);
      58           5 : }
      59             : 
      60           2 : BOOST_AUTO_TEST_CASE(case_1)
      61             : {
      62             :   /*
      63             :    act a, b;
      64             :    init tau.a + tau.b;
      65             :    */
      66             :   const std::string s(
      67             :       "act  Terminate,a,b;\n"
      68             :       "proc P(s3: Pos) =\n"
      69             :       "       (s3 == 5) ->\n"
      70             :       "         b .\n"
      71             :       "         P(s3 = 3)\n"
      72             :       "     + (s3 == 3) ->\n"
      73             :       "         Terminate .\n"
      74             :       "         P(s3 = 4)\n"
      75             :       "     + (s3 == 2) ->\n"
      76             :       "         a .\n"
      77             :       "         P(s3 = 3)\n"
      78             :       "     + sum e: Bool.\n"
      79             :       "         (if(e, true, true) && s3 == 1) ->\n"
      80             :       "         tau .\n"
      81             :       "         P(s3 = if(e, 5, 2))\n"
      82             :       "     + delta;\n"
      83             :       "init P(1);\n"
      84           1 :   );
      85             : 
      86           1 :   run_confluence_test_case(s,0);
      87           1 : }
      88             : 
      89             : 
      90           2 : BOOST_AUTO_TEST_CASE(case_2)
      91             : {
      92             :   /*
      93             :    act a, b;
      94             :    init a.tau.b.delta;
      95             :    */
      96             :   const std::string s(
      97             :     "act  a,b;\n"
      98             :     "proc P(s3: Pos) =\n"
      99             :     "       (s3 == 3) ->\n"
     100             :     "         b .\n"
     101             :     "         P(s3 = 4)\n"
     102             :     "     + (s3 == 2) ->\n"
     103             :     "         tau .\n"
     104             :     "         P(s3 = 3)\n"
     105             :     "     + (s3 == 1) ->\n"
     106             :     "         a .\n"
     107             :     "         P(s3 = 2)\n"
     108             :     "     + delta;\n"
     109             :     "init P(1);\n"
     110           1 :   );
     111             : 
     112           1 :   run_confluence_test_case(s,1);
     113           1 : }
     114             : 
     115           2 : BOOST_AUTO_TEST_CASE(case_3)
     116             : {
     117             :   /*
     118             :    act a, b;
     119             :    init a.b.delta;
     120             :    */
     121             :   const std::string s(
     122             :     "act  a,b;\n"
     123             :     "proc P(s3: Pos) =\n"
     124             :     "       (s3 == 2) ->\n"
     125             :     "         b .\n"
     126             :     "         P(s3 = 3)\n"
     127             :     "     + (s3 == 1) ->\n"
     128             :     "         a .\n"
     129             :     "         P(s3 = 2)\n"
     130             :     "     + delta;\n"
     131             :     "init P(1);\n"
     132           1 :     );
     133           1 :   run_confluence_test_case(s,0);
     134           1 : }
     135             : 
     136             : // The following test case unearthed an assertion failure when applying
     137             : // substitutions.
     138           2 : BOOST_AUTO_TEST_CASE(case_4)
     139             : {
     140             :   const std::string s(
     141             :     "proc P(m: Int) =\n"
     142             :     "       (m == 1) ->\n"
     143             :     "         tau .\n"
     144             :     "         P(m = m - 1)\n"
     145             :     "     + (m == 1) ->\n"
     146             :     "         tau .\n"
     147             :     "         P()\n"
     148             :     "     + delta;\n"
     149             :     "\n"
     150             :     "init P(0);\n"
     151           1 :     );
     152           1 :   run_confluence_test_case(s,0);
     153           1 : }
     154             : 
     155             : // Test case provided by Jaco van der Pol
     156             : // in some versions the algorithm hangs on this example.
     157           2 : BOOST_AUTO_TEST_CASE(case_5)
     158             : {
     159             :   const std::string s(
     160             :       "sort Byte = struct ESC | END | OTHER;\n"
     161             :       "     Enum3 = struct e2_3 | e1_3 | e0_3;\n"
     162             :       "     Enum4 = struct e3_4 | e2_4 | e1_4 | e0_4;\n"
     163             :       "map  special: Byte -> Bool;\n"
     164             :       "var  b: Byte;\n"
     165             :       "eqn  special(b)  =  b == ESC || b == END;\n"
     166             :       "act  r,s,r1,s1,r2,s2,c1,c2: Byte;\n"
     167             :       "proc P(s3_S: Enum3, b_S: Byte, s30_C: Bool, b_C: Byte, s31_R: Enum4, b_R,b0_R: Byte) =\n"
     168             :       "       sum b1_S: Byte.\n"
     169             :       "         (s3_S == e2_3 && !(b1_S == ESC || b1_S == END)) ->\n"
     170             :       "         r(b1_S) .\n"
     171             :       "         P(s3_S = e0_3, b_S = b1_S)\n"
     172             :       "     + sum b2_S: Byte.\n"
     173             :       "         (s3_S == e2_3 && (b2_S == ESC || b2_S == END)) ->\n"
     174             :       "         r(b2_S) .\n"
     175             :       "         P(s3_S = e1_3, b_S = b2_S)\n"
     176             :       "     + ((s30_C && s31_R == e3_4) && ESC == b_C) ->\n"
     177             :       "         tau .\n"
     178             :       "         P(s30_C = false, b_C = ESC, s31_R = e2_4, b_R = ESC, b0_R = ESC)\n"
     179             :       "     + ((s30_C && s31_R == e3_4) && !(b_C == ESC)) ->\n"
     180             :       "         tau .\n"
     181             :       "         P(s30_C = false, b_C = ESC, s31_R = e0_4, b_R = b_C, b0_R = ESC)\n"
     182             :       "     + (s30_C && s31_R == e2_4) ->\n"
     183             :       "         tau .\n"
     184             :       "         P(s30_C = false, b_C = ESC, s31_R = e1_4, b_R = ESC, b0_R = b_C)\n"
     185             :       "     + (s31_R == e1_4) ->\n"
     186             :       "         s(b0_R) .\n"
     187             :       "         P(s31_R = e3_4, b_R = ESC, b0_R = ESC)\n"
     188             :       "     + (s31_R == e0_4) ->\n"
     189             :       "         s(b_R) .\n"
     190             :       "         P(s31_R = e3_4, b_R = ESC, b0_R = ESC)\n"
     191             :       "     + (s3_S == e0_3 && !s30_C) ->\n"
     192             :       "         tau .\n"
     193             :       "         P(s3_S = e2_3, b_S = ESC, s30_C = true, b_C = b_S)\n"
     194             :       "     + (s3_S == e1_3 && !s30_C) ->\n"
     195             :       "         tau .\n"
     196             :       "         P(s3_S = e0_3, s30_C = true, b_C = ESC)\n"
     197             :       "     + delta;\n"
     198             :       "init P(e2_3, ESC, false, ESC, e3_4, ESC, ESC);\n"
     199           1 :   );
     200           1 :   run_confluence_test_case(s,5);
     201           1 : }
     202             : 

Generated by: LCOV version 1.14