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

Generated by: LCOV version 1.13