mCRL2
Searching...
No Matches
liblts_coupledsim.h
Go to the documentation of this file.
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//
7// (See accompanying file LICENSE_1_0.txt or copy at
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"
38
39namespace mcrl2
40{
41namespace lts
42{
43namespace 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
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
60 {
62 cs_game_node _to,
63 std::size_t _act,
64 std::string _label_of_action,
65 bool _weak = false
66 ) :
67 from(_from), to(_to), act(_act), label_of_action(_label_of_action), weak(_weak)
68 {}
69
71 std::size_t act;
72 std::string label_of_action;
73 bool weak;
74 };
75
76 // support
77 inline bool operator==(const cs_game_node &n0, const cs_game_node &n1)
78 {
79 return n0.flag == n1.flag
80 && n0.swapped == n1.swapped
81 && n0.act == n1.act
82 && n0.p == n1.p
83 && n0.q == n1.q;
84 }
85
86 // support
87 inline bool operator!=(const cs_game_node &n0, const cs_game_node &n1)
88 {
89 return !(n0 == n1);
90 }
91
92 // support
93 inline bool operator<(const cs_game_node &n0, const cs_game_node &n1)
94 {
95 return n0.flag != n1.flag ? n0.flag < n1.flag
96 : n0.act != n1.act ? n0.act < n1.act
97 : n0.swapped != n1.swapped ? n0.swapped < n1.swapped
98 : n0.p != n1.p ? n0.p < n1.p
99 : n0.q < n1.q;
100 }
101
102 // support / debug (display struct cs_game_node;
103 inline std::string to_string(const cs_game_node &n)
104 {
105 std::string fst = !n.swapped ? "p" : "q";
106 std::string snd = !n.swapped ? "q" : "p";
107
108 switch (n.flag)
109 {
110 case NODE_ATK:
111 return
112 "(" + fst + std::to_string(n.p) +
113 "," + snd + std::to_string(n.q) + ")a";
114
115 case NODE_CPL:
116 return "(Cpl,"
117 + fst + std::to_string(n.p) + ","
118 + snd + std::to_string(n.q) + ")d";
119
120 case NODE_DEF:
121 return
122 "(" + std::to_string(n.act) +
123 "," + fst + std::to_string(n.p) +
124 "," + snd + std::to_string(n.q) + ")d";
125
126 default: return "(<strange node>)?";
127 }
128 }
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 inline bool operator<(const cs_game_move &m0, const cs_game_move &m1)
141 {
142 return m0.from != m1.from ? m0.from < m1.from : m0.to < m1.to;
143 }
144
145// --
146
147template <class LTS_TYPE>
148 bool coupled_simulation_compare(LTS_TYPE& l1, LTS_TYPE& l2)
149 {
150 // ./liblts_weak_bisim.h:70
151 bool preserve_divergences = true;
152 weak_bisimulation_reduce(l1,preserve_divergences);
153 weak_bisimulation_reduce(l2,preserve_divergences);
154
156 << "Input LTSs now reduced "
157 << "(preserve_divergences:" << (preserve_divergences ? "true" : "false") << "), "
158 << "continue with reduced version."
159 << std::endl;
160
161 std::set<cs_game_node> attacker_nodes; // (flag=NODE_ATK, placeholder, node::int, node::int)
162 std::set<cs_game_node> defender_nodes; // (flag, act::int, (node:int, node::int))
163
164 std::map<cs_game_node,std::set<cs_game_node>> predecessors;
165 std::map<cs_game_node,int> successor_count;
166 std::map<cs_game_node,int> node_winner;
167 const int WIN_DEFENDER = 0, WIN_ATTACKER = 1;
168
169
170 std::set<cs_game_move> moves; // moves (node,node)
171 std::string move_label; // label as string representation.
172 std::ostringstream stream; // bypassing behavior (workaround for DEBUG)
173
174 /* Define game nodes here. */
175
176 /* Get Weak transitions. */
177 std::stack<transition> todo_weak;
178 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 l2_tran_from_node, l2_tran_into_node,
183 l1_tran_from_node, l1_tran_into_node;
184
186 << "Find weak transitions."
187 << std::endl;
188
189 { // restructure l1 => get meta data and chain weak transitions.
190 for (const transition& t1 : l1.get_transitions())
191 {
192 l1_tran_from_node[t1.from()][t1] = true; // outgoing
193 l1_tran_into_node[t1.to()][t1] = true; // incoming
194
195 /* Every transition is a weak transition, append to todo. */
196 todo_weak.push(t1);
197
198 l1_weak_transitions.insert(t1);
199
200 // add tau loop for everyone.
201 l1_weak_transitions.insert(transition(t1.from(), 0, t1.from()));
202 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 while (!todo_weak.empty())
208 {
209 // pop and keep just start and extension.
210 // finish if next is second not tau.
211 transition weak = todo_weak.top();
212 todo_weak.pop();
213 std::size_t f = weak.from();
214 std::size_t l = weak.label();
215 std::size_t t = weak.to();
216 bool already_good = !l1.is_tau(l); // path already has a good action
217
218 const std::map<transition,bool>& next = l1_tran_from_node[t];
219 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 l1_weak_transitions.insert(weak);
224 l1_tran_into_node[t][weak] |= false;
225 l1_tran_from_node[f][weak] |= false;
226
227 if (len < 1) // no further steps.
228 {
229 continue;
230 }
231 else // just extend simply.
232 {
233 for (const auto& ntrans : next)
234 {
235 std::size_t next_label = ntrans.first.label();
236 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 */
242 {
243 /* Maybe use new label: If now good.*/
244 transition new_extended_weak
245 = transition(f,
246 !already_good ? next_label : l, ntrans.first.to());
247
249 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 for (const transition& t2 : l2.get_transitions())
259 {
260 l2_tran_from_node[t2.from()][t2] = true; // outgoing
261 l2_tran_into_node[t2.to()][t2] = true; // incoming
262
263 /* Every transition is a weak transition, append to todo. */
264 todo_weak.push(t2);
265 l2_weak_transitions.insert(t2);
266
267 // add tau loop for everyone.
268 l2_weak_transitions.insert(transition(t2.from(), 0, t2.from()));
269 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 while (!todo_weak.empty())
275 {
276 // pop and keep just start and extension.
277 // finish if next is second not tau.
278 transition weak = todo_weak.top();
279 todo_weak.pop();
280 std::size_t f = weak.from();
281 std::size_t l = weak.label();
282 std::size_t t = weak.to();
283 bool already_good = !l2.is_tau(l); // path already has a good action
284
285 const std::map<transition,bool>& next = l2_tran_from_node[t];
286 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 l2_weak_transitions.insert(weak);
291 l2_tran_into_node[t][weak] |= false;
292 l2_tran_from_node[f][weak] |= false;
293
294 if (len < 1) // no further steps.
295 {
296 continue;
297 }
298 else // just extend simply.
299 {
300 for (const auto &ntrans : next)
301 {
302 std::size_t next_label = ntrans.first.label();
303 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 */
309 {
310 /* Maybe use new label: If now good.*/
311 transition new_extended_weak
312 = transition(f, !already_good ? next_label : l, ntrans.first.to());
313
315 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
324 << "Creating now the cs-game arena."
325 << std::endl;
326
327 for (std::size_t p0 = 0; p0 < l1.num_states(); p0++)
328 {
329 for (std::size_t q0 = 0; q0 < l2.num_states(); q0++)
330 {
331 cs_game_node p0q0 = {NODE_ATK, 0, p0, q0, false}; // atk (p0,q0)
332 cs_game_node cplp0q0 = {NODE_CPL, 0, p0, q0, false}; // (cpl,p0,q0)
333
334 /* swapped. */
335 cs_game_node q0p0 = {NODE_ATK, 0, q0, p0, true}; // swapped (q0,p0)
336 cs_game_node cplq0p0 = {NODE_CPL, 0, q0, p0, true}; // swapped (cpl,q0,p0)
337
338 attacker_nodes.insert(p0q0);
339 attacker_nodes.insert(q0p0);
340 defender_nodes.insert(cplp0q0);
341 defender_nodes.insert(cplq0p0);
342
343 moves.emplace(p0q0, cplp0q0, 0, "cpl"); // (p0,q0) -> (Cpl,p0,q0)
344 moves.emplace(q0p0, cplq0p0, 0, "cpl"); // (q0,p0) -> (Cpl,q0,p0)
345
346 /* bisim: coupling answer q'=q, p'=p*/
347 moves.emplace(cplp0q0, q0p0, 0, "bisim");
348 moves.emplace(cplq0p0, p0q0, 0, "bisim");
349
350 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 for (const auto& t1 : l1_tran_from_node[p0])
359 {
360 std::size_t a = t1.first.label();
361 std::size_t p1 = t1.first.to();
362 bool atau = l1.is_tau(a);
363 bool strong = t1.second; // transition was strong
364
365 stream << (l1.action_label(a));
366 move_label = stream.str();
367 stream.str("");
368 stream.clear();
369
370 // --
371
372 // only strong
373 if (strong)
374 {
375 /* (p0,q0) -> (a,p1,q0), if [p0] a -> [p1] */
376 cs_game_node ap1q0 = {NODE_DEF, a, p1, q0, false};
377 defender_nodes.insert(ap1q0);
378 moves.emplace(p0q0, ap1q0, a, move_label);
379
380 if (atau) // => answering q0 can also stay.
381 {
382 cs_game_node q0_stay = {NODE_ATK, 0, p1, q0, false};
383 attacker_nodes.insert(q0_stay);
384 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 for (const transition &bq1 : l2.get_transitions())
393 {
394 std::size_t b = bq1.label(), q1 = bq1.to();
395
396 // strong q a-> q1 demonstrates, p0 a=> p1 simulates.
397 if (l2.action_label(b) == l1.action_label(a))
398 {
399 /* (a, q1, p0) -> (q1, p1), ... if p0 a=> p1.*/
400 cs_game_node bqp0 = {NODE_DEF, b, q1, p0, true}; // (b, q, p0)d
401 cs_game_node qp1 = {NODE_ATK, 0, q1, p1, true};
402 defender_nodes.insert(bqp0);
403 attacker_nodes.insert(qp1);
404 // todo_if.insert(); // waiting list for this move on condition.
405 moves.emplace(bqp0, qp1, a, move_label);
406 }
407 }
408
409 /* Coupling, .. if p0 => p1 */
410 if (atau) // for cplq0p0, answer the swapped cpl-challenge
411 {
412 cs_game_node p0p1 = {NODE_ATK, 0, p1, q0, false}; // swapping
413 attacker_nodes.insert(p0p1);
414 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 for (const auto &t2 : l2_tran_from_node[q0])
425 {
426 std::size_t b = t2.first.label();
427 std::size_t q1 = t2.first.to();
428 bool btau = l2.is_tau(b);
429 bool strong = t2.second; // transition was strong
430
431 stream << (l2.action_label(b));
432 move_label = stream.str();
433 stream.str("");
434 stream.clear();
435
436 // --
437
438 // only strong
439 if (strong) // only strong
440 {
441 /* swapped.
442 * (q0,p0) -> (a,q1,p0), if [q0] a -> [q1] */
443 cs_game_node bq1p0 = {NODE_DEF, b, q1, p0, true};
444 defender_nodes.insert(bq1p0);
445 moves.emplace(q0p0, bq1p0, b, move_label);
446
447 if (btau) // => answering q0 can also stay.
448 {
449 cs_game_node p0_stay = {NODE_ATK, 0, q1, p0, true};
450 attacker_nodes.insert(p0_stay);
451 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 for (const transition &ap1 : l1.get_transitions())
460 {
461 std::size_t a = ap1.label(), p1 = ap1.to();
462
463 // strong q a-> q1 demonstrates, p0 a=> p1 simulates.
464 if (l2.action_label(b) == l1.action_label(a))
465 {
466 /* (a, p1, q0) -> (p1, q1), ... if q0 a=> q1.*/
467 cs_game_node apq0 = {NODE_DEF, a, p1, q0, false}; // (a,p?,q0)d
468 cs_game_node pq1 = {NODE_ATK, 0, p1, q1, false}; // (p?,q1)a
469 defender_nodes.insert(apq0);
470 attacker_nodes.insert(pq1);
471 // todo_if.insert(); // waiting list for this move on condition.
472 moves.emplace(apq0, pq1, b, move_label);
473 }
474 }
475
476 /* Coupling, .. if q0 => q1 */
477 if (btau) // strong and weak, for cplp0q0
478 {
479 cs_game_node q0q1 = {NODE_ATK, 0, q1, p0, true}; // swapping
480 attacker_nodes.insert(q0q1);
481 moves.emplace(cplp0q0, q0q1, 0, "q \21d2 q'");
482 }
483 }
484 }
485 }
486
487 mCRL2log(log::verbose) << "The cs-game arena contains "
488 << attacker_nodes.size() << " attacker nodes and "
489 << defender_nodes.size() << " defender nodes."
490 << 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 for (const auto &m : moves)
497 {
498 cs_game_node pred = m.from;
499 cs_game_node succ = m.to;
500
501 /* All nodes set won by defender. */
502 node_winner[pred] = WIN_DEFENDER;
503 node_winner[succ] = WIN_DEFENDER;
504
505 /* Update predecessors for succ.
506 * Predecessors[succ] += [pred] */
507 predecessors[succ].insert(pred); // append predecessors.
508
509 /* Update succesors for the pred. */
510 successor_count[pred] += 1; // "append" successors.
511 }
512
513 std::stack<cs_game_node> todo;
514 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
518 << "Compute the winning area of the defender." << std::endl;
519
520 /* Calculate winning region. */
521 while (!todo.empty())
522 {
523 /* Pop from queue. */
524 cs_game_node n = todo.top();
525 todo.pop();
526
527 if (successor_count[n] <= 0)
528 {
529 if (node_winner[n] == WIN_DEFENDER)
530 {
531 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 for (const cs_game_node& pred : predecessors[n])
537 {
538 successor_count[pred] -= 1;
539 if (successor_count[pred] < 1 || attacker_nodes.count(pred))
540 {
541 todo.push(pred);
542 successor_count[pred] = 0; // to propagate next run.
543 }
544 }
545 }
546 }
547 }
548
550 << "Get coupled simulation from defender's winning area."
551 << std::endl;
552
553 char seperator[3] = {'\0', ' ', '\0'};
554 mCRL2log(log::verbose) << "R = {";
555
556 /* Filter R, where its elemens are coupled similar. */
557 std::set<cs_game_node> cs_relation;
558 for (const auto &n : attacker_nodes)
559 {
560#ifndef NDEBUG
561 if (node_winner.find(n) == node_winner.end())
562 {
563 std::cerr
564 << "I am requested, but never listed."
565 << " Set to default. (" << to_string(n) << std::endl;
566 }
567#endif // NDEBUG
568
569 if (node_winner[n] == WIN_DEFENDER)
570 {
571 cs_relation.insert(n);
572 mCRL2log(log::verbose) << seperator << to_string(n);
573 seperator[0] = ',';
574 }
575 }
576
577 mCRL2log(log::verbose) << "}" << std::endl;
578
579 /* Return true iff root nodes are in R / won by defender. */
580 cs_game_node roots[]
581 = { {NODE_ATK, 0, l1.initial_state(), l2.initial_state(), false}
582 , {NODE_ATK, 0, l2.initial_state(), l1.initial_state(), true}};
583
584 bool similar // root is in R
585 = node_winner[roots[0]] == WIN_DEFENDER
586 && node_winner[roots[1]] == WIN_DEFENDER;
587
588 return similar;
589 }
590} // end namespace detail
591} // end namespace lts
592} // end namespace mclr
593#endif // _LIBLTS_COUPLED_SIM_H
bool operator==(const ParityGameVertex &a, const ParityGameVertex &b)
Definition ParityGame.h:68
bool operator!=(const ParityGameVertex &a, const ParityGameVertex &b)
Definition ParityGame.h:73
A class containing triples, source label and target representing transitions.
Definition transition.h:47
size_type from() const
The source of the transition.
Definition transition.h:81
size_type label() const
The label of the transition.
Definition transition.h:87
size_type to() const
The target of the transition.
Definition transition.h:94
This file defines an algorithm for weak bisimulation, by calculating the transitive tau closure and a...
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
The file containing the core class for transition systems.
@ verbose
Definition logger.h:37
bool operator<(const action_summand &x, const action_summand &y)
Comparison operator for action summands.
const unsigned char NODE_ATK
bool coupled_simulation_compare(LTS_TYPE &l1, LTS_TYPE &l2)
void weak_bisimulation_reduce(LTS_TYPE &l, const bool preserve_divergences=false)
Reduce LTS l with respect to (divergence-preserving) weak bisimulation.
const unsigned char NODE_DEF
bool equals(const cs_game_move &m0, const cs_game_move &m1, bool weak_transition=false)
const unsigned char NODE_CPL
std::string to_string(const cs_game_node &n)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
cs_game_move(cs_game_node _from, cs_game_node _to, std::size_t _act, std::string _label_of_action, bool _weak=false)
A header file defining a transition as a triple from,label,to.