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

          Line data    Source code
       1             : // Author(s): Jan Friso Groote
       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 ltsconvert_test.cpp
      10             : /// \brief This file contains tests to see whether ltsconvert
      11             : //         reduces problems well.
      12             : 
      13             : #define BOOST_TEST_MODULE ltsconvert_test
      14             : // #include <iostream>
      15             : 
      16             : #include <boost/test/included/unit_test_framework.hpp>
      17             : 
      18             : #include "mcrl2/lts/lts_algorithm.h"
      19             : 
      20             : using namespace mcrl2::lts;
      21             : 
      22         163 : static lts_aut_t parse_aut(const std::string& s)
      23             : {
      24         326 :   std::stringstream is(s);
      25         163 :   lts_aut_t l;
      26         163 :   l.load(is);
      27         326 :   return l;
      28             : }
      29             : 
      30           1 : const std::string test1=
      31             :   "des (0,2,2)\n"
      32             :   "(0,\"move_to_ERROR\",1)\n"
      33             :   "(1,\"move_to_ERROR\",0)\n";
      34             : 
      35           1 : const std::string test2=
      36             :   "des (0,2,2)\n"
      37             :   "(0,\"move_to_ERROR\",1)\n"
      38             :   "(1,\"move_to_ERROR1\",0)\n";
      39             : 
      40           1 : const std::string test3=
      41             :   "des (0,3,2)\n"
      42             :   "(0,\"tau\",1)\n"
      43             :   "(1,\"tau\",0)\n"
      44             :   "(0,\"a\",1)\n";
      45             : 
      46             : // Example below represents a(tau(b+c)+b) which can be reduced to a(b+c).
      47           1 : const std::string test4=
      48             :   "des (0,5,6)\n"
      49             :   "(0,\"a\",1)\n"
      50             :   "(1,\"tau\",2)\n"
      51             :   "(2,\"b\",3)\n"
      52             :   "(2,\"c\",4)\n"
      53             :   "(1,\"b\",5)\n";
      54             : 
      55             : // Example below is inspired by the rhs of Milner's third tau law, a(tau.b+c)=a(tau.b+c)+a.b
      56             : // which contains a non inert tau.
      57           1 : const std::string test5=
      58             :   "des (0,6,7)\n"
      59             :   "(0,\"a\",1)\n"
      60             :   "(0,\"a\",2)\n"
      61             :   "(1,\"tau\",3)\n"
      62             :   "(1,\"c\",4)\n"
      63             :   "(3,\"b\",5)\n"
      64             :   "(2,\"b\",6)\n";
      65             : 
      66             : // Example below is inspired by Milner's third tau law, a(tau.b+c)=a(tau.b+c)+a.b.
      67             : // The states 1 and 2 should be identified in weak bisimulation, but not in branching
      68             : // bisimulation.
      69           1 : const std::string test5a=
      70             :   "des (0,10,7)\n"
      71             :   "(0,\"d\",1)\n"
      72             :   "(0,\"d\",2)\n"
      73             :   "(1,\"a\",3)\n"
      74             :   "(2,\"a\",4)\n"
      75             :   "(2,\"a\",5)\n"
      76             :   "(3,\"b\",6)\n"
      77             :   "(3,\"tau\",4)\n"
      78             :   "(4,\"c\",6)\n"
      79             :   "(5,\"b\",6)\n"
      80             :   "(5,\"tau\",4)\n";
      81             : 
      82             : 
      83             : // In the term a.Y with Y=tau.Y divergence-preserving bisimulation must not remove the tau.
      84           1 : const std::string test6=
      85             :   "des (0,2,2)\n"
      86             :   "(0,\"a\",1)\n"
      87             :   "(1,\"tau\",1)\n";
      88             : 
      89             : // Test whether a mixed up sequence of tau's is properly dealt with.
      90             : // Example is essentially: tau.X where X=tau.tau.tau.tau.tau.a.X.
      91           1 : const std::string test7=
      92             :   "des (0,7,7)\n"
      93             :   "(0,\"tau\",4)\n"
      94             :   "(2,\"tau\",1)\n"
      95             :   "(3,\"tau\",2)\n"
      96             :   "(4,\"tau\",3)\n"
      97             :   "(1,\"tau\",5)\n"
      98             :   "(5,\"tau\",6)\n"
      99             :   "(6,\"a\",3)\n";
     100             : 
     101             : // Test whether a mixed up sequence of tau's is properly dealt with.
     102             : // Example is essentially: tau.X where X=tau.tau.tau.tau.tau.a.X.
     103           1 : const std::string test8=
     104             :   "des (0,6,5)\n"
     105             :   "(0,\"tau\",1)\n"
     106             :   "(0,\"tau\",2)\n"
     107             :   "(0,\"tau\",3)\n"
     108             :   "(0,\"tau\",4)\n"
     109             :   "(3,\"tau\",3)\n"
     110             :   "(4,\"tau\",4)\n";
     111             : 
     112             : // Test whether a tau-loop at the end of a process is correctly dealt with.
     113           1 : const std::string test9=
     114             :   "des (0,4,4)\n"
     115             :   "(0,\"a\",1)\n"
     116             :   "(1,\"tau\",2)\n"
     117             :   "(2,\"tau\",3)\n"
     118             :   "(3,\"tau\",1)\n";
     119             : 
     120             : // Test whether a tau that does become non inert will act to split blocks.
     121           1 : const std::string test10=
     122             :   "des (0,7,8)\n"
     123             :   "(0,\"b\",1)\n"
     124             :   "(0,\"b\",2)\n"
     125             :   "(1,\"a\",3)\n"
     126             :   "(1,\"tau\",4)\n"
     127             :   "(2,\"a\",5)\n"
     128             :   "(2,\"tau\",6)\n"
     129             :   "(6,\"a\",7)\n";
     130             : 
     131             : // Test whether tau's can repeatedly become non inert
     132           1 : const std::string test11=
     133             :   "des (0,5,5)\n"
     134             :   "(0,\"tau\",1)\n"
     135             :   "(0,\"tau\",3)\n"
     136             :   "(1,\"a\",2)\n"
     137             :   "(1,\"tau\",3)\n"
     138             :   "(3,\"tau\",4)\n";
     139             : 
     140             : // The test below caused the tau_star reduction to go astray, as there
     141             : // were problems with the reachability check.
     142           1 : const std::string test12=
     143             :   "des (0,7,6)\n"
     144             :   "(0,\"tau\",1)\n"
     145             :   "(0,\"tau\",2)\n"
     146             :   "(1,\"tau\",3)\n"
     147             :   "(2,\"tau\",4)\n"
     148             :   "(2,\"a\",5)\n"
     149             :   "(3,\"c\",5)\n"
     150             :   "(4,\"b\",5)\n";
     151             : 
     152             : // Test whether subtle tau loops are handled properly in divergence-preserving weak and branching bisimulation.
     153           1 : const std::string test13=
     154             :   "des (0,4,4)\n"
     155             :   "(0,\"tau\",1)\n"
     156             :   "(1,\"tau\",2)\n"
     157             :   "(2,\"tau\",2)\n"
     158             :   "(1,\"a\",3)\n";
     159             : 
     160             : 
     161             : 
     162           3 : BOOST_AUTO_TEST_CASE(test_state_space_reductions)
     163             : {
     164             :  {
     165           1 :   std::cerr << "Test1\n";
     166           2 :   lts_aut_t t1=parse_aut(test1);
     167           1 :   reduce(t1,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     168           1 :   BOOST_CHECK(t1.num_states()==1 && t1.num_transitions()==1);
     169           1 :   t1 = parse_aut(test1);
     170           1 :   reduce(t1,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
     171           1 :   BOOST_CHECK(t1.num_states()==1 && t1.num_transitions()==1);
     172           1 :   t1 = parse_aut(test1);
     173           1 :   reduce(t1,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
     174           1 :   BOOST_CHECK(t1.num_states()==1 && t1.num_transitions()==1);
     175           1 :   t1 = parse_aut(test1);
     176           1 :   reduce(t1,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
     177           1 :   BOOST_CHECK(t1.num_states()==1 && t1.num_transitions()==1);
     178             :  }
     179             :  {
     180           1 :   std::cerr << "Test2\n";
     181           2 :   lts_aut_t t2=parse_aut(test2);
     182           1 :   reduce(t2,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     183           1 :   BOOST_CHECK(t2.num_states()==2 && t2.num_transitions()==2);
     184           1 :   t2 = parse_aut(test2);
     185           1 :   reduce(t2,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
     186           1 :   BOOST_CHECK(t2.num_states()==2 && t2.num_transitions()==2);
     187           1 :   t2 = parse_aut(test2);
     188           1 :   reduce(t2,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
     189           1 :   BOOST_CHECK(t2.num_states()==2 && t2.num_transitions()==2);
     190           1 :   t2 = parse_aut(test2);
     191           1 :   reduce(t2,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
     192           1 :   BOOST_CHECK(t2.num_states()==2 && t2.num_transitions()==2);
     193             :  }
     194             :  {
     195           1 :   std::cerr << "Test3\n";
     196           2 :   lts_aut_t t3=parse_aut(test3);
     197           1 :   reduce(t3,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     198           1 :   BOOST_CHECK(t3.num_states()==2 && t3.num_transitions()==3);
     199           1 :   t3=parse_aut(test3);
     200           1 :   reduce(t3,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
     201           1 :   BOOST_CHECK(t3.num_states()==2 && t3.num_transitions()==3);
     202           1 :   t3=parse_aut(test3);
     203           1 :   reduce(t3,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
     204           1 :   BOOST_CHECK(t3.num_states()==2 && t3.num_transitions()==3);
     205           1 :   t3=parse_aut(test3);
     206           1 :   reduce(t3,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
     207           1 :   BOOST_CHECK(t3.num_states()==2 && t3.num_transitions()==3);
     208           1 :   t3=parse_aut(test3);
     209           1 :   reduce(t3,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     210           1 :   BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==1);
     211           1 :   t3=parse_aut(test3);
     212           1 :   reduce(t3,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
     213           1 :   BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==1);
     214           1 :   t3=parse_aut(test3);
     215           1 :   reduce(t3,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
     216           1 :   BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==1);
     217           1 :   t3=parse_aut(test3);
     218           1 :   reduce(t3,lts_eq_branching_bisim_sigref); //Branching bisimulation reduction sigref [Blom/Orzan 2003]
     219           1 :   BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==1);
     220           1 :   t3=parse_aut(test3);
     221           1 :   reduce(t3,lts_eq_weak_bisim); //Weak bisimulation reduction
     222           1 :   BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==1);
     223             : 
     224             :   //Divergence-preserving branching bisimulation reduction
     225           1 :   t3=parse_aut(test3);
     226           1 :   reduce(t3,lts_eq_divergence_preserving_branching_bisim_gjkw);
     227           1 :   BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==2);
     228           1 :   t3=parse_aut(test3);
     229           1 :   reduce(t3,lts_eq_divergence_preserving_branching_bisim_gv);
     230           1 :   BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==2);
     231           1 :   t3=parse_aut(test3);
     232           1 :   reduce(t3,lts_eq_divergence_preserving_branching_bisim);
     233           1 :   BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==2);
     234           1 :   t3=parse_aut(test3);
     235           1 :   reduce(t3,lts_eq_divergence_preserving_branching_bisim_sigref);
     236           1 :   BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==2);
     237           1 :   t3=parse_aut(test3);
     238           1 :   reduce(t3,lts_eq_divergence_preserving_weak_bisim);
     239           1 :   BOOST_CHECK(t3.num_states()==1 && t3.num_transitions()==2);
     240             :  }
     241             :  {
     242           1 :   std::cerr << "Test4\n";
     243           2 :   lts_aut_t t4=parse_aut(test4);
     244           1 :   reduce(t4,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     245           1 :   BOOST_CHECK(t4.num_states()==4 && t4.num_transitions()==5);
     246           1 :   t4=parse_aut(test4);
     247           1 :   reduce(t4,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
     248           1 :   BOOST_CHECK(t4.num_states()==4 && t4.num_transitions()==5);
     249           1 :   t4=parse_aut(test4);
     250           1 :   reduce(t4,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
     251           1 :   BOOST_CHECK(t4.num_states()==4 && t4.num_transitions()==5);
     252           1 :   t4=parse_aut(test4);
     253           1 :   reduce(t4,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
     254           1 :   BOOST_CHECK(t4.num_states()==4 && t4.num_transitions()==5);
     255           1 :   t4=parse_aut(test4);
     256           1 :   reduce(t4,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     257           1 :   BOOST_CHECK(t4.num_states()==3 && t4.num_transitions()==3);
     258           1 :   t4=parse_aut(test4);
     259           1 :   reduce(t4,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
     260           1 :   BOOST_CHECK(t4.num_states()==3 && t4.num_transitions()==3);
     261           1 :   t4=parse_aut(test4);
     262           1 :   reduce(t4,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
     263           1 :   BOOST_CHECK(t4.num_states()==3 && t4.num_transitions()==3);
     264           1 :   t4=parse_aut(test4);
     265           1 :   reduce(t4,lts_eq_branching_bisim_sigref);
     266           1 :   BOOST_CHECK(t4.num_states()==3 && t4.num_transitions()==3);
     267           1 :   t4=parse_aut(test4);
     268           1 :   reduce(t4,lts_eq_weak_bisim); //Weak bisimulation reduction
     269           1 :   BOOST_CHECK(t4.num_states()==3 && t4.num_transitions()==3);
     270             :  }
     271             :  {
     272           1 :   std::cerr << "Test5\n";
     273           2 :   lts_aut_t t5=parse_aut(test5);
     274           1 :   reduce(t5,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     275           1 :   BOOST_CHECK(t5.num_states()==4 && t5.num_transitions()==5);
     276           1 :   t5=parse_aut(test5);
     277           1 :   reduce(t5,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
     278           1 :   BOOST_CHECK(t5.num_states()==4 && t5.num_transitions()==5);
     279           1 :   t5=parse_aut(test5);
     280           1 :   reduce(t5,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
     281           1 :   BOOST_CHECK(t5.num_states()==4 && t5.num_transitions()==5);
     282           1 :   t5=parse_aut(test5);
     283           1 :   reduce(t5,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
     284           1 :   BOOST_CHECK(t5.num_states()==4 && t5.num_transitions()==5);
     285           1 :   t5=parse_aut(test5);
     286           1 :   reduce(t5,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     287           1 :   BOOST_CHECK(t5.num_states()==4 && t5.num_transitions()==5);
     288           1 :   t5=parse_aut(test5);
     289           1 :   reduce(t5,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
     290           1 :   BOOST_CHECK(t5.num_states()==4 && t5.num_transitions()==5);
     291           1 :   t5=parse_aut(test5);
     292           1 :   reduce(t5,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
     293           1 :   BOOST_CHECK(t5.num_states()==4 && t5.num_transitions()==5);
     294           1 :   t5=parse_aut(test5);
     295           1 :   reduce(t5,lts_eq_branching_bisim_sigref);
     296           1 :   BOOST_CHECK(t5.num_states()==4 && t5.num_transitions()==5);
     297           1 :   t5=parse_aut(test5);
     298           1 :   reduce(t5,lts_eq_weak_bisim); //Weak bisimulation reduction
     299           1 :   BOOST_CHECK(t5.num_states()==4 && t5.num_transitions()==4);
     300             :  }
     301             :  {
     302           1 :   std::cerr << "Test5a\n";
     303           2 :   lts_aut_t t5a=parse_aut(test5a);
     304           1 :   reduce(t5a,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     305           1 :   BOOST_CHECK(t5a.num_states()==6 && t5a.num_transitions()==8);
     306           1 :   t5a=parse_aut(test5a);
     307           1 :   reduce(t5a,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
     308           1 :   BOOST_CHECK(t5a.num_states()==6 && t5a.num_transitions()==8);
     309           1 :   t5a=parse_aut(test5a);
     310           1 :   reduce(t5a,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
     311           1 :   BOOST_CHECK(t5a.num_states()==6 && t5a.num_transitions()==8);
     312           1 :   t5a=parse_aut(test5a);
     313           1 :   reduce(t5a,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
     314           1 :   BOOST_CHECK(t5a.num_states()==6 && t5a.num_transitions()==8);
     315           1 :   t5a=parse_aut(test5a);
     316           1 :   reduce(t5a,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     317           1 :   BOOST_CHECK(t5a.num_states()==6 && t5a.num_transitions()==8);
     318           1 :   t5a=parse_aut(test5a);
     319           1 :   reduce(t5a,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
     320           1 :   BOOST_CHECK(t5a.num_states()==6 && t5a.num_transitions()==8);
     321           1 :   t5a=parse_aut(test5a);
     322           1 :   reduce(t5a,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
     323           1 :   BOOST_CHECK(t5a.num_states()==6 && t5a.num_transitions()==8);
     324           1 :   t5a=parse_aut(test5a);
     325           1 :   reduce(t5a,lts_eq_branching_bisim_sigref); //Branching bisimulation reduction sigref
     326           1 :   BOOST_CHECK(t5a.num_states()==6 && t5a.num_transitions()==8);
     327           1 :   t5a=parse_aut(test5a);
     328           1 :   reduce(t5a,lts_eq_weak_bisim); //Weak bisimulation reduction
     329           1 :   BOOST_CHECK(t5a.num_states()==5 && t5a.num_transitions()==5);
     330             :  }
     331             :  {
     332           1 :   std::cerr << "Test6\n";
     333           2 :   lts_aut_t t6=parse_aut(test6);
     334           1 :   reduce(t6,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     335           1 :   BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==2);
     336           1 :   t6=parse_aut(test6);
     337           1 :   reduce(t6,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
     338           1 :   BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==2);
     339           1 :   t6=parse_aut(test6);
     340           1 :   reduce(t6,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
     341           1 :   BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==2);
     342           1 :   t6=parse_aut(test6);
     343           1 :   reduce(t6,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
     344           1 :   BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==2);
     345             : 
     346           1 :   std::cerr << "Test6a\n";
     347           1 :   t6=parse_aut(test6);
     348           1 :   reduce(t6,lts_eq_divergence_preserving_branching_bisim_gjkw); //Divergence-preserving branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     349           1 :   BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==2);
     350           1 :   t6=parse_aut(test6);
     351           1 :   reduce(t6,lts_eq_divergence_preserving_branching_bisim_gv); //Divergence-preserving branching bisimulation reduction [Groote/Vaandrager 1990]
     352           1 :   BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==2);
     353           1 :   t6=parse_aut(test6);
     354           1 :   reduce(t6,lts_eq_divergence_preserving_branching_bisim); //Divergence-preserving branching bisimulation reduction directly on LTS
     355           1 :   BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==2);
     356           1 :   t6=parse_aut(test6);
     357           1 :   reduce(t6,lts_eq_divergence_preserving_branching_bisim_sigref);
     358           1 :   BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==2);
     359           1 :   t6=parse_aut(test6);
     360           1 :   reduce(t6,lts_eq_divergence_preserving_weak_bisim); //Divergence-preserving weak bisimulation reduction
     361           1 :   BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==2);
     362             : 
     363           1 :   std::cerr << "Test6b\n";
     364           1 :   t6=parse_aut(test6);
     365           1 :   reduce(t6,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     366           1 :   BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==1);
     367           1 :   t6=parse_aut(test6);
     368           1 :   reduce(t6,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
     369           1 :   BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==1);
     370           1 :   t6=parse_aut(test6);
     371           1 :   reduce(t6,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
     372           1 :   BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==1);
     373           1 :   t6=parse_aut(test6);
     374           1 :   reduce(t6,lts_eq_branching_bisim_sigref);
     375           1 :   BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==1);
     376           1 :   t6=parse_aut(test6);
     377           1 :   reduce(t6,lts_eq_weak_bisim); //Weak bisimulation reduction
     378           1 :   BOOST_CHECK(t6.num_states()==2 && t6.num_transitions()==1);
     379             :  }
     380             :  {
     381           1 :   std::cerr << "Test7\n";
     382           2 :   lts_aut_t t7=parse_aut(test7);
     383           1 :   reduce(t7,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     384           1 :   BOOST_CHECK(t7.num_states()==7 && t7.num_transitions()==7);
     385           1 :   t7=parse_aut(test7);
     386           1 :   reduce(t7,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
     387           1 :   BOOST_CHECK(t7.num_states()==7 && t7.num_transitions()==7);
     388           1 :   t7=parse_aut(test7);
     389           1 :   reduce(t7,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
     390           1 :   BOOST_CHECK(t7.num_states()==7 && t7.num_transitions()==7);
     391           1 :   t7=parse_aut(test7);
     392           1 :   reduce(t7,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
     393           1 :   BOOST_CHECK(t7.num_states()==7 && t7.num_transitions()==7);
     394           1 :   t7=parse_aut(test7);
     395           1 :   reduce(t7,lts_eq_divergence_preserving_branching_bisim_gjkw); //Divergence-preserving branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     396           1 :   BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
     397           1 :   t7=parse_aut(test7);
     398           1 :   reduce(t7,lts_eq_divergence_preserving_branching_bisim_gv); //Divergence-preserving branching bisimulation reduction [Groote/Vaandrager 1990]
     399           1 :   BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
     400           1 :   t7=parse_aut(test7);
     401           1 :   reduce(t7,lts_eq_divergence_preserving_branching_bisim); //Divergence-preserving branching bisimulation reduction directly on LTS
     402           1 :   BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
     403           1 :   t7=parse_aut(test7);
     404           1 :   reduce(t7,lts_eq_divergence_preserving_branching_bisim_sigref);
     405           1 :   BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
     406           1 :   t7=parse_aut(test7);
     407           1 :   reduce(t7,lts_eq_divergence_preserving_weak_bisim); //Divergence-preserving weak bisimulation reduction
     408           1 :   BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
     409           1 :   t7=parse_aut(test7);
     410           1 :   reduce(t7,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     411           1 :   BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
     412           1 :   t7=parse_aut(test7);
     413           1 :   reduce(t7,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
     414           1 :   BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
     415           1 :   t7=parse_aut(test7);
     416           1 :   reduce(t7,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
     417           1 :   BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
     418           1 :   t7=parse_aut(test7);
     419           1 :   reduce(t7,lts_eq_branching_bisim_sigref);
     420           1 :   BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
     421           1 :   t7=parse_aut(test7);
     422           1 :   reduce(t7,lts_eq_weak_bisim); //Weak bisimulation reduction
     423           1 :   BOOST_CHECK(t7.num_states()==1 && t7.num_transitions()==1);
     424             :  }
     425             :  {
     426           1 :   std::cerr << "Test8\n";
     427           2 :   lts_aut_t t8=parse_aut(test8);
     428           1 :   reduce(t8,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     429           1 :   BOOST_CHECK(t8.num_states()==3 && t8.num_transitions()==3);
     430           1 :   t8 = parse_aut(test8);
     431           1 :   reduce(t8,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
     432           1 :   BOOST_CHECK(t8.num_states()==3 && t8.num_transitions()==3);
     433           1 :   t8 = parse_aut(test8);
     434           1 :   reduce(t8,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
     435           1 :   BOOST_CHECK(t8.num_states()==3 && t8.num_transitions()==3);
     436           1 :   t8 = parse_aut(test8);
     437           1 :   reduce(t8,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
     438           1 :   BOOST_CHECK(t8.num_states()==3 && t8.num_transitions()==3);
     439             : 
     440           1 :   std::cerr << "Test8a\n";
     441           1 :   t8=parse_aut(test8);
     442           1 :   reduce(t8,lts_eq_divergence_preserving_branching_bisim_gjkw); //Divergence-preserving branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     443           1 :   BOOST_CHECK(t8.num_states()==3 && t8.num_transitions()==3);
     444           1 :   t8=parse_aut(test8);
     445           1 :   reduce(t8,lts_eq_divergence_preserving_branching_bisim_gv); //Divergence-preserving branching bisimulation reduction [Groote/Vaandrager 1990]
     446           1 :   BOOST_CHECK(t8.num_states()==3 && t8.num_transitions()==3);
     447           1 :   t8=parse_aut(test8);
     448           1 :   reduce(t8,lts_eq_divergence_preserving_branching_bisim); //Divergence-preserving branching bisimulation reduction directly on LTS
     449           1 :   BOOST_CHECK(t8.num_states()==3 && t8.num_transitions()==3);
     450           1 :   t8=parse_aut(test8);
     451           1 :   reduce(t8,lts_eq_divergence_preserving_branching_bisim_sigref);
     452           1 :   BOOST_CHECK(t8.num_states()==3 && t8.num_transitions()==3);
     453           1 :   t8=parse_aut(test8);
     454           1 :   reduce(t8,lts_eq_divergence_preserving_weak_bisim); //Divergence-preserving weak bisimulation reduction
     455           1 :   BOOST_CHECK(t8.num_states()==3 && t8.num_transitions()==3);
     456             : 
     457           1 :   std::cerr << "Test8b\n";
     458           1 :   t8=parse_aut(test8);
     459           1 :   reduce(t8,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     460           1 :   BOOST_CHECK(t8.num_states()==1 && t8.num_transitions()==0);
     461           1 :   t8=parse_aut(test8);
     462           1 :   reduce(t8,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
     463           1 :   BOOST_CHECK(t8.num_states()==1 && t8.num_transitions()==0);
     464           1 :   t8=parse_aut(test8);
     465           1 :   reduce(t8,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
     466           1 :   BOOST_CHECK(t8.num_states()==1 && t8.num_transitions()==0);
     467           1 :   t8=parse_aut(test8);
     468           1 :   reduce(t8,lts_eq_branching_bisim_sigref);
     469           1 :   BOOST_CHECK(t8.num_states()==1 && t8.num_transitions()==0);
     470           1 :   t8=parse_aut(test8);
     471           1 :   reduce(t8,lts_eq_weak_bisim); //Weak bisimulation reduction
     472           1 :   BOOST_CHECK(t8.num_states()==1 && t8.num_transitions()==0);
     473             :  }
     474             :  {
     475           1 :   std::cerr << "Test9\n";
     476           2 :   lts_aut_t t9=parse_aut(test9);
     477           1 :   reduce(t9,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     478           1 :   BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==2);
     479           1 :   t9=parse_aut(test9);
     480           1 :   reduce(t9,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
     481           1 :   BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==2);
     482           1 :   t9=parse_aut(test9);
     483           1 :   reduce(t9,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
     484           1 :   BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==2);
     485           1 :   t9=parse_aut(test9);
     486           1 :   reduce(t9,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
     487           1 :   BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==2);
     488           1 :   t9=parse_aut(test9);
     489           1 :   reduce(t9,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     490           1 :   BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==1);
     491           1 :   t9=parse_aut(test9);
     492           1 :   reduce(t9,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
     493           1 :   BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==1);
     494           1 :   t9=parse_aut(test9);
     495           1 :   reduce(t9,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
     496           1 :   BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==1);
     497           1 :   t9=parse_aut(test9);
     498           1 :   reduce(t9,lts_eq_branching_bisim_sigref);
     499           1 :   BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==1);
     500           1 :   t9=parse_aut(test9);
     501           1 :   reduce(t9,lts_eq_weak_bisim); //Weak bisimulation reduction
     502           1 :   BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==1);
     503           1 :   t9=parse_aut(test9);
     504           1 :   reduce(t9,lts_eq_divergence_preserving_branching_bisim_gjkw); //Divergence-preserving branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     505           1 :   BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==2);
     506           1 :   t9=parse_aut(test9);
     507           1 :   reduce(t9,lts_eq_divergence_preserving_branching_bisim_gv); //Divergence-preserving branching bisimulation reduction [Groote/Vaandrager 1990]
     508           1 :   BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==2);
     509           1 :   t9=parse_aut(test9);
     510           1 :   reduce(t9,lts_eq_divergence_preserving_branching_bisim); //Divergence-preserving branching bisimulation reduction directly on LTS
     511           1 :   BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==2);
     512           1 :   t9=parse_aut(test9);
     513           1 :   reduce(t9,lts_eq_divergence_preserving_branching_bisim_sigref);
     514           1 :   BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==2);
     515           1 :   t9=parse_aut(test9);
     516           1 :   reduce(t9,lts_eq_divergence_preserving_weak_bisim); //Divergence preserving weak bisimulation reduction
     517           1 :   BOOST_CHECK(t9.num_states()==2 && t9.num_transitions()==2);
     518             :  }
     519             :  {
     520           1 :   std::cerr << "Test10\n";
     521           2 :   lts_aut_t t10=parse_aut(test10);
     522           1 :   reduce(t10,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     523           1 :   BOOST_CHECK(t10.num_states()==5 && t10.num_transitions()==7);
     524           1 :   t10=parse_aut(test10);
     525           1 :   reduce(t10,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
     526           1 :   BOOST_CHECK(t10.num_states()==5 && t10.num_transitions()==7);
     527           1 :   t10=parse_aut(test10);
     528           1 :   reduce(t10,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
     529           1 :   BOOST_CHECK(t10.num_states()==5 && t10.num_transitions()==7);
     530           1 :   t10=parse_aut(test10);
     531           1 :   reduce(t10,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
     532           1 :   BOOST_CHECK(t10.num_states()==5 && t10.num_transitions()==7);
     533           1 :   t10=parse_aut(test10);
     534           1 :   reduce(t10,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     535           1 :   BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
     536           1 :   t10=parse_aut(test10);
     537           1 :   reduce(t10,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
     538           1 :   BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
     539           1 :   t10=parse_aut(test10);
     540           1 :   reduce(t10,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
     541           1 :   BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
     542           1 :   t10=parse_aut(test10);
     543           1 :   reduce(t10,lts_eq_branching_bisim_sigref);
     544           1 :   BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
     545           1 :   t10=parse_aut(test10);
     546           1 :   reduce(t10,lts_eq_weak_bisim); //Weak bisimulation reduction
     547           1 :   BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
     548           1 :   t10=parse_aut(test10);
     549           1 :   reduce(t10,lts_eq_divergence_preserving_branching_bisim_gjkw); //Divergence-preserving branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     550           1 :   BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
     551           1 :   t10=parse_aut(test10);
     552           1 :   reduce(t10,lts_eq_divergence_preserving_branching_bisim_gv); //Divergence-preserving branching bisimulation reduction [Groote/Vaandrager 1990]
     553           1 :   BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
     554           1 :   t10=parse_aut(test10);
     555           1 :   reduce(t10,lts_eq_divergence_preserving_branching_bisim); //Divergence-preserving branching bisimulation reduction directly on LTS
     556           1 :   BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
     557           1 :   t10=parse_aut(test10);
     558           1 :   reduce(t10,lts_eq_divergence_preserving_branching_bisim_sigref);
     559           1 :   BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
     560           1 :   t10=parse_aut(test10);
     561           1 :   reduce(t10,lts_eq_divergence_preserving_weak_bisim); //Divergence preserving weak bisimulation reduction
     562           1 :   BOOST_CHECK(t10.num_states()==4 && t10.num_transitions()==5);
     563             :  }
     564             :  {
     565           1 :   std::cerr << "Test11\n";
     566           2 :   lts_aut_t t11=parse_aut(test11);
     567           1 :   reduce(t11,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     568           1 :   BOOST_CHECK(t11.num_states()==4 && t11.num_transitions()==5);
     569           1 :   t11=parse_aut(test11);
     570           1 :   reduce(t11,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
     571           1 :   BOOST_CHECK(t11.num_states()==4 && t11.num_transitions()==5);
     572           1 :   t11=parse_aut(test11);
     573           1 :   reduce(t11,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
     574           1 :   BOOST_CHECK(t11.num_states()==4 && t11.num_transitions()==5);
     575           1 :   t11=parse_aut(test11);
     576           1 :   reduce(t11,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
     577           1 :   BOOST_CHECK(t11.num_states()==4 && t11.num_transitions()==5);
     578           1 :   t11=parse_aut(test11);
     579           1 :   reduce(t11,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     580           1 :   BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
     581           1 :   t11=parse_aut(test11);
     582           1 :   reduce(t11,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
     583           1 :   BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
     584           1 :   t11=parse_aut(test11);
     585           1 :   reduce(t11,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
     586           1 :   BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
     587           1 :   t11=parse_aut(test11);
     588           1 :   reduce(t11,lts_eq_branching_bisim_sigref);
     589           1 :   BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
     590           1 :   t11=parse_aut(test11);
     591           1 :   reduce(t11,lts_eq_weak_bisim); //Weak bisimulation reduction
     592           1 :   BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
     593           1 :   t11=parse_aut(test11);
     594           1 :   reduce(t11,lts_eq_divergence_preserving_branching_bisim_gjkw); //Divergence-preserving branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     595           1 :   BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
     596           1 :   t11=parse_aut(test11);
     597           1 :   reduce(t11,lts_eq_divergence_preserving_branching_bisim_gv); //Divergence-preserving branching bisimulation reduction [Groote/Vaandrager 1990]
     598           1 :   BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
     599           1 :   t11=parse_aut(test11);
     600           1 :   reduce(t11,lts_eq_divergence_preserving_branching_bisim); //Divergence-preserving branching bisimulation reduction directly on LTS
     601           1 :   BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
     602           1 :   t11=parse_aut(test11);
     603           1 :   reduce(t11,lts_eq_divergence_preserving_branching_bisim_sigref);
     604           1 :   BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
     605           1 :   t11=parse_aut(test11);
     606           1 :   reduce(t11,lts_eq_divergence_preserving_weak_bisim); //Divergence-preserving weak bisimulation reduction
     607           1 :   BOOST_CHECK(t11.num_states()==2 && t11.num_transitions()==2);
     608             :  }
     609             :  {
     610           1 :   std::cerr << "Test12\n";
     611           2 :   lts_aut_t t12=parse_aut(test12);
     612           1 :   reduce(t12,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     613           1 :   BOOST_CHECK(t12.num_states()==6 && t12.num_transitions()==7);
     614           1 :   t12=parse_aut(test12);
     615           1 :   reduce(t12,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
     616           1 :   BOOST_CHECK(t12.num_states()==6 && t12.num_transitions()==7);
     617           1 :   t12=parse_aut(test12);
     618           1 :   reduce(t12,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
     619           1 :   BOOST_CHECK(t12.num_states()==6 && t12.num_transitions()==7);
     620           1 :   t12=parse_aut(test12);
     621           1 :   reduce(t12,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
     622           1 :   BOOST_CHECK(t12.num_states()==6 && t12.num_transitions()==7);
     623           1 :   t12=parse_aut(test12);
     624           1 :   reduce(t12,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     625           1 :   BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
     626           1 :   t12=parse_aut(test12);
     627           1 :   reduce(t12,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
     628           1 :   BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
     629           1 :   t12=parse_aut(test12);
     630           1 :   reduce(t12,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
     631           1 :   BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
     632           1 :   t12=parse_aut(test12);
     633           1 :   reduce(t12,lts_eq_branching_bisim_sigref);
     634           1 :   BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
     635           1 :   t12=parse_aut(test12);
     636           1 :   reduce(t12,lts_eq_weak_bisim); //Weak bisimulation reduction
     637           1 :   BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
     638           1 :   t12=parse_aut(test12);
     639           1 :   reduce(t12,lts_eq_divergence_preserving_branching_bisim_gjkw); //Divergence-preserving branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     640           1 :   BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
     641           1 :   t12=parse_aut(test12);
     642           1 :   reduce(t12,lts_eq_divergence_preserving_branching_bisim_gv); //Divergence-preserving branching bisimulation reduction [Groote/Vaandrager 1990]
     643           1 :   BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
     644           1 :   t12=parse_aut(test12);
     645           1 :   reduce(t12,lts_eq_divergence_preserving_branching_bisim); //Divergence-preserving branching bisimulation reduction directly on LTS
     646           1 :   BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
     647           1 :   t12=parse_aut(test12);
     648           1 :   reduce(t12,lts_eq_divergence_preserving_branching_bisim_sigref);
     649           1 :   BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
     650           1 :   t12=parse_aut(test12);
     651           1 :   reduce(t12,lts_eq_divergence_preserving_weak_bisim); //Divergence-preserving weak bisimulation reduction
     652           1 :   BOOST_CHECK(t12.num_states()==5 && t12.num_transitions()==6);
     653           1 :   t12=parse_aut(test12);
     654           1 :   reduce(t12,lts_red_tau_star); //Tau star reduction
     655           1 :   BOOST_CHECK(t12.num_states()==2 && t12.num_transitions()==3);
     656             :  }
     657             :  {
     658           1 :   std::cerr << "Test13\n";
     659           2 :   lts_aut_t t13=parse_aut(test13);
     660           1 :   reduce(t13,lts_eq_bisim_gjkw); //Strong bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     661           1 :   BOOST_CHECK(t13.num_states()==4 && t13.num_transitions()==4);
     662           1 :   t13=parse_aut(test13);
     663           1 :   reduce(t13,lts_eq_bisim_gv); //Strong bisimulation reduction [Groote/Vaandrager 1990]
     664           1 :   BOOST_CHECK(t13.num_states()==4 && t13.num_transitions()==4);
     665           1 :   t13=parse_aut(test13);
     666           1 :   reduce(t13,lts_eq_bisim); //Strong bisimulation reduction directly on LTS
     667           1 :   BOOST_CHECK(t13.num_states()==4 && t13.num_transitions()==4);
     668           1 :   t13=parse_aut(test13);
     669           1 :   reduce(t13,lts_eq_bisim_sigref); //Strong bisimulation reduction sigref [Blom/Orzan 2003]
     670           1 :   BOOST_CHECK(t13.num_states()==4 && t13.num_transitions()==4);
     671           1 :   t13=parse_aut(test13);
     672           1 :   reduce(t13,lts_eq_branching_bisim_gjkw); //Branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     673           1 :   BOOST_CHECK(t13.num_states()==2 && t13.num_transitions()==2);
     674           1 :   t13=parse_aut(test13);
     675           1 :   reduce(t13,lts_eq_branching_bisim_gv); //Branching bisimulation reduction [Groote/Vaandrager 1990]
     676           1 :   BOOST_CHECK(t13.num_states()==2 && t13.num_transitions()==2);
     677           1 :   t13=parse_aut(test13);
     678           1 :   reduce(t13,lts_eq_branching_bisim); //Branching bisimulation reduction directly on LTS
     679           1 :   BOOST_CHECK(t13.num_states()==2 && t13.num_transitions()==2);
     680           1 :   t13=parse_aut(test13);
     681           1 :   reduce(t13,lts_eq_branching_bisim_sigref);
     682           1 :   BOOST_CHECK(t13.num_states()==2 && t13.num_transitions()==2);
     683           1 :   t13=parse_aut(test13);
     684           1 :   reduce(t13,lts_eq_weak_bisim); //Weak bisimulation reduction
     685           1 :   BOOST_CHECK(t13.num_states()==2 && t13.num_transitions()==2);
     686           1 :   t13=parse_aut(test13);
     687           1 :   reduce(t13,lts_eq_divergence_preserving_branching_bisim_gjkw); //Divergence-preserving branching bisimulation reduction [Groote/Jansen/Keiren/Wijs 2017]
     688           1 :   BOOST_CHECK(t13.num_states()==3 && t13.num_transitions()==3);
     689           1 :   t13=parse_aut(test13);
     690           1 :   reduce(t13,lts_eq_divergence_preserving_branching_bisim_gv); //Divergence-preserving branching bisimulation reduction [Groote/Vaandrager 1990]
     691           1 :   BOOST_CHECK(t13.num_states()==3 && t13.num_transitions()==3);
     692           1 :   t13=parse_aut(test13);
     693           1 :   reduce(t13,lts_eq_divergence_preserving_branching_bisim); //Divergence-preserving branching bisimulation reduction directly on LTS
     694           1 :   BOOST_CHECK(t13.num_states()==3 && t13.num_transitions()==3);
     695           1 :   t13=parse_aut(test13);
     696           1 :   reduce(t13,lts_eq_divergence_preserving_branching_bisim_sigref);
     697           1 :   BOOST_CHECK(t13.num_states()==3 && t13.num_transitions()==3);
     698           1 :   t13=parse_aut(test13);
     699           1 :   reduce(t13,lts_eq_divergence_preserving_weak_bisim); //Divergence-preserving weak bisimulation reduction
     700           1 :   BOOST_CHECK(t13.num_states()==3 && t13.num_transitions()==3);
     701           1 :   t13=parse_aut(test13);
     702           1 :   reduce(t13,lts_red_tau_star); //Tau star reduction
     703           1 :   BOOST_CHECK(t13.num_states()==2 && t13.num_transitions()==1);
     704             :  }
     705           4 : }
     706             : 

Generated by: LCOV version 1.13