LCOV - code coverage report
Current view: top level - lts/test - lts_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 301 304 99.0 %
Date: 2020-02-19 00:44:21 Functions: 19 19 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): anonymous
       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 lts_test.cpp
      10             : /// \brief Add your file description here.
      11             : 
      12             : #define BOOST_TEST_MODULE lts_test
      13             : #include <boost/test/included/unit_test_framework.hpp>
      14             : 
      15             : #include "mcrl2/lts/lts_algorithm.h"
      16             : 
      17             : using namespace mcrl2;
      18             : 
      19             : class expected_sizes
      20             : {
      21             :   public:
      22             :     std::size_t states_plain, transitions_plain, labels_plain;
      23             :     std::size_t states_bisimulation, transitions_bisimulation, labels_bisimulation;
      24             :     std::size_t states_branching_bisimulation, transitions_branching_bisimulation, labels_branching_bisimulation;
      25             :     std::size_t states_divergence_preserving_branching_bisimulation, transitions_divergence_preserving_branching_bisimulation, labels_divergence_preserving_branching_bisimulation;
      26             :     std::size_t states_weak_bisimulation, transitions_weak_bisimulation, labels_weak_bisimulation;
      27             :     std::size_t states_divergence_preserving_weak_bisimulation, transitions_divergence_preserving_weak_bisimulation, labels_divergence_preserving_weak_bisimulation;
      28             :     std::size_t states_simulation, transitions_simulation, labels_simulation;
      29             :     std::size_t states_trace_equivalence, transitions_trace_equivalence, labels_trace_equivalence;
      30             :     std::size_t states_weak_trace_equivalence, transitions_weak_trace_equivalence, labels_weak_trace_equivalence;
      31             :     std::size_t states_determinisation, transitions_determinisation, labels_determinisation;
      32             :     bool is_deterministic;
      33             : };
      34             : 
      35         116 : static void test_lts(const std::string& test_description,
      36             :               const lts::lts_aut_t& l,
      37             :               std::size_t expected_label_count,
      38             :               std::size_t expected_state_count,
      39             :               std::size_t expected_transition_count
      40             :              )
      41             : {
      42         116 :   std::cerr << "LPS test: " << test_description << " -----------------------------------------------\n";
      43         116 :   BOOST_CHECK(l.num_action_labels() == expected_label_count);
      44         116 :   if (l.num_action_labels() != expected_label_count)
      45             :   {
      46           0 :     std::cerr << "Expected # of labels " << expected_label_count << " Actual # " << l.num_action_labels() << "\n";
      47             :   }
      48         116 :   BOOST_CHECK(l.num_states() == expected_state_count);
      49         116 :   if (l.num_states() != expected_state_count)
      50             :   {
      51           0 :     std::cerr << "Expected # of states " << expected_state_count << " Actual # " << l.num_states() << "\n";
      52             :   }
      53         116 :   BOOST_CHECK(l.num_transitions() == expected_transition_count);
      54         116 :   if (l.num_transitions() != expected_transition_count)
      55             :   {
      56           0 :     std::cerr << "Expected # of transitions " << expected_transition_count << " Actual # " << l.num_transitions() << "\n";
      57             :   }
      58         116 : }
      59             : 
      60           5 : static void reduce_lts_in_various_ways(const std::string& test_description,
      61             :                                        const std::string& lts,
      62             :                                        const expected_sizes& expected)
      63             : {
      64          10 :   std::istringstream is(lts);
      65          10 :   lts::lts_aut_t l_in;
      66           5 :   l_in.load(is);
      67           5 :   test_lts(test_description + " (plain input)",l_in, expected.labels_plain,expected.states_plain, expected.transitions_plain);
      68          10 :   lts::lts_aut_t l=l_in;
      69           5 :   reduce(l,lts::lts_eq_none);
      70           5 :   test_lts(test_description + " (no reduction)",l, expected.labels_plain,expected.states_plain, expected.transitions_plain);
      71           5 :   l=l_in;
      72           5 :   reduce(l,lts::lts_eq_bisim);
      73           5 :   test_lts(test_description + " (bisimulation [Jansen/Groote/Keiren/Wijs 2019])",l, expected.labels_bisimulation,expected.states_bisimulation, expected.transitions_bisimulation);
      74           5 :   l=l_in;
      75           5 :   reduce(l,lts::lts_eq_bisim_gv);
      76           5 :   test_lts(test_description + " (bisimulation [Groote/Vaandrager 1990])",l, expected.labels_bisimulation,expected.states_bisimulation, expected.transitions_bisimulation);
      77           5 :   l=l_in;
      78           5 :   reduce(l,lts::lts_eq_bisim_gjkw);
      79           5 :   test_lts(test_description + " (bisimulation [Groote/Jansen/Keiren/Wijs 2017)",l, expected.labels_bisimulation,expected.states_bisimulation, expected.transitions_bisimulation);
      80           5 :   l=l_in;
      81           5 :   reduce(l,lts::lts_eq_bisim_sigref);
      82           5 :   test_lts(test_description + " (bisimulation signature [Blom/Orzan 2003])",l, expected.labels_bisimulation,expected.states_bisimulation, expected.transitions_bisimulation);
      83           5 :   l=l_in;
      84           5 :   reduce(l,lts::lts_eq_branching_bisim);
      85           5 :   test_lts(test_description + " (branching bisimulation [Jansen/Groote/Keiren/Wijs 2019])",l, expected.labels_branching_bisimulation,expected.states_branching_bisimulation, expected.transitions_branching_bisimulation);
      86           5 :   l=l_in;
      87           5 :   reduce(l,lts::lts_eq_branching_bisim_gv);
      88           5 :   test_lts(test_description + " (branching bisimulation [Groote/Vaandrager 1990])",l, expected.labels_branching_bisimulation,expected.states_branching_bisimulation, expected.transitions_branching_bisimulation);
      89           5 :   l=l_in;
      90           5 :   reduce(l,lts::lts_eq_branching_bisim_gjkw);
      91           5 :   test_lts(test_description + " (branching bisimulation [Groote/Jansen/Keiren/Wijs 2017])",l, expected.labels_branching_bisimulation,expected.states_branching_bisimulation, expected.transitions_branching_bisimulation);
      92           5 :   l=l_in;
      93           5 :   reduce(l,lts::lts_eq_branching_bisim_sigref);
      94           5 :   test_lts(test_description + " (branching bisimulation signature [Blom/Orzan 2003])",l, expected.labels_branching_bisimulation,expected.states_branching_bisimulation, expected.transitions_branching_bisimulation);
      95           5 :   l=l_in;
      96           5 :   reduce(l,lts::lts_eq_divergence_preserving_branching_bisim);
      97           5 :   test_lts(test_description + " (divergence-preserving branching bisimulation [Jansen/Groote/Keiren/Wijs 2019])",l,
      98           5 :                                       expected.labels_divergence_preserving_branching_bisimulation,
      99           5 :                                       expected.states_divergence_preserving_branching_bisimulation,
     100           5 :                                       expected.transitions_divergence_preserving_branching_bisimulation);
     101           5 :   l=l_in;
     102           5 :   reduce(l,lts::lts_eq_divergence_preserving_branching_bisim_gv);
     103           5 :   test_lts(test_description + " (divergence-preserving branching bisimulation [Groote/Vaandrager 1990])",l,
     104           5 :                                       expected.labels_divergence_preserving_branching_bisimulation,
     105           5 :                                       expected.states_divergence_preserving_branching_bisimulation,
     106           5 :                                       expected.transitions_divergence_preserving_branching_bisimulation);
     107           5 :   l=l_in;
     108           5 :   reduce(l,lts::lts_eq_divergence_preserving_branching_bisim_gjkw);
     109           5 :   test_lts(test_description + " (divergence-preserving branching bisimulation [Groote/Jansen/Keiren/Wijs 2017])",l,
     110           5 :                                      expected.labels_divergence_preserving_branching_bisimulation,
     111           5 :                                      expected.states_divergence_preserving_branching_bisimulation,
     112           5 :                                      expected.transitions_divergence_preserving_branching_bisimulation);
     113           5 :   l=l_in;
     114           5 :   reduce(l,lts::lts_eq_divergence_preserving_branching_bisim_sigref);
     115           5 :   test_lts(test_description + " (divergence-preserving branching bisimulation signature [Blom/Orzan 2003])",l,
     116           5 :                                       expected.labels_divergence_preserving_branching_bisimulation,
     117           5 :                                       expected.states_divergence_preserving_branching_bisimulation,
     118           5 :                                       expected.transitions_divergence_preserving_branching_bisimulation);
     119           5 :   l=l_in;
     120           5 :   reduce(l,lts::lts_eq_weak_bisim);
     121           5 :   test_lts(test_description + " (weak bisimulation)",l, expected.labels_weak_bisimulation,expected.states_weak_bisimulation, expected.transitions_weak_bisimulation);
     122           5 :   l=l_in;
     123           5 :   reduce(l,lts::lts_eq_divergence_preserving_weak_bisim);
     124           5 :   test_lts(test_description + " (divergence-preserving weak bisimulation)",l,
     125           5 :                                       expected.labels_divergence_preserving_weak_bisimulation,
     126           5 :                                       expected.states_divergence_preserving_weak_bisimulation,
     127           5 :                                       expected.transitions_divergence_preserving_weak_bisimulation);
     128           5 :   l=l_in;
     129           5 :   reduce(l,lts::lts_eq_sim);
     130           5 :   test_lts(test_description + " (simulation equivalence)",l, expected.labels_simulation,expected.states_simulation, expected.transitions_simulation);
     131           5 :   l=l_in;
     132           5 :   reduce(l,lts::lts_eq_trace);
     133           5 :   test_lts(test_description + " (trace equivalence)",l, expected.labels_trace_equivalence,expected.states_trace_equivalence, expected.transitions_trace_equivalence);
     134           5 :   l=l_in;
     135           5 :   reduce(l,lts::lts_eq_weak_trace);
     136           5 :   test_lts(test_description + " (weak trace equivalence)",l, expected.labels_weak_trace_equivalence,expected.states_weak_trace_equivalence, expected.transitions_weak_trace_equivalence);
     137           5 :   l=l_in;
     138           5 :   if (expected.is_deterministic)
     139             :   {
     140           3 :     BOOST_CHECK(is_deterministic(l));
     141             :   }
     142             :   else
     143             :   {
     144           2 :     BOOST_CHECK(!is_deterministic(l));
     145             :   }
     146             : 
     147           5 :   reduce(l,lts::lts_red_determinisation);
     148           5 :   test_lts(test_description + " (determinisation)",l, expected.labels_determinisation,expected.states_determinisation, expected.transitions_determinisation);
     149           5 :   BOOST_CHECK(is_deterministic(l));
     150           5 : }
     151             : 
     152           1 : static void reduce_simple_loop()
     153             : {
     154             :   std::string SIMPLE_AUT =
     155             :     "des (0,2,2)\n"
     156             :     "(0,\"a\",1)\n"
     157           2 :     "(1,\"a\",0)\n"
     158             :     ;
     159             : 
     160             :   expected_sizes expected;
     161           1 :   expected.states_plain=2; expected.transitions_plain=2; expected.labels_plain=2;
     162           1 :   expected.states_bisimulation=1, expected.transitions_bisimulation=1, expected.labels_bisimulation=2;
     163           1 :   expected.states_branching_bisimulation=1, expected.transitions_branching_bisimulation=1, expected.labels_branching_bisimulation=2;
     164           1 :   expected.states_divergence_preserving_branching_bisimulation=1, expected.transitions_divergence_preserving_branching_bisimulation=1, expected.labels_divergence_preserving_branching_bisimulation=2;
     165           1 :   expected.states_weak_bisimulation=1, expected.transitions_weak_bisimulation=1, expected.labels_weak_bisimulation=2;
     166           1 :   expected.states_divergence_preserving_weak_bisimulation=1, expected.transitions_divergence_preserving_weak_bisimulation=1, expected.labels_divergence_preserving_weak_bisimulation=3;
     167           1 :   expected.states_simulation=1, expected.transitions_simulation=1, expected.labels_simulation=2;
     168           1 :   expected.states_trace_equivalence=1, expected.transitions_trace_equivalence=1, expected.labels_trace_equivalence=2;
     169           1 :   expected.states_weak_trace_equivalence=1, expected.transitions_weak_trace_equivalence=1, expected.labels_weak_trace_equivalence=2;
     170           1 :   expected.states_determinisation=2, expected.transitions_determinisation=2, expected.labels_determinisation=2;
     171           1 :   expected.is_deterministic=true;
     172             : 
     173           1 :   reduce_lts_in_various_ways("Simple loop", SIMPLE_AUT, expected);
     174           1 : }
     175             : 
     176           1 : static void reduce_simple_loop_with_tau()
     177             : {
     178             :   std::string SIMPLE_AUT =
     179             :     "des (0,2,2)\n"
     180             :     "(0,\"a\",1)\n"
     181           2 :     "(1,\"tau\",0)\n"
     182             :     ;
     183             : 
     184             :   expected_sizes expected;
     185           1 :   expected.states_plain=2; expected.transitions_plain=2; expected.labels_plain=2;
     186           1 :   expected.states_bisimulation=2, expected.transitions_bisimulation=2, expected.labels_bisimulation=2;
     187           1 :   expected.states_branching_bisimulation=1, expected.transitions_branching_bisimulation=1, expected.labels_branching_bisimulation=2;
     188           1 :   expected.states_divergence_preserving_branching_bisimulation=1, expected.transitions_divergence_preserving_branching_bisimulation=1, expected.labels_divergence_preserving_branching_bisimulation=2;
     189           1 :   expected.states_weak_bisimulation=1, expected.transitions_weak_bisimulation=1, expected.labels_weak_bisimulation=2;
     190           1 :   expected.states_divergence_preserving_weak_bisimulation=1, expected.transitions_divergence_preserving_weak_bisimulation=1, expected.labels_divergence_preserving_weak_bisimulation=3;
     191           1 :   expected.states_simulation=2, expected.transitions_simulation=2, expected.labels_simulation=2;
     192           1 :   expected.states_trace_equivalence=2, expected.transitions_trace_equivalence=2, expected.labels_trace_equivalence=2;
     193           1 :   expected.states_weak_trace_equivalence=1, expected.transitions_weak_trace_equivalence=1, expected.labels_weak_trace_equivalence=2;
     194           1 :   expected.states_determinisation=2, expected.transitions_determinisation=2, expected.labels_determinisation=2;
     195           1 :   expected.is_deterministic=true;
     196             : 
     197           1 :   reduce_lts_in_various_ways("Simple loop with tau", SIMPLE_AUT, expected);
     198           1 : }
     199             : 
     200             : /* The example below was encountered by David Jansen. The problem is that
     201             :  * for branching bisimulations the tau may supersede the b, not leading to the
     202             :  * necessary splitting into two equivalence classes. */
     203           1 : static void tricky_example_for_branching_bisimulation()
     204             : {
     205             :   std::string TRICKY_BB =
     206             :     "des (0,3,2)\n"
     207             :     "(0,\"a\",1)\n"
     208             :     "(1,\"b\",0)\n"
     209           2 :     "(1,\"tau\",0)\n"
     210             :     ;
     211             : 
     212             :   expected_sizes expected;
     213           1 :   expected.states_plain=2; expected.transitions_plain=3; expected.labels_plain=3;
     214           1 :   expected.states_bisimulation=2, expected.transitions_bisimulation=3, expected.labels_bisimulation=3;
     215           1 :   expected.states_branching_bisimulation=2, expected.transitions_branching_bisimulation=3, expected.labels_branching_bisimulation=3;
     216           1 :   expected.states_divergence_preserving_branching_bisimulation=2, expected.transitions_divergence_preserving_branching_bisimulation=3, expected.labels_divergence_preserving_branching_bisimulation=3;
     217           1 :   expected.states_weak_bisimulation=2, expected.transitions_weak_bisimulation=3, expected.labels_weak_bisimulation=3;
     218           1 :   expected.states_divergence_preserving_weak_bisimulation=2, expected.transitions_divergence_preserving_weak_bisimulation=3, expected.labels_divergence_preserving_weak_bisimulation=4;
     219           1 :   expected.states_simulation=2, expected.transitions_simulation=3, expected.labels_simulation=3;
     220           1 :   expected.states_trace_equivalence=2, expected.transitions_trace_equivalence=3, expected.labels_trace_equivalence=3;
     221           1 :   expected.states_weak_trace_equivalence=2, expected.transitions_weak_trace_equivalence=3, expected.labels_weak_trace_equivalence=3;
     222           1 :   expected.states_determinisation=2, expected.transitions_determinisation=3, expected.labels_determinisation=3;
     223           1 :   expected.is_deterministic=true;
     224             : 
     225           1 :   reduce_lts_in_various_ways("Tricky example for branching bisimulation", TRICKY_BB, expected);
     226           1 : }
     227             : 
     228             : 
     229           1 : static void reduce_abp()
     230             : {
     231             :   std::string ABP_AUT =
     232             :     "des (0,92,74)\n"
     233             :     "(0,\"r1(d1)\",1)\n"
     234             :     "(0,\"r1(d2)\",2)\n"
     235             :     "(1,\"tau\",3)\n"
     236             :     "(2,\"tau\",4)\n"
     237             :     "(3,\"tau\",5)\n"
     238             :     "(3,\"tau\",6)\n"
     239             :     "(4,\"tau\",7)\n"
     240             :     "(4,\"tau\",8)\n"
     241             :     "(5,\"tau\",9)\n"
     242             :     "(6,\"tau\",10)\n"
     243             :     "(7,\"tau\",11)\n"
     244             :     "(8,\"tau\",12)\n"
     245             :     "(9,\"tau\",13)\n"
     246             :     "(10,\"s4(d1)\",14)\n"
     247             :     "(11,\"tau\",15)\n"
     248             :     "(12,\"s4(d2)\",16)\n"
     249             :     "(13,\"tau\",17)\n"
     250             :     "(13,\"tau\",18)\n"
     251             :     "(14,\"tau\",19)\n"
     252             :     "(15,\"tau\",20)\n"
     253             :     "(15,\"tau\",21)\n"
     254             :     "(16,\"tau\",22)\n"
     255             :     "(17,\"tau\",1)\n"
     256             :     "(18,\"tau\",1)\n"
     257             :     "(19,\"tau\",23)\n"
     258             :     "(19,\"tau\",24)\n"
     259             :     "(20,\"tau\",2)\n"
     260             :     "(21,\"tau\",2)\n"
     261             :     "(22,\"tau\",25)\n"
     262             :     "(22,\"tau\",26)\n"
     263             :     "(23,\"tau\",27)\n"
     264             :     "(24,\"tau\",28)\n"
     265             :     "(25,\"tau\",29)\n"
     266             :     "(26,\"tau\",28)\n"
     267             :     "(27,\"tau\",30) \n"
     268             :     "(28,\"r1(d1)\",31)\n"
     269             :     "(28,\"r1(d2)\",32)\n"
     270             :     "(29,\"tau\",33)\n"
     271             :     "(30,\"tau\",34)\n"
     272             :     "(30,\"tau\",35)\n"
     273             :     "(31,\"tau\",36)\n"
     274             :     "(32,\"tau\",37)\n"
     275             :     "(33,\"tau\",38)\n"
     276             :     "(33,\"tau\",39)\n"
     277             :     "(34,\"tau\",40)\n"
     278             :     "(35,\"tau\",40)\n"
     279             :     "(36,\"tau\",41)\n"
     280             :     "(36,\"tau\",42)\n"
     281             :     "(37,\"tau\",43)\n"
     282             :     "(37,\"tau\",44)\n"
     283             :     "(38,\"tau\",45)\n"
     284             :     "(39,\"tau\",45)\n"
     285             :     "(40,\"tau\",19)\n"
     286             :     "(41,\"tau\",46)\n"
     287             :     "(42,\"tau\",47)\n"
     288             :     "(43,\"tau\",48)\n"
     289             :     "(44,\"tau\",49)\n"
     290             :     "(45,\"tau\",22)\n"
     291             :     "(46,\"tau\",50)\n"
     292             :     "(47,\"s4(d1)\",51)\n"
     293             :     "(48,\"tau\",52)\n"
     294             :     "(49,\"s4(d2)\",53)\n"
     295             :     "(50,\"tau\",54)\n"
     296             :     "(50,\"tau\",55)\n"
     297             :     "(51,\"tau\",56)\n"
     298             :     "(52,\"tau\",57)\n"
     299             :     "(52,\"tau\",58)\n"
     300             :     "(53,\"tau\",59)\n"
     301             :     "(54,\"tau\",31)\n"
     302             :     "(55,\"tau\",31)\n"
     303             :     "(56,\"tau\",60)\n"
     304             :     "(56,\"tau\",61)\n"
     305             :     "(57,\"tau\",32)\n"
     306             :     "(58,\"tau\",32)\n"
     307             :     "(59,\"tau\",62)\n"
     308             :     "(59,\"tau\",63)\n"
     309             :     "(60,\"tau\",64)\n"
     310             :     "(61,\"tau\",0)\n"
     311             :     "(62,\"tau\",65)\n"
     312             :     "(63,\"tau\",0)\n"
     313             :     "(64,\"tau\",66)\n"
     314             :     "(65,\"tau\",67)\n"
     315             :     "(66,\"tau\",68)\n"
     316             :     "(66,\"tau\",69)\n"
     317             :     "(67,\"tau\",70)\n"
     318             :     "(67,\"tau\",71)\n"
     319             :     "(68,\"tau\",72)\n"
     320             :     "(69,\"tau\",72)\n"
     321             :     "(70,\"tau\",73)\n"
     322             :     "(71,\"tau\",73)\n"
     323             :     "(72,\"tau\",56)\n"
     324           2 :     "(73,\"tau\",59)\n"
     325             :     ;
     326             : 
     327             :   expected_sizes expected;
     328           1 :   expected.states_plain=74; expected.transitions_plain=92; expected.labels_plain=5;
     329           1 :   expected.states_bisimulation=24, expected.transitions_bisimulation=28, expected.labels_bisimulation=5;
     330           1 :   expected.states_branching_bisimulation=3, expected.transitions_branching_bisimulation=4, expected.labels_branching_bisimulation=5;
     331           1 :   expected.states_divergence_preserving_branching_bisimulation=6, expected.transitions_divergence_preserving_branching_bisimulation=10, expected.labels_divergence_preserving_branching_bisimulation=5;
     332           1 :   expected.states_weak_bisimulation=3, expected.transitions_weak_bisimulation=4, expected.labels_weak_bisimulation=5;
     333           1 :   expected.states_divergence_preserving_weak_bisimulation=6, expected.transitions_divergence_preserving_weak_bisimulation=10, expected.labels_divergence_preserving_weak_bisimulation=6;
     334           1 :   expected.states_simulation=24, expected.transitions_simulation=28, expected.labels_simulation=5;
     335           1 :   expected.states_trace_equivalence=19, expected.transitions_trace_equivalence=24, expected.labels_trace_equivalence=5;
     336           1 :   expected.states_weak_trace_equivalence=3, expected.transitions_weak_trace_equivalence=4, expected.labels_weak_trace_equivalence=5;
     337           1 :   expected.states_determinisation=53, expected.transitions_determinisation=66, expected.labels_determinisation=5;
     338           1 :   expected.is_deterministic=false;
     339             : 
     340           1 :   reduce_lts_in_various_ways("Alternating bit protocol", ABP_AUT, expected);
     341           1 : }
     342             : 
     343             : // Peterson's protocol has the interesting property that the number of states modulo branching bisimulation
     344             : // differs from the number of states modulo weak bisimulation, as observed by Rob van Glabbeek.
     345           1 : static void reduce_peterson()
     346             : {
     347             :   std::string PETERSON_AUT =
     348             :     "des (0,59,35)\n"
     349             :     "(0,\"wish(1)\",1)\n"
     350             :     "(0,\"wish(0)\",2)\n"
     351             :     "(1,\"tau\",3)\n"
     352             :     "(1,\"wish(0)\",4)\n"
     353             :     "(2,\"wish(1)\",4)\n"
     354             :     "(2,\"tau\",5)\n"
     355             :     "(3,\"tau\",6)\n"
     356             :     "(3,\"wish(0)\",7)\n"
     357             :     "(4,\"tau\",7)\n"
     358             :     "(4,\"tau\",8)\n"
     359             :     "(5,\"wish(1)\",8)\n"
     360             :     "(6,\"enter(1)\",9)\n"
     361             :     "(6,\"wish(0)\",10)\n"
     362             :     "(7,\"tau\",11)\n"
     363             :     "(8,\"tau\",12)\n"
     364             :     "(9,\"leave(1)\",13)\n"
     365             :     "(9,\"wish(0)\",14)\n"
     366             :     "(10,\"enter(1)\",14)\n"
     367             :     "(10,\"tau\",15)\n"
     368             :     "(11,\"tau\",15)\n"
     369             :     "(12,\"tau\",16)\n"
     370             :     "(13,\"tau\",17)\n"
     371             :     "(13,\"wish(0)\",18)\n"
     372             :     "(14,\"leave(1)\",18)\n"
     373             :     "(14,\"tau\",19)\n"
     374             :     "(15,\"enter(1)\",19)\n"
     375             :     "(16,\"enter(0)\",20)\n"
     376             :     "(17,\"wish(1)\",1)\n"
     377             :     "(17,\"wish(0)\",21)\n"
     378             :     "(18,\"tau\",21)\n"
     379             :     "(18,\"tau\",22)\n"
     380             :     "(19,\"leave(1)\",22)\n"
     381             :     "(20,\"leave(0)\",23)\n"
     382             :     "(21,\"wish(1)\",4)\n"
     383             :     "(21,\"tau\",24)\n"
     384             :     "(22,\"tau\",24)\n"
     385             :     "(23,\"tau\",3)\n"
     386             :     "(24,\"wish(1)\",8)\n"
     387             :     "(24,\"tau\",25)\n"
     388             :     "(25,\"enter(0)\",26)\n"
     389             :     "(25,\"wish(1)\",27)\n"
     390             :     "(26,\"leave(0)\",28)\n"
     391             :     "(26,\"wish(1)\",29)\n"
     392             :     "(27,\"enter(0)\",29)\n"
     393             :     "(27,\"tau\",16)\n"
     394             :     "(28,\"wish(1)\",30)\n"
     395             :     "(28,\"tau\",31)\n"
     396             :     "(29,\"leave(0)\",30)\n"
     397             :     "(29,\"tau\",20)\n"
     398             :     "(30,\"tau\",23)\n"
     399             :     "(30,\"tau\",32)\n"
     400             :     "(31,\"wish(1)\",32)\n"
     401             :     "(31,\"wish(0)\",33)\n"
     402             :     "(32,\"tau\",3)\n"
     403             :     "(32,\"wish(0)\",34)\n"
     404             :     "(33,\"wish(1)\",34)\n"
     405             :     "(33,\"tau\",24)\n"
     406             :     "(34,\"tau\",7)\n"
     407           2 :     "(34,\"tau\",8)\n"
     408             :     ;
     409             : 
     410             :   expected_sizes expected;
     411           1 :   expected.states_plain=35; expected.transitions_plain=59; expected.labels_plain=7;
     412           1 :   expected.states_bisimulation=31, expected.transitions_bisimulation=51, expected.labels_bisimulation=7;
     413           1 :   expected.states_branching_bisimulation=21, expected.transitions_branching_bisimulation=37, expected.labels_branching_bisimulation=7;
     414           1 :   expected.states_divergence_preserving_branching_bisimulation=21, expected.transitions_divergence_preserving_branching_bisimulation=37, expected.labels_divergence_preserving_branching_bisimulation=7;
     415           1 :   expected.states_weak_bisimulation=19, expected.transitions_weak_bisimulation=33, expected.labels_weak_bisimulation=7;
     416           1 :   expected.states_divergence_preserving_weak_bisimulation=19, expected.transitions_divergence_preserving_weak_bisimulation=33, expected.labels_divergence_preserving_weak_bisimulation=8;
     417           1 :   expected.states_simulation=31, expected.transitions_simulation=49, expected.labels_simulation=7;
     418           1 :   expected.states_trace_equivalence=34, expected.transitions_trace_equivalence=52, expected.labels_trace_equivalence=7;
     419           1 :   expected.states_weak_trace_equivalence=18, expected.transitions_weak_trace_equivalence=29, expected.labels_weak_trace_equivalence=7;
     420           1 :   expected.states_determinisation=40, expected.transitions_determinisation=63, expected.labels_determinisation=7;
     421           1 :   expected.is_deterministic=false;
     422             : 
     423           1 :   reduce_lts_in_various_ways("Peterson protocol", PETERSON_AUT, expected);
     424           1 : }
     425             : 
     426           1 : static void test_reachability()
     427             : {
     428             :   std::string REACH =
     429             :     "des (0,4,5)       \n"
     430             :     "(0,\"reachable\",1)\n"
     431             :     "(1,\"reachable1\",2)\n"
     432             :     "(1,\"reachable2\",3)\n"
     433           2 :     "(4,\"unreachable\",0)\n"
     434             :     ;
     435             : 
     436           1 :   std::size_t expected_label_count = 5;
     437           1 :   std::size_t expected_state_count = 5;
     438           1 :   std::size_t expected_transition_count = 4;
     439             : 
     440           2 :   std::istringstream is(REACH);
     441           2 :   lts::lts_aut_t l_reach;
     442           1 :   l_reach.load(is);
     443           1 :   test_lts("reach test",l_reach, expected_label_count, expected_state_count, expected_transition_count);
     444           1 :   BOOST_CHECK(!reachability_check(l_reach,false));
     445           1 :   reachability_check(l_reach,true);
     446           1 :   test_lts("reach test after reachability reduction",l_reach, expected_label_count-1, expected_state_count-1, expected_transition_count-1);
     447           1 :   BOOST_CHECK(reachability_check(l_reach,false));
     448           1 : }
     449             : 
     450             : // The example below caused failures in the GW mlogn branching bisimulation
     451             : // algorithm when cleaning the code up.
     452           1 : static void failing_test_groote_wijs_algorithm()
     453             : {
     454             :   std::string GWLTS =
     455             :     "des(0,29,10)\n"
     456             :     "(0,\"a\",5)\n"
     457             :     "(1,\"a\",3)\n"
     458             :     "(2,\"a\",6)\n"
     459             :     "(3,\"a\",8)\n"
     460             :     "(4,\"a\",5)\n"
     461             :     "(5,\"a\",6)\n"
     462             :     "(6,\"a\",4)\n"
     463             :     "(7,\"a\",8)\n"
     464             :     "(8,\"a\",9)\n"
     465             :     "(9,\"a\",6)\n"
     466             :     "(0,\"b\",9)\n"
     467             :     "(1,\"b\",3)\n"
     468             :     "(2,\"b\",3)\n"
     469             :     "(3,\"b\",7)\n"
     470             :     "(4,\"b\",9)\n"
     471             :     "(5,\"b\",8)\n"
     472             :     "(6,\"b\",5)\n"
     473             :     "(7,\"b\",9)\n"
     474             :     "(8,\"b\",1)\n"
     475             :     "(9,\"b\",6)\n"
     476             :     "(6,\"c\",7)\n"
     477             :     "(8,\"c\",9)\n"
     478             :     "(2,\"d\",7)\n"
     479             :     "(3,\"d\",2)\n"
     480             :     "(5,\"d\",6)\n"
     481             :     "(7,\"d\",4)\n"
     482             :     "(8,\"tau\",0)\n"
     483             :     "(4,\"tau\",1)\n"
     484           2 :     "(3,\"tau\",7)\n"
     485             :     ;
     486             : 
     487           1 :   std::size_t expected_label_count = 5;
     488           1 :   std::size_t expected_state_count = 10;
     489           1 :   std::size_t expected_transition_count = 29;
     490             : 
     491           2 :   std::istringstream is(GWLTS);
     492           2 :   lts::lts_aut_t l_gw;
     493           1 :   l_gw.load(is);
     494           2 :   lts::lts_aut_t l=l_gw;
     495           1 :   reduce(l,lts::lts_eq_branching_bisim);
     496           1 :   test_lts("gw problem (branching bisimulation [Jansen/Groote/Keiren/Wijs 2019])",l,expected_label_count, expected_state_count, expected_transition_count);
     497           1 :   l=l_gw;
     498           1 :   reduce(l,lts::lts_eq_branching_bisim_gv);
     499           1 :   test_lts("gw problem (branching bisimulation [Groote/Vaandrager 1990])",l,expected_label_count, expected_state_count, expected_transition_count);
     500           1 :   l=l_gw;
     501           1 :   reduce(l,lts::lts_eq_branching_bisim_gjkw);
     502           1 :   test_lts("gw problem (branching bisimulation [Groote/Jansen/Keiren/Wijs 2017])",l,expected_label_count, expected_state_count, expected_transition_count);
     503           1 :   l=l_gw;
     504           1 :   reduce(l,lts::lts_eq_branching_bisim_sigref);
     505           1 :   test_lts("gw problem (branching bisimulation signature [Blom/Orzan 2003])",l,expected_label_count, expected_state_count, expected_transition_count);
     506           1 : }
     507             : 
     508             : // The following counterexample was taken from
     509             : // Jansen/Keiren: Stuttering equivalence is too slow! Eprint arXiv: 1603.05789,
     510             : // 2016. http://arxiv.org/abs/1603.05789
     511             : // It has not been implemented fully. The problem is that it is difficult to
     512             : // prescribe the order in which refinements have to be done.
     513             : 
     514           1 : static void counterexample_jk_1(std::size_t k)
     515             : {
     516             :     // numbering scheme of states:
     517             :     // states 0..k-1 are the blue squares
     518             :     // state k is the orange circle
     519             :     // states k+1..2k are the red triangles
     520             :     // states 2k+1 and 2k+2 are the grey pentagons
     521             :     // The grey diamonds are inserted as extra Kripke states.
     522             : 
     523           1 :     assert(1 < k);
     524           2 :     std::string CJK1 = "des(0," + std::to_string(5*k+2) + "," + std::to_string(2*k+3) + ")\n";
     525             : 
     526           4 :     for (std::size_t i = 0; i < k; ++i)
     527             :     {
     528           9 :         CJK1 += "(" + std::to_string(k) + ",a" + std::to_string(i) + "," + std::to_string(k) + ")\n"
     529          12 :                 "(" + std::to_string(k) + ",tau," + std::to_string(i) + ")\n"
     530          12 :                 "(0,a" + std::to_string(i) + "," + std::to_string(k) + ")\n";
     531             :     }
     532           3 :     for (std::size_t i = k-1; i > 0; --i)
     533             :     {
     534           6 :         CJK1 += "(" + std::to_string(i) + ",tau," + std::to_string(i-1) + ")\n"
     535           8 :                 "(" + std::to_string(i+k+1) + ",tau," + std::to_string(i+k) + ")\n";
     536             :     }
     537           3 :     CJK1 += "(" + std::to_string(k+1) + ",tau," + std::to_string(k) + ")\n"
     538           4 :             "(" + std::to_string(2*k+1) + ",a," + std::to_string(2*k+2) + ")\n"
     539           4 :             "(" + std::to_string(k) + ",tau," + std::to_string(2*k+1) + ")\n"
     540           4 :             "(0,tau," + std::to_string(2*k+2) + ")\n";
     541             : 
     542           1 :     std::size_t expected_label_count = k+2;
     543           1 :     std::size_t expected_state_count = 4;
     544           1 :     std::size_t expected_transition_count = 10;
     545             : 
     546           2 :     std::istringstream is(CJK1);
     547           2 :     lts::lts_aut_t l_cjk1;
     548           1 :     l_cjk1.load(is);
     549           2 :     lts::lts_aut_t l=l_cjk1;
     550           1 :     reduce(l,lts::lts_eq_branching_bisim);
     551           1 :     test_lts("counterexample JK 1 (branching bisimulation [Groote/Jansen/Keiren/Wijs 2017])",l,expected_label_count, expected_state_count, expected_transition_count);
     552           1 :     l=l_cjk1;
     553           1 :     reduce(l,lts::lts_eq_branching_bisim_gv);
     554           1 :     test_lts("counterexample JK 1 (branching bisimulation [Groote/Vaandrager 1990])",l,expected_label_count, expected_state_count, expected_transition_count);
     555           1 : }
     556             : 
     557             : 
     558             : // The following LTS is a counterexample to the algorithm to postprocess new
     559             : // bottom states.  Found the error in November 2016.
     560             : // The central part of the model consists of states 0--3.  The algorithm will
     561             : // split w. r. t. the constellation for "a"-labelled transitions.  This makes
     562             : // state 1 blue and the other states red.  Also, state 2 will become a new
     563             : // bottom state.  After that, it should split for "b"-labelled transitions, so
     564             : // that state 3 will get into a separate block;  however, it will not find this
     565             : // label.
     566             : 
     567             : // If the algorithm later splits w. r. t. "b", then the final result would
     568             : // still be correct.  The model is therefore sensitive to the order in which
     569             : // transitions appear.  To remove this sensitivity, I added copies of the
     570             : // states for other permutations.
     571             : 
     572             : // In the meantime, the bug is corrected:  this is why the first part of the
     573             : // algorithm now follows a much simpler line than previously.
     574           1 : static void counterexample_postprocessing()
     575             : {
     576             :   std::string POSTPROCESS_AUT =
     577             :     "des(0,33,13)\n"
     578             :     "(0,\"a\",0)\n"
     579             :     "(0,\"b\",0)\n"
     580             :     "(0,\"c\",0)\n"
     581             : 
     582             :     "(1,\"b\",0)\n"
     583             :     "(1,\"c\",0)\n"
     584             :     "(2,\"tau\",1)\n"
     585             :     "(2,\"a\",0)\n"
     586             :     "(3,\"tau\",2)\n"
     587             :     "(3,\"a\",0)\n"
     588             :     "(3,\"b\",0)\n"
     589             :     "(4,\"tau\",2)\n" // state 3 copied, with b and c swapped
     590             :     "(4,\"a\",0)\n"
     591             :     "(4,\"c\",0)\n"
     592             : 
     593             :     "(5,\"a\",0)\n" // states 1-4 copied, with a and b swapped
     594             :     "(5,\"c\",0)\n"
     595             :     "(6,\"tau\",5)\n"
     596             :     "(6,\"b\",0)\n"
     597             :     "(7,\"tau\",6)\n"
     598             :     "(7,\"a\",0)\n"
     599             :     "(7,\"b\",0)\n"
     600             :     "(8,\"tau\",6)\n"
     601             :     "(8,\"b\",0)\n"
     602             :     "(8,\"c\",0)\n"
     603             : 
     604             :     "(9,\"a\",0)\n" // states 1-4 copied, with a and c swapped
     605             :     "(9,\"b\",0)\n"
     606             :     "(10,\"tau\",9)\n"
     607             :     "(10,\"c\",0)\n"
     608             :     "(11,\"tau\",10)\n"
     609             :     "(11,\"b\",0)\n"
     610             :     "(11,\"c\",0)\n"
     611             :     "(12,\"tau\",10)\n"
     612             :     "(12,\"a\",0)\n"
     613           2 :     "(12,\"c\",0)\n"
     614             :     ;
     615             : 
     616           1 :   std::size_t expected_label_count = 4;
     617           1 :   std::size_t expected_state_count = 13;
     618           1 :   std::size_t expected_transition_count = 33;
     619             : 
     620           2 :   std::istringstream is(POSTPROCESS_AUT);
     621           2 :   lts::lts_aut_t l_gw;
     622           1 :   l_gw.load(is);
     623           2 :   lts::lts_aut_t l=l_gw;
     624           1 :   reduce(l,lts::lts_eq_branching_bisim);
     625           1 :   test_lts("postprocessing problem (branching bisimulation [Jansen/Groote/Keiren/Wijs 2019])",l,expected_label_count, expected_state_count, expected_transition_count);
     626           1 :   l=l_gw;
     627           1 :   reduce(l,lts::lts_eq_branching_bisim_gv);
     628           1 :   test_lts("postprocessing problem (branching bisimulation [Groote/Vaandrager 1990])",l,expected_label_count, expected_state_count, expected_transition_count);
     629           1 :   l=l_gw;
     630           1 :   reduce(l,lts::lts_eq_branching_bisim_gjkw);
     631           1 :   test_lts("postprocessing problem (branching bisimulation [Groote/Jansen/Keiren/Wijs 2017])",l,expected_label_count, expected_state_count, expected_transition_count);
     632           1 :   l=l_gw;
     633           1 :   reduce(l,lts::lts_eq_branching_bisim_sigref);
     634           1 :   test_lts("postprocessing problem (branching bisimulation signature [Blom/Orzan 2003])",l,expected_label_count, expected_state_count, expected_transition_count);
     635           1 : }
     636             : 
     637           1 : static void regression_delete_old_bb_slice()
     638             : {
     639             :   std::string POSTPROCESS_AUT =
     640             :     "des(0,163,100)\n"
     641             :     "(33,\"a\",79)\n"
     642             :     "(87,\"a\",2)\n"
     643             :     "(4,\"b\",35)\n"
     644             :     "(13,\"b\",10)\n"
     645             :     "(15,\"b\",32)\n"
     646             :     "(31,\"b\",3)\n"
     647             :     "(35,\"b\",86)\n"
     648             :     "(47,\"b\",73)\n"
     649             :     "(61,\"b\",10)\n"
     650             :     "(67,\"b\",59)\n"
     651             :     "(81,\"b\",38)\n"
     652             :     "(89,\"b\",77)\n"
     653             :     "(94,\"b\",34)\n"
     654             :     "(20,\"tau\",10)\n"
     655             :     "(65,\"tau\",61)\n"
     656             :     "(38,\"tau\",64)\n"
     657             :     "(86,\"tau\",41)\n"
     658             :     "(18,\"tau\",55)\n"
     659             :     "(50,\"tau\",65)\n"
     660             :     "(28,\"tau\",50)\n"
     661             :     "(29,\"tau\",55)\n"
     662             :     "(43,\"tau\",85)\n"
     663             :     "(93,\"tau\",8)\n"
     664             :     "(54,\"tau\",72)\n"
     665             :     "(52,\"tau\",47)\n"
     666             :     "(7,\"tau\",36)\n"
     667             :     "(6,\"tau\",60)\n"
     668             :     "(48,\"tau\",43)\n"
     669             :     "(77,\"tau\",68)\n"
     670             :     "(90,\"tau\",34)\n"
     671             :     "(18,\"tau\",21)\n"
     672             :     "(18,\"tau\",56)\n"
     673             :     "(36,\"tau\",70)\n"
     674             :     "(54,\"tau\",28)\n"
     675             :     "(62,\"tau\",40)\n"
     676             :     "(5,\"tau\",18)\n"
     677             :     "(91,\"tau\",47)\n"
     678             :     "(42,\"tau\",27)\n"
     679             :     "(34,\"tau\",70)\n"
     680             :     "(23,\"tau\",63)\n"
     681             :     "(19,\"tau\",70)\n"
     682             :     "(39,\"tau\",43)\n"
     683             :     "(86,\"tau\",34)\n"
     684             :     "(25,\"tau\",73)\n"
     685             :     "(16,\"tau\",4)\n"
     686             :     "(34,\"tau\",30)\n"
     687             :     "(70,\"tau\",20)\n"
     688             :     "(30,\"tau\",22)\n"
     689             :     "(51,\"tau\",97)\n"
     690             :     "(5,\"tau\",67)\n"
     691             :     "(80,\"tau\",13)\n"
     692             :     "(66,\"tau\",59)\n"
     693             :     "(24,\"tau\",23)\n"
     694             :     "(95,\"tau\",82)\n"
     695             :     "(5,\"tau\",2)\n"
     696             :     "(82,\"tau\",9)\n"
     697             :     "(40,\"tau\",46)\n"
     698             :     "(94,\"tau\",31)\n"
     699             :     "(19,\"tau\",96)\n"
     700             :     "(34,\"tau\",32)\n"
     701             :     "(62,\"tau\",24)\n"
     702             :     "(74,\"tau\",8)\n"
     703             :     "(9,\"tau\",76)\n"
     704             :     "(98,\"tau\",50)\n"
     705             :     "(25,\"tau\",62)\n"
     706             :     "(89,\"tau\",95)\n"
     707             :     "(1,\"tau\",56)\n"
     708             :     "(44,\"tau\",66)\n"
     709             :     "(1,\"tau\",45)\n"
     710             :     "(73,\"tau\",60)\n"
     711             :     "(70,\"tau\",98)\n"
     712             :     "(36,\"tau\",14)\n"
     713             :     "(18,\"tau\",27)\n"
     714             :     "(87,\"tau\",27)\n"
     715             :     "(65,\"tau\",17)\n"
     716             :     "(57,\"tau\",97)\n"
     717             :     "(98,\"tau\",8)\n"
     718             :     "(29,\"tau\",25)\n"
     719             :     "(59,\"tau\",97)\n"
     720             :     "(1,\"tau\",94)\n"
     721             :     "(30,\"tau\",74)\n"
     722             :     "(53,\"tau\",90)\n"
     723             :     "(50,\"tau\",19)\n"
     724             :     "(41,\"tau\",81)\n"
     725             :     "(73,\"tau\",97)\n"
     726             :     "(97,\"tau\",62)\n"
     727             :     "(40,\"tau\",59)\n"
     728             :     "(33,\"tau\",86)\n"
     729             :     "(16,\"tau\",47)\n"
     730             :     "(50,\"tau\",72)\n"
     731             :     "(90,\"tau\",68)\n"
     732             :     "(90,\"tau\",63)\n"
     733             :     "(17,\"tau\",75)\n"
     734             :     "(70,\"tau\",49)\n"
     735             :     "(85,\"tau\",33)\n"
     736             :     "(25,\"tau\",52)\n"
     737             :     "(63,\"tau\",99)\n"
     738             :     "(22,\"tau\",29)\n"
     739             :     "(47,\"tau\",31)\n"
     740             :     "(39,\"tau\",88)\n"
     741             :     "(41,\"tau\",88)\n"
     742             :     "(49,\"tau\",83)\n"
     743             :     "(60,\"tau\",34)\n"
     744             :     "(85,\"tau\",59)\n"
     745             :     "(12,\"tau\",6)\n"
     746             :     "(47,\"tau\",99)\n"
     747             :     "(47,\"tau\",23)\n"
     748             :     "(77,\"tau\",73)\n"
     749             :     "(78,\"tau\",55)\n"
     750             :     "(7,\"tau\",6)\n"
     751             :     "(0,\"tau\",67)\n"
     752             :     "(66,\"tau\",12)\n"
     753             :     "(75,\"tau\",31)\n"
     754             :     "(25,\"tau\",80)\n"
     755             :     "(53,\"tau\",35)\n"
     756             :     "(83,\"tau\",79)\n"
     757             :     "(74,\"tau\",88)\n"
     758             :     "(57,\"tau\",80)\n"
     759             :     "(7,\"tau\",77)\n"
     760             :     "(77,\"tau\",8)\n"
     761             :     "(87,\"tau\",1)\n"
     762             :     "(59,\"tau\",54)\n"
     763             :     "(66,\"tau\",33)\n"
     764             :     "(86,\"tau\",80)\n"
     765             :     "(90,\"tau\",30)\n"
     766             :     "(1,\"tau\",4)\n"
     767             :     "(47,\"tau\",78)\n"
     768             :     "(75,\"tau\",47)\n"
     769             :     "(26,\"tau\",7)\n"
     770             :     "(6,\"tau\",93)\n"
     771             :     "(51,\"tau\",14)\n"
     772             :     "(7,\"tau\",77)\n"
     773             :     "(13,\"tau\",67)\n"
     774             :     "(65,\"tau\",77)\n"
     775             :     "(41,\"tau\",39)\n"
     776             :     "(91,\"tau\",96)\n"
     777             :     "(69,\"tau\",38)\n"
     778             :     "(71,\"tau\",77)\n"
     779             :     "(81,\"tau\",56)\n"
     780             :     "(53,\"tau\",44)\n"
     781             :     "(50,\"tau\",88)\n"
     782             :     "(65,\"tau\",4)\n"
     783             :     "(39,\"tau\",49)\n"
     784             :     "(82,\"tau\",93)\n"
     785             :     "(20,\"tau\",13)\n"
     786             :     "(4,\"tau\",49)\n"
     787             :     "(16,\"tau\",6)\n"
     788             :     "(42,\"tau\",9)\n"
     789             :     "(74,\"tau\",3)\n"
     790             :     "(17,\"tau\",21)\n"
     791             :     "(7,\"tau\",80)\n"
     792             :     "(58,\"tau\",84)\n"
     793             :     "(74,\"tau\",62)\n"
     794             :     "(81,\"tau\",58)\n"
     795             :     "(19,\"tau\",87)\n"
     796             :     "(42,\"tau\",45)\n"
     797             :     "(26,\"tau\",30)\n"
     798             :     "(57,\"tau\",87)\n"
     799             :     "(57,\"tau\",96)\n"
     800             :     "(34,\"tau\",32)\n"
     801             :     "(43,\"tau\",11)\n"
     802             :     "(53,\"tau\",35)\n"
     803           2 :     "(30,\"tau\",56)\n"
     804             :     ;
     805             : 
     806           1 :   std::size_t expected_label_count = 3;
     807           1 :   std::size_t expected_state_count = 17;
     808           1 :   std::size_t expected_transition_count = 43;
     809             : 
     810           2 :   std::istringstream is(POSTPROCESS_AUT);
     811           2 :   lts::lts_aut_t l_gw;
     812           1 :   l_gw.load(is);
     813           2 :   lts::lts_aut_t l=l_gw;
     814           1 :   reduce(l,lts::lts_eq_divergence_preserving_branching_bisim);
     815           1 :   test_lts("regression test for GJKW bug (branching bisimulation [Jansen/Groote/Keiren/Wijs 2019])",l,expected_label_count, expected_state_count, expected_transition_count);
     816           1 :   l=l_gw;
     817           1 :   reduce(l,lts::lts_eq_divergence_preserving_branching_bisim_gv);
     818           1 :   test_lts("regression test for GJKW bug (branching bisimulation [Groote/Vaandrager 1990])",l,expected_label_count, expected_state_count, expected_transition_count);
     819           1 :   l=l_gw;
     820           1 :   reduce(l,lts::lts_eq_divergence_preserving_branching_bisim_gjkw);
     821           1 :   test_lts("regression test for GJKW bug (branching bisimulation [Groote/Jansen/Keiren/Wijs 2017])",l,expected_label_count, expected_state_count, expected_transition_count);
     822           1 :   l=l_gw;
     823           1 :   reduce(l,lts::lts_eq_divergence_preserving_branching_bisim_sigref);
     824           1 :   test_lts("regression test for GJKW bug (branching bisimulation signature [Blom/Orzan 2003])",l,expected_label_count, expected_state_count, expected_transition_count);
     825           1 : }
     826             : 
     827           1 : void is_deterministic_test1()
     828             : {
     829             :   std::string automaton =
     830             :     "des(0,2,2)\n"
     831             :     "(0,\"a\",1)\n"
     832           2 :     "(0,\"a\",1)\n";
     833             : 
     834           2 :   std::istringstream is(automaton);
     835           2 :   lts::lts_aut_t l_det;
     836           1 :   l_det.load(is);
     837           1 :   BOOST_CHECK(is_deterministic(l_det));
     838           1 : }
     839             : 
     840           1 : void is_deterministic_test2()
     841             : {
     842             :   std::string automaton =
     843             :     "des(0,2,2)\n"
     844             :     "(0,\"a\",1)\n"
     845           2 :     "(0,\"a\",0)\n";
     846             : 
     847           2 :   std::istringstream is(automaton);
     848           2 :   lts::lts_aut_t l_det;
     849           1 :   l_det.load(is);
     850           1 :   BOOST_CHECK(!is_deterministic(l_det));
     851           1 : }
     852             : 
     853           1 : void test_is_deterministic()
     854             : {
     855           1 :   is_deterministic_test1();
     856           1 :   is_deterministic_test2();
     857           1 : }
     858             : 
     859           3 : BOOST_AUTO_TEST_CASE(test_main)
     860             : {
     861           1 :   reduce_simple_loop();
     862           1 :   reduce_simple_loop_with_tau();
     863           1 :   tricky_example_for_branching_bisimulation();
     864           1 :   reduce_abp();
     865           1 :   reduce_peterson();
     866           1 :   test_reachability();
     867           1 :   test_is_deterministic();
     868           1 :   failing_test_groote_wijs_algorithm();
     869           1 :   counterexample_jk_1(3);
     870           1 :   counterexample_postprocessing();
     871           1 :   regression_delete_old_bb_slice();
     872             :   // TODO: Add groote wijs branching bisimulation and add weak bisimulation tests. For the last Peterson is a good candidate.
     873           4 : }

Generated by: LCOV version 1.13