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

          Line data    Source code
       1             : // Author(s): Muck van Weerdenburg, 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             : #define BOOST_TEST_MODULE compare
      10             : #include <boost/test/included/unit_test.hpp>
      11             : 
      12             : #include "mcrl2/lts/lts_algorithm.h"
      13             : 
      14             : using namespace mcrl2::lts;
      15             : 
      16         260 : static lts_aut_t parse_aut(const std::string& s)
      17             : {
      18         260 :   std::stringstream is(s);
      19         260 :   lts_aut_t l;
      20         260 :   l.load(is);
      21         520 :   return l;
      22         260 : }
      23             : 
      24             : // a.(b+c)
      25             : const std::string l1 =
      26             :   "des(0,3,4)\n"
      27             :   "(0,\"a\",1)\n"
      28             :   "(1,\"b\",2)\n"
      29             :   "(1,\"c\",3)\n";
      30             : 
      31             : // a.b+a.c
      32             : const std::string l2 =
      33             :   "des(0,4,5)\n"
      34             :   "(0,\"a\",1)\n"
      35             :   "(0,\"a\",2)\n"
      36             :   "(1,\"b\",3)\n"
      37             :   "(2,\"c\",4)\n";
      38             : 
      39             : // a.b+a.c+ a.(b+c)
      40             : const std::string l2a =
      41             :   "des(0,7,8)\n"
      42             :   "(0,\"a\",1)\n"
      43             :   "(0,\"a\",2)\n"
      44             :   "(1,\"b\",3)\n"
      45             :   "(2,\"c\",4)\n"
      46             :   "(0,\"a\",5)\n"
      47             :   "(5,\"b\",6)\n"
      48             :   "(5,\"c\",7)\n";
      49             : 
      50             : // a.tau.(b+c)
      51             : const std::string l3 =
      52             :   "des(0,4,5)\n"
      53             :   "(0,\"a\",1)\n"
      54             :   "(1,\"tau\",2)\n"
      55             :   "(2,\"b\",3)\n"
      56             :   "(2,\"c\",4)\n";
      57             : 
      58             : // a.(b+b)
      59             : const std::string l4 =
      60             :   "des(0,3,4)\n"
      61             :   "(0,\"a\",1)\n"
      62             :   "(1,\"b\",2)\n"
      63             :   "(1,\"b\",3)\n";
      64             : 
      65             : // a
      66             : const std::string a =
      67             :   "des (0,1,2)\n"
      68             :   "(0,\"a\",1)\n";
      69             : 
      70             : // b
      71             : const std::string b =
      72             :   "des (0,1,2)\n"
      73             :   "(0,\"b\",1)\n";
      74             : 
      75             : static inline
      76          89 : bool preorder_compare(const std::string& s1, const std::string& s2, lts_preorder pre)
      77             : {
      78          89 :   lts_aut_t t1=parse_aut(s1);
      79          89 :   lts_aut_t t2=parse_aut(s2);
      80         178 :   return compare(t1, t2, pre,false);
      81          89 : }
      82             : 
      83             : static inline
      84          41 : bool compare(const std::string& s1, const std::string& s2, lts_equivalence eq, bool counterexample=false)
      85             : {
      86          41 :   lts_aut_t t1=parse_aut(s1);
      87          41 :   lts_aut_t t2=parse_aut(s2);
      88          82 :   return compare(t1, t2, eq, counterexample);
      89          41 : }
      90             : 
      91           2 : BOOST_AUTO_TEST_CASE(test_reflexive)
      92             : {
      93           1 :   BOOST_CHECK(preorder_compare(l2a,l2a,lts_pre_sim));
      94           1 :   BOOST_CHECK(preorder_compare(l2a,l2a,lts_pre_trace));
      95           1 :   BOOST_CHECK(compare(l2a,l2a,lts_eq_sim));
      96           1 :   BOOST_CHECK(compare(l2a,l2a,lts_eq_trace));
      97           1 :   BOOST_CHECK(preorder_compare(l2a,l2a,lts_pre_ready_sim));
      98           1 :   BOOST_CHECK(compare(l2a,l2a,lts_eq_ready_sim));    
      99           1 : }
     100             : 
     101             : 
     102           2 : BOOST_AUTO_TEST_CASE(test_sim_1_2)
     103             : {
     104           1 :   BOOST_CHECK(!preorder_compare(l1,l2,lts_pre_sim));  
     105           1 :   BOOST_CHECK(preorder_compare(l2,l1,lts_pre_sim));
     106           1 :   BOOST_CHECK(!compare(l2,l1,lts_eq_sim));
     107           1 :   BOOST_CHECK(!compare(l1,l2,lts_eq_sim));    
     108           1 : }
     109             : 
     110           2 : BOOST_AUTO_TEST_CASE(test_sim_2_2a)
     111             : {
     112           1 :   BOOST_CHECK(preorder_compare(l2,l2a,lts_pre_sim));
     113           1 :   BOOST_CHECK(!preorder_compare(l2a,l2,lts_pre_sim));
     114           1 :   BOOST_CHECK(!compare(l2a,l2,lts_eq_sim));
     115           1 :   BOOST_CHECK(!compare(l2,l2a,lts_eq_sim));    
     116           1 : }
     117             : 
     118           2 : BOOST_AUTO_TEST_CASE(test_sim_1_3)
     119             : {
     120           1 :   BOOST_CHECK(!preorder_compare(l1,l3,lts_pre_sim));
     121           1 :   BOOST_CHECK(!preorder_compare(l3,l1,lts_pre_sim));
     122           1 :   BOOST_CHECK(!compare(l3,l1,lts_eq_sim));
     123           1 :   BOOST_CHECK(!compare(l1,l3,lts_eq_sim));    
     124           1 : }
     125             : 
     126             : 
     127           2 : BOOST_AUTO_TEST_CASE(test_sim_1_4)
     128             : {
     129           1 :   BOOST_CHECK(!preorder_compare(l1,l4,lts_pre_sim));
     130           1 :   BOOST_CHECK(preorder_compare(l4,l1,lts_pre_sim));
     131           1 :   BOOST_CHECK(!compare(l1,l4,lts_eq_sim));
     132           1 :   BOOST_CHECK(!compare(l4,l1,lts_eq_sim));
     133           1 : }
     134             : 
     135             : 
     136           2 : BOOST_AUTO_TEST_CASE(test_ready_sim_1_2)
     137             : {
     138           1 :   BOOST_CHECK(!preorder_compare(l1,l2,lts_pre_ready_sim));
     139           1 :   BOOST_CHECK(!preorder_compare(l2,l1,lts_pre_ready_sim));
     140           1 :   BOOST_CHECK(!compare(l2,l1,lts_eq_ready_sim));
     141           1 :   BOOST_CHECK(!compare(l1,l2,lts_eq_ready_sim));  
     142           1 : }
     143             : 
     144           2 : BOOST_AUTO_TEST_CASE(test_ready_sim_2_2a)
     145             : {
     146           1 :   BOOST_CHECK(preorder_compare(l2,l2a,lts_pre_ready_sim));      
     147           1 :   BOOST_CHECK(!preorder_compare(l2a,l2,lts_pre_ready_sim));
     148           1 :   BOOST_CHECK(!compare(l2,l2a,lts_eq_ready_sim));      
     149           1 :   BOOST_CHECK(!compare(l2a,l2,lts_eq_ready_sim));  
     150           1 : }
     151             : 
     152           2 : BOOST_AUTO_TEST_CASE(test_ready_sim_1_3)
     153             : {
     154           1 :   BOOST_CHECK(!preorder_compare(l1,l3,lts_pre_ready_sim));
     155           1 :   BOOST_CHECK(!preorder_compare(l3,l1,lts_pre_ready_sim));
     156           1 :   BOOST_CHECK(!compare(l3,l1,lts_eq_ready_sim));  
     157           1 : }
     158             : 
     159           2 : BOOST_AUTO_TEST_CASE(test_ready_sim_1_4)
     160             : {
     161           1 :   BOOST_CHECK(!preorder_compare(l1,l4,lts_pre_ready_sim));
     162           1 :   BOOST_CHECK(!preorder_compare(l4,l1,lts_pre_ready_sim));
     163           1 :   BOOST_CHECK(!compare(l1,l4,lts_eq_ready_sim));  
     164           1 : }
     165             : 
     166           2 : BOOST_AUTO_TEST_CASE(test_symmetric_trace_1_2)
     167             : {
     168           1 :   BOOST_CHECK(compare(l1,l2,lts_eq_trace));
     169           1 :   BOOST_CHECK(compare(l2,l1,lts_eq_trace));
     170           1 :   BOOST_CHECK(!compare(l2,l1,lts_eq_bisim));
     171           1 :   BOOST_CHECK(!compare(l2,l1,lts_eq_bisim_gv));
     172           1 :   BOOST_CHECK(!compare(l2,l1,lts_eq_bisim_gjkw));
     173           1 :   BOOST_CHECK(preorder_compare(l1,l2,lts_pre_trace));
     174           1 :   BOOST_CHECK(preorder_compare(l2,l1,lts_pre_trace));
     175           1 :   BOOST_CHECK(preorder_compare(l1,l2,lts_pre_trace_anti_chain));
     176           1 :   BOOST_CHECK(preorder_compare(l2,l1,lts_pre_trace_anti_chain));
     177           1 :   BOOST_CHECK(preorder_compare(l1,l2,lts_pre_failures_refinement));
     178           1 :   BOOST_CHECK(!preorder_compare(l2,l1,lts_pre_failures_refinement));
     179           1 :   BOOST_CHECK(preorder_compare(l1,l2,lts_pre_failures_divergence_refinement));
     180           1 :   BOOST_CHECK(!preorder_compare(l2,l1,lts_pre_failures_divergence_refinement));
     181           1 : }
     182             : 
     183           2 : BOOST_AUTO_TEST_CASE(test_symmetric_trace_1_2a)
     184             : {
     185           1 :   BOOST_CHECK(compare(l2,l2a,lts_eq_trace));
     186           1 :   BOOST_CHECK(compare(l2a,l2,lts_eq_trace));
     187           1 :   BOOST_CHECK(!compare(l2a,l2,lts_eq_bisim));
     188           1 :   BOOST_CHECK(!compare(l2a,l2,lts_eq_bisim_gv));
     189           1 :   BOOST_CHECK(!compare(l2a,l2,lts_eq_bisim_gjkw));
     190           1 :   BOOST_CHECK(preorder_compare(l2,l2a,lts_pre_trace));
     191           1 :   BOOST_CHECK(preorder_compare(l2a,l2,lts_pre_trace));
     192           1 :   BOOST_CHECK(preorder_compare(l2,l2a,lts_pre_trace_anti_chain));
     193           1 :   BOOST_CHECK(preorder_compare(l2a,l2,lts_pre_trace_anti_chain));
     194           1 :   BOOST_CHECK(preorder_compare(l2,l2a,lts_pre_failures_refinement));
     195           1 :   BOOST_CHECK(preorder_compare(l2a,l2,lts_pre_failures_refinement));
     196           1 :   BOOST_CHECK(preorder_compare(l2,l2a,lts_pre_failures_divergence_refinement));
     197           1 :   BOOST_CHECK(preorder_compare(l2a,l2,lts_pre_failures_divergence_refinement));
     198           1 : }
     199             : 
     200           2 : BOOST_AUTO_TEST_CASE(test_symmetric_trace_1_3)
     201             : {
     202           1 :   BOOST_CHECK(!compare(l1,l3,lts_eq_trace));
     203           1 :   BOOST_CHECK(!compare(l3,l1,lts_eq_trace));
     204           1 :   BOOST_CHECK(compare(l1,l3,lts_eq_weak_trace));
     205           1 :   BOOST_CHECK(compare(l3,l1,lts_eq_weak_trace));
     206           1 :   BOOST_CHECK(!preorder_compare(l1,l3,lts_pre_trace_anti_chain));
     207           1 :   BOOST_CHECK(!preorder_compare(l3,l1,lts_pre_trace_anti_chain));
     208           1 :   BOOST_CHECK(preorder_compare(l1,l3,lts_pre_weak_trace_anti_chain));
     209           1 :   BOOST_CHECK(preorder_compare(l3,l1,lts_pre_weak_trace_anti_chain));
     210           1 :   BOOST_CHECK(!preorder_compare(l1,l3,lts_pre_failures_refinement));
     211           1 :   BOOST_CHECK(!preorder_compare(l3,l1,lts_pre_failures_refinement));
     212           1 :   BOOST_CHECK(preorder_compare(l1,l3,lts_pre_weak_failures_refinement));
     213           1 :   BOOST_CHECK(preorder_compare(l3,l1,lts_pre_weak_failures_refinement));
     214           1 :   BOOST_CHECK(preorder_compare(l1,l3,lts_pre_failures_divergence_refinement));
     215           1 :   BOOST_CHECK(preorder_compare(l3,l1,lts_pre_failures_divergence_refinement));
     216           1 : }
     217             : 
     218           2 : BOOST_AUTO_TEST_CASE(test_symmetric_trace_1_4)
     219             : {
     220           1 :   BOOST_CHECK(!compare(l1,l4,lts_eq_trace));
     221           1 :   BOOST_CHECK(!compare(l4,l1,lts_eq_trace));
     222           1 : }
     223             : 
     224           2 : BOOST_AUTO_TEST_CASE(test_symmetric_weak_trace_2_3)
     225             : {
     226           1 :   BOOST_CHECK(compare(l2,l3,lts_eq_weak_trace));
     227           1 :   BOOST_CHECK(compare(l3,l2,lts_eq_weak_trace));
     228           1 : }
     229             : 
     230           2 : BOOST_AUTO_TEST_CASE(test_symmetric_weak_trace_3_4)
     231             : {
     232           1 :   BOOST_CHECK(!compare(l4,l3,lts_eq_weak_trace));
     233           1 :   BOOST_CHECK(!compare(l3,l4,lts_eq_weak_trace));
     234           1 : }
     235             : 
     236             : // Regression test for bug #1082
     237           2 : BOOST_AUTO_TEST_CASE(test_bisim_a_b)
     238             : {
     239           1 :   BOOST_CHECK(!compare(a,b,lts_eq_bisim, true));
     240           1 : }
     241             : 
     242             : // a.(b.c1+d1) + a.(b.c2+d2)
     243             :   const std::string failures_law_left_hand_side =
     244             :    "des(0,8,6)\n"
     245             :    "(0,\"a\",1)\n"
     246             :    "(1,\"b\",2)\n"
     247             :    "(2,\"c1\",3)\n"
     248             :    "(1,\"d1\",3)\n"
     249             :    "(0,\"a\",4)\n"
     250             :    "(4,\"b\",5)\n"
     251             :    "(5,\"c2\",3)\n"
     252             :    "(4,\"d2\",3)\n";
     253             : 
     254             : // a.(b.c1+b.c2+d1) + a.(b.c2+b.c1+d2)
     255             :   const std::string failures_law_right_hand_side =
     256             :    "des(0,10,6)\n"
     257             :    "(0,\"a\",1)\n"
     258             :    "(1,\"b\",2)\n"
     259             :    "(2,\"c1\",3)\n"
     260             :    "(1,\"d1\",3)\n"
     261             :    "(1,\"b\",5)\n"
     262             :    "(0,\"a\",4)\n"
     263             :    "(4,\"b\",5)\n"
     264             :    "(4,\"b\",2)\n"
     265             :    "(5,\"c2\",3)\n"
     266             :    "(4,\"d2\",3)\n";
     267             : 
     268             : // The typical law for strong failures equivalence is 
     269             : // a.(b.x+u)+a.(b.y+v) = a.(b.x+b.y+u)+a.(b.x+b.y+v).
     270             : // The validity of this law is tested here, where the
     271             : // variables have been replaced by single actions.
     272           2 : BOOST_AUTO_TEST_CASE(laws_for_failures_equivalence)
     273             : {
     274           1 :   BOOST_CHECK(preorder_compare(failures_law_left_hand_side,failures_law_right_hand_side,lts_pre_failures_refinement));
     275           1 :   BOOST_CHECK(preorder_compare(failures_law_right_hand_side,failures_law_left_hand_side,lts_pre_failures_refinement));
     276           1 :   BOOST_CHECK(preorder_compare(failures_law_left_hand_side,failures_law_right_hand_side,lts_pre_trace));
     277           1 :   BOOST_CHECK(preorder_compare(failures_law_right_hand_side,failures_law_left_hand_side,lts_pre_trace));
     278           1 :   BOOST_CHECK(preorder_compare(failures_law_left_hand_side,failures_law_right_hand_side,lts_pre_trace_anti_chain));
     279           1 :   BOOST_CHECK(preorder_compare(failures_law_right_hand_side,failures_law_left_hand_side,lts_pre_trace_anti_chain));
     280           1 :   BOOST_CHECK(preorder_compare(failures_law_left_hand_side,failures_law_right_hand_side,lts_pre_failures_divergence_refinement));
     281           1 :   BOOST_CHECK(preorder_compare(failures_law_right_hand_side,failures_law_left_hand_side,lts_pre_failures_divergence_refinement));
     282           1 : }
     283             : 
     284             : // a.b + a.(b+c)
     285             :   const std::string ababc =
     286             :    "des(0,5,6)\n"
     287             :    "(0,\"a\",1)\n"
     288             :    "(1,\"b\",2)\n"
     289             :    "(0,\"a\",3)\n"
     290             :    "(3,\"b\",4)\n"
     291             :    "(3,\"c\",5)\n";
     292             : 
     293             : // a.(b+c) is typically failure included in a.b+a(b+c), but not vice versa.
     294           2 : BOOST_AUTO_TEST_CASE(failures_inclusion_test)
     295             : {
     296           1 :   BOOST_CHECK(preorder_compare(l1,ababc,lts_pre_failures_refinement));
     297           1 :   BOOST_CHECK(!preorder_compare(ababc,l1,lts_pre_failures_refinement));
     298           1 : }
     299             : 
     300             : // a.(tau.b + tau.c)
     301             :   const std::string a_taub_tauc =
     302             :    "des(0,5,6)\n"
     303             :    "(0,\"a\",1)\n"
     304             :    "(1,\"tau\",2)\n"
     305             :    "(2,\"b\",3)\n"
     306             :    "(1,\"tau\",4)\n"
     307             :    "(4,\"c\",5)\n";
     308             : 
     309             : // a.(tau.b+tau.c) and a.b + a.c are weak failure equivalent.
     310           2 : BOOST_AUTO_TEST_CASE(weak_failures_equivalence_test)
     311             : {
     312           1 :   BOOST_CHECK(!preorder_compare(l2,a_taub_tauc,lts_pre_failures_refinement));
     313           1 :   BOOST_CHECK(!preorder_compare(a_taub_tauc,l2,lts_pre_failures_refinement));
     314           1 :   BOOST_CHECK(preorder_compare(l2,a_taub_tauc,lts_pre_weak_trace));
     315           1 :   BOOST_CHECK(preorder_compare(a_taub_tauc,l2,lts_pre_weak_trace));
     316           1 :   BOOST_CHECK(preorder_compare(l2,a_taub_tauc,lts_pre_weak_trace_anti_chain));
     317           1 :   BOOST_CHECK(preorder_compare(a_taub_tauc,l2,lts_pre_weak_trace_anti_chain));
     318           1 :   BOOST_CHECK(preorder_compare(l2,a_taub_tauc,lts_pre_weak_failures_refinement));
     319           1 :   BOOST_CHECK(preorder_compare(a_taub_tauc,l2,lts_pre_weak_failures_refinement));
     320           1 : }
     321             : 
     322             : // a.b + a.(b+c)
     323             :   const std::string abc_div =
     324             :    "des(0,4,4)\n"
     325             :    "(0,\"a\",1)\n"
     326             :    "(1,\"tau\",1)\n"
     327             :    "(1,\"b\",2)\n"
     328             :    "(1,\"c\",3)\n";
     329             : 
     330             : // a.tau*(b+c) is typically failures equivalent to a.(b+c).
     331             : // But a.tau*.(b+c) is not failures-divergence included in a.(b+c). The reverse however holds.
     332           2 : BOOST_AUTO_TEST_CASE(failures_divergence_inclusion_test)
     333             : {
     334           1 :   BOOST_CHECK(!preorder_compare(l1,abc_div,lts_pre_failures_refinement));
     335           1 :   BOOST_CHECK(!preorder_compare(abc_div,l1,lts_pre_failures_refinement));
     336           1 :   BOOST_CHECK(preorder_compare(abc_div,l1,lts_pre_weak_trace));
     337           1 :   BOOST_CHECK(preorder_compare(l1,abc_div,lts_pre_weak_trace));
     338           1 :   BOOST_CHECK(preorder_compare(abc_div,l1,lts_pre_weak_trace_anti_chain));
     339           1 :   BOOST_CHECK(preorder_compare(l1,abc_div,lts_pre_weak_trace_anti_chain));
     340           1 :   BOOST_CHECK(!preorder_compare(l1,abc_div,lts_pre_weak_failures_refinement));
     341           1 :   BOOST_CHECK(preorder_compare(abc_div,l1,lts_pre_weak_failures_refinement));
     342           1 :   BOOST_CHECK(preorder_compare(l1,abc_div,lts_pre_failures_divergence_refinement));
     343           1 :   BOOST_CHECK(!preorder_compare(abc_div,l1,lts_pre_failures_divergence_refinement));
     344           1 : }
     345             : 
     346             : //  Example by Verum showing an error in the weak failures inclusion check. Did not work with 
     347             : //  the -c flag (which does not preprocess using branching bisimulation) but did work after
     348             : //  applying branching bisimulation.
     349             : 
     350             :   const std::string lts_impl =
     351             :    "des (1,8,6)\n"
     352             :    "(0,f,1)\n"
     353             :    "(1,b,2)\n"
     354             :    "(1,a,2)\n"
     355             :    "(2,tau,0)\n"
     356             :    "(2,tau,5)\n"
     357             :    "(3,tau,5)\n"
     358             :    "(4,tau,0)\n"
     359             :    "(5,t,1)\n";
     360             : 
     361             :   const std::string lts_spec =
     362             :    "des (1,5,3)\n"
     363             :    "(0,f,1)\n"
     364             :    "(1,b,2)\n"
     365             :    "(1,b,0)\n"
     366             :    "(1,a,2)\n"
     367             :    "(2,t,1)\n";
     368             :   
     369           2 : BOOST_AUTO_TEST_CASE(verum_test)
     370             : {
     371           1 :   BOOST_CHECK(!preorder_compare(lts_impl,lts_spec,lts_pre_failures_refinement));
     372           1 :   BOOST_CHECK(!preorder_compare(lts_impl,lts_spec,lts_pre_failures_divergence_refinement));
     373           1 :   BOOST_CHECK(!preorder_compare(lts_impl,lts_spec,lts_pre_weak_failures_refinement));
     374           1 :   BOOST_CHECK(!preorder_compare(lts_impl,lts_spec,lts_pre_weak_trace));
     375           1 :   BOOST_CHECK(!preorder_compare(lts_impl,lts_spec,lts_pre_trace));
     376           1 :   BOOST_CHECK(!preorder_compare(lts_impl,lts_spec,lts_pre_weak_trace_anti_chain));
     377           1 :   BOOST_CHECK(!preorder_compare(lts_impl,lts_spec,lts_pre_trace_anti_chain));
     378             : 
     379           1 :   BOOST_CHECK(!preorder_compare(lts_spec,lts_impl,lts_pre_failures_refinement));
     380           1 :   BOOST_CHECK(preorder_compare(lts_spec,lts_impl,lts_pre_failures_divergence_refinement));
     381           1 :   BOOST_CHECK(preorder_compare(lts_spec,lts_impl,lts_pre_weak_failures_refinement));
     382           1 :   BOOST_CHECK(preorder_compare(lts_spec,lts_impl,lts_pre_weak_trace));
     383           1 :   BOOST_CHECK(!preorder_compare(lts_spec,lts_impl,lts_pre_trace));
     384           1 :   BOOST_CHECK(preorder_compare(lts_spec,lts_impl,lts_pre_weak_trace_anti_chain));
     385           1 :   BOOST_CHECK(!preorder_compare(lts_spec,lts_impl,lts_pre_trace_anti_chain));
     386           1 : }
     387             : 
     388             : // P = a.P + tau.P
     389             : const std::string aPtauP =
     390             :   "des (0,2,1)\n"
     391             :   "(0,\"a\",0)\n"
     392             :   "(0,\"tau\",0)\n";
     393             : 
     394             : // P = b.P
     395             : const std::string bP =
     396             :   "des (0,1,1)\n"
     397             :   "(0,\"b\",0)\n";
     398             : 
     399             : // Check that diverging behaviour in a specification for failures-divergence refinement is
     400             : // regarded as catastrophic. Meaning that all failures are allowed after a divergence in spec.
     401             : // Furthermore check that for failures refinement that trace refinement holds as well. For
     402             : // failures refinement this does not hold, but here trace refinement is required so it does
     403             : // not hold.
     404           2 : BOOST_AUTO_TEST_CASE(failures_divergence_incomparable_test)
     405             : {
     406           1 :   BOOST_CHECK(!preorder_compare(aPtauP, bP, lts_pre_failures_refinement)); // empty = failures(aPtauP) subset failures(bP); traces(aPtauP) nsubset traces(bP).
     407           1 :   BOOST_CHECK(preorder_compare(bP, aPtauP, lts_pre_failures_divergence_refinement)); // failures(bP) subset failures(aPtau) != empty because divergences.
     408           1 : }
     409             : 
     410             : 
     411             : // Test belonging to #1595. Check wheter action a|b and b|a are considered equal. 
     412           2 : BOOST_AUTO_TEST_CASE(properly_order_multiactions)
     413             : {
     414             : 
     415             :   const std::string ab =
     416             :     "des (0,1,1)\n"
     417           1 :     "(0,\"a|b\",0)\n";
     418             :   
     419             :   // P = b.P
     420             :   const std::string ba =
     421             :     "des (0,1,1)\n"
     422           2 :     "(0,\"b|a\",0)\n";
     423             : 
     424           1 :   BOOST_CHECK(compare(ab, ba, lts_eq_bisim)); // These transition systems must be equal. 
     425           1 : }
     426             : 
     427             : // Test cases for coupled similarity
     428             : 
     429             : const std::string philosophers_gradual =
     430             :  "des (0,8,6)\n"
     431             :  "(0,\"tau\",1)\n"
     432             :  "(0,\"tau\",2)\n"
     433             :  "(1,\"tau\",3)\n"
     434             :  "(2,\"tau\",4)\n"
     435             :  "(2,\"tau\",5)\n"
     436             :  "(3,\"aEats\",3)\n"
     437             :  "(4,\"bEats\",4)\n"
     438             :  "(5,\"cEats\",5)\n"
     439             :  ;
     440             : 
     441             : const std::string philosophers_merged =
     442             :  "des (0,6,4)\n"
     443             :  "(0,\"tau\",1)\n"
     444             :  "(0,\"tau\",2)\n"
     445             :  "(0,\"tau\",3)\n"
     446             :  "(1,\"aEats\",1)\n"
     447             :  "(2,\"bEats\",2)\n"
     448             :  "(3,\"cEats\",3)\n"
     449             :  ;
     450             : 
     451           2 : BOOST_AUTO_TEST_CASE(coupled_similarity_test)
     452             : {
     453           1 :   BOOST_CHECK(compare(philosophers_gradual, philosophers_merged, lts_eq_coupled_sim)); // These transition systems must be equal.
     454           1 :   BOOST_CHECK(!compare(philosophers_gradual, philosophers_merged, lts_eq_bisim)); // These transition systems must be different.
     455           1 : }

Generated by: LCOV version 1.14