LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts/detail - liblts_coupledsim.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 206 237 86.9 %
Date: 2024-03-08 02:52:28 Functions: 6 7 85.7 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Huong Ngoc Le
       2             : //
       3             : // Copyright: see the accompanying file COPYING or copy at
       4             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       5             : //
       6             : // Distributed under the Boost Software License, Version 1.0.
       7             : // (See accompanying file LICENSE_1_0.txt or copy at
       8             : // http://www.boost.org/LICENSE_1_0.txt)
       9             : //
      10             : // \file lts/detail/liblts_coupledsim.h
      11             : //
      12             : // \brief algorithm for coupled simulation equivalence
      13             : //
      14             : // \details This file implements a computation of coupled simulation equivalence
      15             : // introduced by Parrow and Sjoedin in 1992 [PS92].  The algorithm creates a
      16             : // game arena from the given input and returns the solution based on solving the
      17             : // game with Graedel's algorithm on game graphs.
      18             : //
      19             : // \author Huong Ngoc Le
      20             : 
      21             : 
      22             : #ifndef _LIBLTS_COUPLED_SIM_H
      23             : #define _LIBLTS_COUPLED_SIM_H
      24             : 
      25             : #include <cstdlib>
      26             : #include <cstdio>
      27             : #include <fstream>
      28             : #include <iostream>
      29             : #include <algorithm>
      30             : #include <map>
      31             : #include <stack>
      32             : #include <string>
      33             : #include <vector>
      34             : #include "mcrl2/lts/lts.h"
      35             : #include "mcrl2/lts/detail/liblts_bisim.h"
      36             : #include "mcrl2/lts/detail/liblts_weak_bisim.h"
      37             : #include "mcrl2/lts/transition.h"
      38             : 
      39             : namespace mcrl2
      40             : {
      41             : namespace lts
      42             : {
      43             : namespace detail
      44             : {
      45             :   const unsigned char NODE_ATK = 0;  // placeholder indicating node is an attacker node
      46             :   const unsigned char NODE_DEF = 1;  // placeholder indicating a node, which is alwas reachable as coupling.
      47             :   const unsigned char NODE_CPL = 2;  // placeholder indicating a node, which is alwas reachable as coupling.
      48             : 
      49             :   // coupled simulation game node
      50             :   struct cs_game_node
      51             :   {
      52             :     unsigned char flag;
      53             :     std::size_t act;
      54             :     std::size_t p; std::size_t q;
      55             :     bool swapped;  // false := p is from lts1
      56             :   };
      57             : 
      58             :   // connection between game nodes
      59             :   struct cs_game_move
      60             :   {
      61         402 :     cs_game_move(cs_game_node _from,
      62             :       cs_game_node _to,
      63             :       std::size_t _act,
      64             :       std::string _label_of_action,
      65             :       bool _weak = false
      66         402 :     ) :
      67         402 :       from(_from), to(_to), act(_act), label_of_action(_label_of_action), weak(_weak)
      68         402 :     {}
      69             : 
      70             :     cs_game_node from, to;
      71             :     std::size_t act;
      72             :     std::string label_of_action;
      73             :     bool weak;
      74             :   };
      75             : 
      76             :   // support
      77        3627 :   inline bool operator==(const cs_game_node &n0, const cs_game_node &n1)
      78             :   {
      79        3627 :     return n0.flag == n1.flag
      80        3060 :       && n0.swapped == n1.swapped
      81        2497 :       && n0.act == n1.act
      82        2383 :       && n0.p == n1.p
      83        6687 :       && n0.q == n1.q;
      84             :   }
      85             : 
      86             :   // support
      87        3627 :   inline bool operator!=(const cs_game_node &n0, const cs_game_node &n1)
      88             :   {
      89        3627 :     return !(n0 == n1);
      90             :   }
      91             : 
      92             :   // support
      93       24508 :   inline bool operator<(const cs_game_node &n0, const cs_game_node &n1)
      94             :   {
      95       44490 :     return n0.flag != n1.flag ? n0.flag < n1.flag
      96       38508 :       : n0.act != n1.act ? n0.act < n1.act
      97       33987 :       : n0.swapped != n1.swapped ? n0.swapped < n1.swapped
      98       15461 :       : n0.p != n1.p ? n0.p < n1.p
      99       34454 :       : n0.q < n1.q;
     100             :   }
     101             : 
     102             :   // support / debug (display struct cs_game_node;
     103           0 :   inline std::string to_string(const cs_game_node &n)
     104             :   {
     105           0 :     std::string fst = !n.swapped ? "p" : "q";
     106           0 :     std::string snd = !n.swapped ? "q" : "p";
     107             : 
     108           0 :     switch (n.flag)
     109             :     {
     110           0 :       case NODE_ATK:
     111             :         return
     112           0 :           "(" + fst + std::to_string(n.p) +
     113           0 :           "," + snd + std::to_string(n.q) + ")a";
     114             : 
     115           0 :       case NODE_CPL:
     116             :         return "(Cpl,"
     117           0 :           + fst + std::to_string(n.p) + ","
     118           0 :           + snd + std::to_string(n.q) + ")d";
     119             : 
     120           0 :       case NODE_DEF:
     121             :         return
     122           0 :           "(" + std::to_string(n.act) +
     123           0 :           "," + fst + std::to_string(n.p) +
     124           0 :           "," + snd + std::to_string(n.q) + ")d";
     125             : 
     126           0 :       default: return "(<strange node>)?";
     127             :     }
     128           0 :   }
     129             : 
     130             :   // support
     131             :   inline bool equals(
     132             :       const cs_game_move &m0,
     133             :       const cs_game_move &m1,
     134             :       bool weak_transition = false)
     135             :   {
     136             :     return m0.act == m1.act && (!weak_transition && !(m0.weak || m1.weak));
     137             :   }
     138             : 
     139             :   // support
     140        3627 :   inline bool operator<(const cs_game_move &m0, const cs_game_move &m1)
     141             :   {
     142        3627 :     return m0.from != m1.from ? m0.from < m1.from : m0.to < m1.to;
     143             :   }
     144             : 
     145             : // --
     146             : 
     147             : template <class LTS_TYPE>
     148           1 :   bool coupled_simulation_compare(LTS_TYPE& l1, LTS_TYPE& l2)
     149             :   {
     150             :     // ./liblts_weak_bisim.h:70
     151           1 :     bool preserve_divergences = true;
     152           1 :     weak_bisimulation_reduce(l1,preserve_divergences);
     153           1 :     weak_bisimulation_reduce(l2,preserve_divergences);
     154             : 
     155           1 :     mCRL2log(log::debug)
     156             :       << "Input LTSs now reduced "
     157             :       << "(preserve_divergences:" << (preserve_divergences ? "true" : "false") << "), "
     158           0 :       << "continue with reduced version."
     159           0 :       << std::endl;
     160             : 
     161           1 :     std::set<cs_game_node> attacker_nodes;  // (flag=NODE_ATK, placeholder, node::int, node::int)
     162           1 :     std::set<cs_game_node> defender_nodes;  // (flag, act::int, (node:int, node::int))
     163             : 
     164           1 :     std::map<cs_game_node,std::set<cs_game_node>> predecessors;
     165           1 :     std::map<cs_game_node,int> successor_count;
     166           1 :     std::map<cs_game_node,int> node_winner;
     167           1 :     const int WIN_DEFENDER = 0, WIN_ATTACKER = 1;
     168             : 
     169             : 
     170           1 :     std::set<cs_game_move> moves;  // moves (node,node)
     171           1 :     std::string move_label; // label as string representation.
     172           1 :     std::ostringstream stream; // bypassing behavior (workaround for DEBUG)
     173             : 
     174             :     /* Define game nodes here. */
     175             : 
     176             :     /* Get Weak transitions. */
     177           1 :     std::stack<transition> todo_weak;
     178           1 :     std::set<transition> l1_weak_transitions, l2_weak_transitions; // do I need to save them?
     179             : 
     180             :     /* filter transitions of t2. */
     181             :     std::map<std::size_t, std::map<transition, bool>>  // if strong transition on true
     182           1 :       l2_tran_from_node, l2_tran_into_node,
     183           1 :       l1_tran_from_node, l1_tran_into_node;
     184             : 
     185           1 :     mCRL2log(log::debug)
     186           0 :       << "Find weak transitions."
     187           0 :       << std::endl;
     188             : 
     189             :     { // restructure l1 => get meta data and chain weak transitions.
     190           8 :       for (const transition& t1 : l1.get_transitions())
     191             :       {
     192           7 :         l1_tran_from_node[t1.from()][t1] = true;  // outgoing
     193           7 :         l1_tran_into_node[t1.to()][t1] = true;  // incoming
     194             : 
     195             :         /* Every transition is a weak transition, append to todo. */
     196           7 :         todo_weak.push(t1);
     197             : 
     198           7 :         l1_weak_transitions.insert(t1);
     199             : 
     200             :         // add tau loop for everyone.
     201           7 :         l1_weak_transitions.insert(transition(t1.from(), 0, t1.from()));
     202           7 :         l1_weak_transitions.insert(transition(t1.to(), 0, t1.to()));
     203             :       }
     204             : 
     205             :       /* Add weak transititions. */
     206             :       // on branching copy path and add all branches fins as fins.
     207          17 :       while (!todo_weak.empty())
     208             :       {
     209             :         // pop and keep just start and extension.
     210             :         // finish if next is second not tau.
     211          16 :         transition weak = todo_weak.top();
     212          16 :         todo_weak.pop();
     213          16 :         std::size_t f = weak.from();
     214          16 :         std::size_t l = weak.label();
     215          16 :         std::size_t t = weak.to();
     216          16 :         bool already_good = !l1.is_tau(l);  // path already has a good action
     217             : 
     218          16 :         const std::map<transition,bool>& next = l1_tran_from_node[t];
     219          16 :         std::size_t len = next.size();
     220             : 
     221             :         // XXX if (already_good) The current todo weak transition is already valid.
     222             :         // if it was strong before, it stays strong, else added as weak.
     223          16 :         l1_weak_transitions.insert(weak);
     224          16 :         l1_tran_into_node[t][weak] |= false;
     225          16 :         l1_tran_from_node[f][weak] |= false;
     226             : 
     227          16 :         if (len < 1)  // no further steps.
     228             :         {
     229           0 :           continue;
     230             :         }
     231             :         else  // just extend simply.
     232             :         {
     233          35 :           for (const auto& ntrans : next)
     234             :           {
     235          19 :             std::size_t next_label = ntrans.first.label();
     236          19 :             bool next_tau = l1.is_tau(next_label);
     237             : 
     238             :             /* If tau: extend new todo with extension.
     239             :              * If all before only tau: extend new todo with extension.
     240             :              */
     241          19 :             if (next_tau || !already_good)
     242             :             {
     243             :               /* Maybe use new label: If now good.*/
     244           9 :               transition new_extended_weak
     245             :                 = transition(f,
     246             :                     !already_good ? next_label : l, ntrans.first.to());
     247             : 
     248             :               // re-add new branches.
     249           9 :               todo_weak.push(new_extended_weak);
     250             :             }
     251             :           }
     252             :         }
     253             :         // current weak transition is done now.
     254             :       } // done l1 tau forest (all tau pathes).
     255             :     }
     256             : 
     257             :     { // ANALOG for l2
     258           7 :       for (const transition& t2 : l2.get_transitions())
     259             :       {
     260           6 :         l2_tran_from_node[t2.from()][t2] = true;  // outgoing
     261           6 :         l2_tran_into_node[t2.to()][t2] = true;  // incoming
     262             : 
     263             :         /* Every transition is a weak transition, append to todo. */
     264           6 :         todo_weak.push(t2);
     265           6 :         l2_weak_transitions.insert(t2);
     266             : 
     267             :         // add tau loop for everyone.
     268           6 :         l2_weak_transitions.insert(transition(t2.from(), 0, t2.from()));
     269           6 :         l2_weak_transitions.insert(transition(t2.to(), 0, t2.to()));
     270             :       }
     271             : 
     272             :       /* Add weak transititions. */
     273             :       // on branching copy path and add all branches fins as fins.
     274          10 :       while (!todo_weak.empty())
     275             :       {
     276             :         // pop and keep just start and extension.
     277             :         // finish if next is second not tau.
     278           9 :         transition weak = todo_weak.top();
     279           9 :         todo_weak.pop();
     280           9 :         std::size_t f = weak.from();
     281           9 :         std::size_t l = weak.label();
     282           9 :         std::size_t t = weak.to();
     283           9 :         bool already_good = !l2.is_tau(l);  // path already has a good action
     284             : 
     285           9 :         const std::map<transition,bool>& next = l2_tran_from_node[t];
     286           9 :         std::size_t len = next.size();
     287             : 
     288             :         // TODO: if (already_good) The current todo weak transition is already valid.
     289             :         // if it was strong before, it stays strong, else added as weak.
     290           9 :         l2_weak_transitions.insert(weak);
     291           9 :         l2_tran_into_node[t][weak] |= false;
     292           9 :         l2_tran_from_node[f][weak] |= false;
     293             : 
     294           9 :         if (len < 1)  // no further steps.
     295             :         {
     296           0 :           continue;
     297             :         }
     298             :         else  // just extend simply.
     299             :         {
     300          18 :           for (const auto &ntrans : next)
     301             :           {
     302           9 :             std::size_t next_label = ntrans.first.label();
     303           9 :             bool next_tau = l2.is_tau(next_label);
     304             : 
     305             :             /* If tau: extend new todo with extension.
     306             :              * If all before only tau: extend new todo with extension.
     307             :              */
     308           9 :             if (next_tau || !already_good)
     309             :             {
     310             :               /* Maybe use new label: If now good.*/
     311           3 :               transition new_extended_weak
     312             :                 = transition(f, !already_good ? next_label : l, ntrans.first.to());
     313             : 
     314             :               // re-add new branches.
     315           3 :               todo_weak.push(new_extended_weak);
     316             :             }
     317             :           }
     318             :         }
     319             :         // current weak transition is done now.
     320             :       } // done l2 tau forest (all tau pathes).
     321             :     }
     322             : 
     323           1 :     mCRL2log(log::verbose)
     324           0 :       << "Creating now the cs-game arena."
     325           0 :       << std::endl;
     326             : 
     327           6 :     for (std::size_t p0 = 0; p0 < l1.num_states(); p0++)
     328             :     {
     329          25 :       for (std::size_t q0 = 0; q0 < l2.num_states(); q0++)
     330             :       {
     331          20 :         cs_game_node p0q0 = {NODE_ATK, 0, p0, q0, false};  // atk (p0,q0)
     332          20 :         cs_game_node cplp0q0 = {NODE_CPL, 0, p0, q0, false}; // (cpl,p0,q0)
     333             : 
     334             :         /* swapped. */
     335          20 :         cs_game_node q0p0 = {NODE_ATK, 0, q0, p0, true};  // swapped (q0,p0)
     336          20 :         cs_game_node cplq0p0 = {NODE_CPL, 0, q0, p0, true};  // swapped (cpl,q0,p0)
     337             : 
     338          20 :         attacker_nodes.insert(p0q0);
     339          20 :         attacker_nodes.insert(q0p0);
     340          20 :         defender_nodes.insert(cplp0q0);
     341          20 :         defender_nodes.insert(cplq0p0);
     342             : 
     343          20 :         moves.emplace(p0q0, cplp0q0, 0, "cpl");  // (p0,q0) -> (Cpl,p0,q0)
     344          20 :         moves.emplace(q0p0, cplq0p0, 0, "cpl");  // (q0,p0) -> (Cpl,q0,p0)
     345             : 
     346             :         /* bisim: coupling answer q'=q, p'=p*/
     347          20 :         moves.emplace(cplp0q0, q0p0, 0, "bisim");
     348          20 :         moves.emplace(cplq0p0, p0q0, 0, "bisim");
     349             : 
     350          20 :         std::map<cs_game_move, bool> todo_if;
     351             : 
     352             :         // TODO This includes also weak, as challenge giver invalid, and that is unnecessary!
     353             :         /* CREATED:
     354             :          * challenge: p0 a -> p1
     355             :          * answers : p0 a => p1, if there's q0 a -> q1
     356             :          * coupling : p0 => p1
     357             :          */
     358          76 :         for (const auto& t1 : l1_tran_from_node[p0])
     359             :         {
     360          56 :           std::size_t a = t1.first.label();
     361          56 :           std::size_t p1 = t1.first.to();
     362          56 :           bool atau = l1.is_tau(a);
     363          56 :           bool strong = t1.second;  // transition was strong
     364             : 
     365          56 :           stream << (l1.action_label(a));
     366          56 :           move_label = stream.str();
     367          56 :           stream.str("");
     368          56 :           stream.clear();
     369             : 
     370             :           // --
     371             : 
     372             :           // only strong
     373          56 :           if (strong)
     374             :           {
     375             :             /* (p0,q0) -> (a,p1,q0),  if [p0] a -> [p1] */
     376          28 :             cs_game_node ap1q0 = {NODE_DEF, a, p1, q0, false};
     377          28 :             defender_nodes.insert(ap1q0);
     378          28 :             moves.emplace(p0q0, ap1q0, a, move_label);
     379             : 
     380          28 :             if (atau)  // => answering q0 can also stay.
     381             :             {
     382          16 :               cs_game_node q0_stay = {NODE_ATK, 0, p1, q0, false};
     383          16 :               attacker_nodes.insert(q0_stay);
     384          16 :               moves.emplace(ap1q0, q0_stay, 0, "");
     385             :             }
     386             :           }
     387             : 
     388             :           /* ANSWER swapped, only if (q0,a,q1)
     389             :            * (a, q1,p0) -> (q1,q1),  if [p0] a => [p1]*/
     390             :           // if [*] a -> [2] exists, and then for all [2].
     391             :           // XXX reconsider, maybe TODO with delayed checks, bc l2_transitions are later reviewed
     392         392 :           for (const transition &bq1 : l2.get_transitions())
     393             :           {
     394         336 :             std::size_t b = bq1.label(), q1 = bq1.to();
     395             : 
     396             :             // strong q a-> q1 demonstrates, p0 a=> p1 simulates.
     397         336 :             if (l2.action_label(b) == l1.action_label(a))
     398             :             {
     399             :               /* (a, q1, p0) -> (q1, p1), ... if p0 a=> p1.*/
     400         104 :               cs_game_node bqp0 = {NODE_DEF, b, q1, p0, true};  // (b, q, p0)d
     401         104 :               cs_game_node qp1 = {NODE_ATK, 0, q1, p1, true};  /// (q,p1)a
     402         104 :               defender_nodes.insert(bqp0);
     403         104 :               attacker_nodes.insert(qp1);
     404             :               // todo_if.insert();  // waiting list for this move on condition.
     405         104 :               moves.emplace(bqp0, qp1, a, move_label);
     406             :             }
     407             :           }
     408             : 
     409             :           /* Coupling, .. if p0 => p1 */
     410          56 :           if (atau)  // for cplq0p0, answer the swapped cpl-challenge
     411             :           {
     412          24 :             cs_game_node p0p1 = {NODE_ATK, 0, p1, q0, false};  // swapping
     413          24 :             attacker_nodes.insert(p0p1);
     414          24 :             moves.emplace(cplq0p0, p0p1, 0, "p \21d2 p'");
     415             :           }
     416             :         }
     417             : 
     418             :         // TODO This includes also weak, as challenge giver invalid, and that is unnecessary!
     419             :         /* CREATED:
     420             :          * challenge: q0 b -> q1
     421             :          * answers : q0 b => q1,  if there's p0 b -> p1
     422             :          * coupling : q0 => q1
     423             :          */
     424          65 :         for (const auto &t2 : l2_tran_from_node[q0])
     425             :         {
     426          45 :           std::size_t b = t2.first.label();
     427          45 :           std::size_t q1 = t2.first.to();
     428          45 :           bool btau = l2.is_tau(b);
     429          45 :           bool strong = t2.second; // transition was strong
     430             : 
     431          45 :           stream << (l2.action_label(b));
     432          45 :           move_label = stream.str();
     433          45 :           stream.str("");
     434          45 :           stream.clear();
     435             : 
     436             :           // --
     437             : 
     438             :           // only strong
     439          45 :           if (strong)  // only strong
     440             :           {
     441             :             /* swapped.
     442             :              * (q0,p0) -> (a,q1,p0),  if [q0] a -> [q1] */
     443          30 :             cs_game_node bq1p0 = {NODE_DEF, b, q1, p0, true};
     444          30 :             defender_nodes.insert(bq1p0);
     445          30 :             moves.emplace(q0p0, bq1p0, b, move_label);
     446             : 
     447          30 :             if (btau)  // => answering q0 can also stay.
     448             :             {
     449          15 :               cs_game_node p0_stay = {NODE_ATK, 0, q1, p0, true};
     450          15 :               attacker_nodes.insert(p0_stay);
     451          15 :               moves.emplace(bq1p0, p0_stay, 0, "");
     452             :             }
     453             :           }
     454             : 
     455             :           /* ANSWER, only if (p0,b,p1)
     456             :            * (b, p1,q0) -> (p1,q1),  if [q0] a => [p1]*/
     457             :           // if [*] a -> [2] exists, and then for all [2].
     458             :           // XXX reconsider, maybe TODO with delayed checks, bc l2_transitions are later reviewed
     459         360 :           for (const transition &ap1 : l1.get_transitions())
     460             :           {
     461         315 :             std::size_t a = ap1.label(), p1 = ap1.to();
     462             : 
     463             :             // strong q a-> q1 demonstrates, p0 a=> p1 simulates.
     464         315 :             if (l2.action_label(b) == l1.action_label(a))
     465             :             {
     466             :               /* (a, p1, q0) -> (p1, q1), ... if q0 a=> q1.*/
     467          90 :               cs_game_node apq0 = {NODE_DEF, a, p1, q0, false};  // (a,p?,q0)d
     468          90 :               cs_game_node pq1 = {NODE_ATK, 0, p1, q1, false};  // (p?,q1)a
     469          90 :               defender_nodes.insert(apq0);
     470          90 :               attacker_nodes.insert(pq1);
     471             :               // todo_if.insert();  // waiting list for this move on condition.
     472          90 :               moves.emplace(apq0, pq1, b, move_label);
     473             :             }
     474             :           }
     475             : 
     476             :           /* Coupling, .. if q0 => q1 */
     477          45 :           if (btau)  // strong and weak, for cplp0q0
     478             :           {
     479          15 :             cs_game_node q0q1 = {NODE_ATK, 0, q1, p0, true};  // swapping
     480          15 :             attacker_nodes.insert(q0q1);
     481          15 :             moves.emplace(cplp0q0, q0q1, 0, "q \21d2 q'");
     482             :           }
     483             :         }
     484             :       }
     485             :     }
     486             : 
     487           1 :     mCRL2log(log::verbose) << "The cs-game arena contains "
     488           0 :       << attacker_nodes.size() << " attacker nodes and "
     489           0 :       << defender_nodes.size() << " defender nodes."
     490           0 :       << std::endl;
     491             : 
     492             :     // if linked before, we need to check, if it's already inserted,
     493             :     // otherwise it counts duplicated, though they were replaced by set
     494             :     // attribites.
     495             : 
     496         253 :     for (const auto &m : moves)
     497             :     {
     498         252 :       cs_game_node pred = m.from;
     499         252 :       cs_game_node succ = m.to;
     500             : 
     501             :       /* All nodes set won by defender. */
     502         252 :       node_winner[pred] = WIN_DEFENDER;
     503         252 :       node_winner[succ] = WIN_DEFENDER;
     504             : 
     505             :       /* Update predecessors for succ.
     506             :        * Predecessors[succ] += [pred] */
     507         252 :       predecessors[succ].insert(pred);  // append predecessors.
     508             : 
     509             :       /* Update succesors for the pred. */
     510         252 :       successor_count[pred] += 1;  // "append" successors.
     511             :     }
     512             : 
     513           1 :     std::stack<cs_game_node> todo;
     514          99 :     for (const cs_game_node& d : defender_nodes) todo.push(d); // XXX make me better
     515             :     // todo.assign(defender_nodes.begin(), defender_nodes.end());
     516             : 
     517           1 :     mCRL2log(log::verbose)
     518           0 :       << "Compute the winning area of the defender." << std::endl;
     519             : 
     520             :     /* Calculate winning region. */
     521         172 :     while (!todo.empty())
     522             :     {
     523             :       /* Pop from queue. */
     524         171 :       cs_game_node n = todo.top();
     525         171 :       todo.pop();
     526             : 
     527         171 :       if (successor_count[n] <= 0)
     528             :       {
     529         102 :         if (node_winner[n] == WIN_DEFENDER)
     530             :         {
     531          66 :           node_winner[n] = WIN_ATTACKER;
     532             : 
     533             :           /* now reduce it from all predecessors as successor.
     534             :            * and check if the predecessor is also about to be won by the
     535             :            * attacker. */
     536         188 :           for (const cs_game_node& pred : predecessors[n])
     537             :           {
     538         122 :             successor_count[pred] -= 1;
     539         122 :             if (successor_count[pred] < 1 || attacker_nodes.count(pred))
     540             :             {
     541          73 :               todo.push(pred);
     542          73 :               successor_count[pred] = 0; // to propagate next run.
     543             :             }
     544             :           }
     545             :         }
     546             :       }
     547             :     }
     548             : 
     549           1 :     mCRL2log(log::verbose)
     550           0 :       << "Get coupled simulation from defender's winning area."
     551           0 :       << std::endl;
     552             : 
     553           1 :     char seperator[3] = {'\0', ' ', '\0'};
     554           1 :     mCRL2log(log::verbose) << "R = {";
     555             : 
     556             :     /* Filter R, where its elemens are coupled similar. */
     557           1 :     std::set<cs_game_node> cs_relation;
     558          41 :     for (const auto &n : attacker_nodes)
     559             :     {
     560             : #ifndef NDEBUG
     561          40 :       if (node_winner.find(n) == node_winner.end())
     562             :       {
     563             :         std::cerr
     564             :           << "I am requested, but never listed."
     565           0 :           << " Set to default. (" << to_string(n) << std::endl;
     566             :       }
     567             : #endif // NDEBUG
     568             : 
     569          40 :       if (node_winner[n] == WIN_DEFENDER)
     570             :       {
     571          17 :         cs_relation.insert(n);
     572          17 :         mCRL2log(log::verbose) << seperator << to_string(n);
     573          17 :         seperator[0] = ',';
     574             :       }
     575             :     }
     576             : 
     577           1 :     mCRL2log(log::verbose) << "}" << std::endl;
     578             : 
     579             :     /* Return true iff root nodes are in R / won by defender. */
     580           5 :     cs_game_node roots[]
     581           1 :       = { {NODE_ATK, 0, l1.initial_state(), l2.initial_state(), false}
     582           1 :         , {NODE_ATK, 0, l2.initial_state(), l1.initial_state(), true}};
     583             : 
     584           1 :     bool similar  // root is in R
     585           1 :       = node_winner[roots[0]] == WIN_DEFENDER
     586           1 :       && node_winner[roots[1]] == WIN_DEFENDER;
     587             : 
     588           1 :     return similar;
     589           1 :   }
     590             : }  // end namespace detail
     591             : }  // end namespace lts
     592             : }  // end namespace mclr
     593             : #endif  // _LIBLTS_COUPLED_SIM_H

Generated by: LCOV version 1.14