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
|