Line data Source code
1 : // Author(s): Jan Martens and Maurice Laveaux
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 : /// \file lts/detail/liblts_bisim_m.h
10 : ///
11 : /// \brief Partition refinement algorithm for guaruanteed minimal depth
12 : /// counter-examples.
13 : ///
14 : /// \details
15 : #ifndef MCRl2_LTS_LIBLTS_BRANCHING_BISIM_MINIMAL_DEPTH
16 : #define MCRl2_LTS_LIBLTS_BRANCHING_BISIM_MINIMAL_DEPTH
17 :
18 :
19 : #include "mcrl2/lts/detail/liblts_merge.h"
20 : #include "mcrl2/lts/detail/liblts_scc.h"
21 : #include "mcrl2/lts/detail/liblts_bisim_dnj.h"
22 : #include "mcrl2/lts/lts_aut.h"
23 : #include "mcrl2/lts/lts_dot.h"
24 : #include "mcrl2/lts/lts_fsm.h"
25 : #include "mcrl2/lts/lts_utilities.h"
26 : #include "mcrl2/modal_formula/state_formula.h"
27 :
28 : #include <fstream>
29 :
30 : namespace mcrl2::lts::detail
31 : {
32 :
33 : template <class LTS_TYPE>
34 : class branching_bisim_partitioner_minimal_depth
35 : {
36 : public:
37 : /** \brief Creates a branching bisimulation partitioner for an LTS.
38 : * \details This partitioner is specifically for creating minimal depth counter-examples for branching bisimulation.
39 : * It guarantees stability w.r.t. the old partition before considering new splitter blocks. This might cause
40 : * this implementation to be less efficient than other partitioners.
41 : * \param l Reference to the LTS.
42 : * \param init_l2 reference to the initial state of lts2.
43 : */
44 2 : branching_bisim_partitioner_minimal_depth(LTS_TYPE& l, const std::size_t init_l2)
45 2 : : m_lts(l),
46 2 : initial_l2(init_l2)
47 : {
48 :
49 17 : for (transition trans : m_lts.get_transitions())
50 : {
51 15 : trans_out[trans.from()].push_back(std::make_pair(trans.label(), trans.to()));
52 15 : if (is_tau(trans.label()))
53 : {
54 8 : silent_out[trans.from()].insert(trans.to());
55 8 : silent_in[trans.to()].insert(trans.from());
56 : }
57 : }
58 :
59 12 : for (state_type s = 0; s < m_lts.num_states(); s++)
60 : {
61 10 : state2block[s] = 0;
62 :
63 10 : if (silent_out[s].size() == 0)
64 : {
65 5 : bottom_states.push_back(s);
66 : }
67 : }
68 :
69 :
70 :
71 : // Initialize the partition with a single block.
72 2 : blocks.push_back(block());
73 2 : blocks[0].state_index = 0;
74 2 : blocks[0].block_index = 0;
75 2 : blocks[0].parent_block_index = 0;
76 2 : blocks[0].level = 0;
77 2 : level2blocksidx[0].insert(0);
78 :
79 : // Now we can start refining the partition.
80 2 : std::size_t num_old_blocks = 0;
81 2 : std::size_t num_blocks_created = 1;
82 2 : std::size_t level = 0;
83 :
84 6 : while (num_blocks_created > num_old_blocks && in_same_class(m_lts.initial_state(), initial_l2))
85 : {
86 4 : level += 1;
87 4 : num_old_blocks = num_blocks_created;
88 4 : num_blocks_created = refine_partition();
89 4 : assert(level2blocksidx[level].size() == num_blocks_created);
90 4 : state2sig = std::map<state_type, signature_type>();
91 4 : mCRL2log(mcrl2::log::verbose) << "Refined partition to " << num_blocks_created
92 0 : << " blocks on level " << level << "."
93 0 : << std::endl;
94 : }
95 2 : }
96 :
97 : /** \brief Creates a state formula that distinguishes state s from state t.
98 : * \details The states s and t are non branching bisimilar states. A distinguishign state formula phi is
99 : * returned, which has the property that s \in \sem{phi} and t \not\in\sem{phi}.
100 : * Based on the preprint "Minimal Depth Distinguishing Formulas without Until for Branching Bisimulation",
101 : * 2024 by Jan Martens and Jan Friso Groote.
102 : * \param[in] s The state number for which the resulting formula should be true
103 : * \param[in] t The state number for which the resulting formula should be false
104 : * \return A minimal observation depth distinguishing state formula, that is often also minimum negation-depth and
105 : * irreducible. */
106 2 : mcrl2::state_formulas::state_formula dist_formula_mindepth(size_t s, size_t t)
107 : {
108 2 : assert(s == m_lts.initial_state() && t == initial_l2);
109 2 : assert(state2block[s] != state2block[t]);
110 2 : std::pair<block_index_type, block_index_type> b1b2 = min_split_blockpair(state2block[s], state2block[t]);
111 4 : return dist_formula(b1b2.first, b1b2.second);
112 : }
113 :
114 8 : bool in_same_class(const std::size_t s, const std::size_t t) { return state2block[s] == state2block[t]; }
115 :
116 :
117 : private:
118 : LTS_TYPE& m_lts;
119 : state_type initial_l2;
120 : state_type max_state_index = 0;
121 : typedef std::size_t block_index_type;
122 : typedef std::size_t level_type;
123 : // This tuple is meant for an observation (s', a, s'') such that s -(silent)-> s' -a-> s''.
124 : typedef std::tuple<block_index_type, label_type, block_index_type> branching_observation_type;
125 : typedef std::set<branching_observation_type> signature_type;
126 : typedef std::pair<label_type, state_type> observation;
127 : typedef std::pair<block_index_type, block_index_type> blockpair_type;
128 :
129 : std::map<state_type, std::set<state_type>> silent_in;
130 : std::map<state_type, std::set<state_type>> silent_out;
131 : std::map<state_type, std::vector<observation>> trans_out;
132 : std::map<state_type, std::size_t> state2num_touched;
133 : std::map<state_type, block_index_type> state2block;
134 : std::map<state_type, signature_type> state2sig;
135 : std::vector<state_type> bottom_states;
136 : std::map<level_type, std::set<block_index_type>> level2blocksidx;
137 :
138 : std::map<std::pair<block_index_type, block_index_type>, mcrl2::state_formulas::state_formula> blockpair2formula;
139 : std::map<std::pair<block_index_type, block_index_type>, std::set<block_index_type>> blockpair2truths;
140 :
141 : struct block
142 : {
143 : state_type state_index; // The state number that represent the states in this block
144 : block_index_type block_index; // The sequence number of this block.
145 : block_index_type parent_block_index; // Index of the parent block. If there is no parent block, this refers to the block itself.
146 : level_type level; // The level of the block in the partition.
147 : signature_type sig;
148 :
149 : void swap(block& b)
150 : {
151 : std::swap(b.state_index, state_index);
152 : std::swap(b.block_index, block_index);
153 : std::swap(b.parent_block_index, parent_block_index);
154 : std::swap(b.level, level);
155 : }
156 :
157 31 : bool operator==(const block& other)
158 : {
159 31 : return block_index == other.block_index;
160 : }
161 :
162 31 : bool operator!=(const block& other)
163 : {
164 31 : return !(*this == other);
165 : }
166 : };
167 : std::vector<block> blocks;
168 :
169 : /*
170 : * Auxiliary function that computes whether a label is a tau index.
171 : */
172 74 : bool is_tau(label_type l)
173 : {
174 74 : return m_lts.is_tau(m_lts.apply_hidden_label_map(l));
175 : }
176 :
177 20 : signature_type get_signature(state_type s)
178 : {
179 20 : signature_type sig;
180 : // Add the block index of the state to the signature.
181 : // sig.insert(std::make_tuple(state2block[s], m_lts.tau_label_index(), state2block[s]));
182 36 : for (state_type target : silent_out[s])
183 : {
184 16 : sig.insert(state2sig[target].begin(), state2sig[target].end());
185 : }
186 50 : for (observation t : trans_out[s])
187 : {
188 30 : if (!is_tau(t.first) || state2block[s] != state2block[t.second])
189 : {
190 20 : sig.insert(std::make_tuple(state2block[s], t.first, state2block[t.second]));
191 : }
192 : }
193 :
194 20 : state2sig[s] = sig;
195 20 : return sig;
196 0 : }
197 :
198 : // Refine the partition exactly one level.
199 4 : std::size_t refine_partition()
200 : {
201 4 : std::queue<state_type> frontier;
202 : // start with bottom states.
203 14 : for (auto s : bottom_states)
204 : {
205 10 : frontier.push(s);
206 : }
207 4 : std::map<signature_type, block_index_type> sig2block;
208 4 : std::map<state_type, block_index_type> state2block_new;
209 4 : std::size_t num_blocks_created = 0;
210 : // Compute signatures in order of bottom states and reachability order.
211 44 : while (!frontier.empty())
212 : {
213 20 : state_type state = frontier.front();
214 20 : frontier.pop();
215 20 : signature_type sig = get_signature(state);
216 20 : if (sig2block.find(sig) == sig2block.end())
217 : {
218 : // Create the new block
219 17 : blocks.push_back(block());
220 17 : num_blocks_created += 1;
221 17 : block_index_type new_block_id = blocks.size() - 1;
222 17 : sig2block[sig] = new_block_id;
223 17 : blocks[new_block_id].state_index = state;
224 17 : blocks[new_block_id].block_index = new_block_id;
225 17 : blocks[new_block_id].parent_block_index = state2block[state];
226 17 : blocks[new_block_id].level = blocks[state2block[state]].level + 1;
227 17 : blocks[new_block_id].sig = sig;
228 17 : level2blocksidx[blocks[new_block_id].level].insert(new_block_id);
229 : }
230 :
231 20 : state2block_new[state] = sig2block[sig];
232 20 : state2num_touched[state] = 0;
233 :
234 36 : for (state_type backward : silent_in[state])
235 : {
236 16 : size_t max_out = silent_out[backward].size();
237 16 : state2num_touched[backward] += 1;
238 16 : if (state2num_touched[backward] == max_out)
239 : {
240 10 : frontier.push(backward);
241 : }
242 : }
243 : }
244 : // Now we have computed the new blocks, we can redefine the partition.
245 4 : state2block = state2block_new;
246 4 : return num_blocks_created;
247 4 : }
248 :
249 31 : std::pair<block_index_type, block_index_type> min_split_blockpair(block_index_type b1, block_index_type b2)
250 : {
251 31 : assert(blocks[b1] != blocks[b2] && blocks[b1].level == blocks[b2].level);
252 31 : while (blocks[b1].parent_block_index != blocks[b2].parent_block_index)
253 : {
254 0 : b1 = blocks[b1].parent_block_index;
255 0 : b2 = blocks[b2].parent_block_index;
256 : }
257 31 : return std::make_pair(b1, b2);
258 : }
259 :
260 : /**
261 : * \brief conjunction Creates a conjunction of state formulas
262 : * \param terms The terms of the conjunction
263 : * \return The conjunctive state formula
264 : */
265 7 : mcrl2::state_formulas::state_formula conjunction(std::vector<mcrl2::state_formulas::state_formula>& conjunctions)
266 : {
267 : return utilities::detail::join<mcrl2::state_formulas::state_formula>(
268 : conjunctions.begin(),
269 : conjunctions.end(),
270 1 : [](mcrl2::state_formulas::state_formula a, mcrl2::state_formulas::state_formula b)
271 1 : { return mcrl2::state_formulas::and_(a, b); },
272 7 : mcrl2::state_formulas::true_());
273 : }
274 :
275 2 : regular_formulas::regular_formula make_tau_hat(regular_formulas::regular_formula& f)
276 : {
277 4 : return regular_formulas::alt(f,
278 6 : regular_formulas::trans_or_nil(regular_formulas::regular_formula(action_formulas::false_())));
279 : }
280 :
281 : /**
282 : * \brief create_regular_formula Creates a regular formula that represents action a
283 : * \details In case the action comes from an LTS in the lts format.
284 : * \param a The action for which to create a regular formula
285 : * \return The created regular formula
286 : */
287 12 : regular_formulas::regular_formula create_regular_formula(const mcrl2::lts::action_label_string& a) const
288 : {
289 : // Copied from Olav no idea what it exactly does.
290 24 : return mcrl2::regular_formulas::regular_formula(mcrl2::action_formulas::multi_action(
291 48 : process::action_list({process::action(process::action_label(a, {}), {})})));
292 : }
293 :
294 : /**
295 : * \brief create_regular_formula Creates a regular formula that represents action a
296 : * \details In case the action comes from an LTS in the lts format.
297 : * \param a The action for which to create a regular formula
298 : * \return The created regular formula
299 : */
300 : regular_formulas::regular_formula create_regular_formula(const mcrl2::lps::multi_action& a) const
301 : {
302 : return regular_formulas::regular_formula(action_formulas::multi_action(a.actions()));
303 : }
304 :
305 : // Updates the truths values according the dist formula and the information in blockpair2truths.
306 13 : void split_and_intersect(std::set<block_index_type>& truths, std::pair<block_index_type, block_index_type> liftedB1B2)
307 : {
308 : // Add the observation to the formula
309 13 : level_type split_level = blocks[liftedB1B2.first].level;
310 :
311 13 : std::set<block_index_type> truths_new;
312 55 : for (block_index_type b_og : truths)
313 : {
314 42 : block_index_type b = b_og;
315 : // Check if b in phi (maybe lift the level)
316 42 : while (blocks[b].level > split_level)
317 : {
318 0 : b = blocks[b].parent_block_index;
319 : }
320 42 : if (blockpair2truths[liftedB1B2].find(b) != blockpair2truths[liftedB1B2].end())
321 : {
322 21 : truths_new.insert(b_og);
323 : }
324 : }
325 13 : truths = truths_new;
326 13 : }
327 :
328 : /**
329 : * \brief is_dist Checks if a given conjunction correctly exludes a set of blocks.
330 : * \param dist_blockpairs The blockpairs that were used to generate the conjuncts.
331 : * \param to_dist The set of blocks that should be excluded by the conjunction, forall b\in to_dist.
332 : * b\not\in\sem{phi_dist_blockpairs}. \return True if the conjunction correctly excludes the set of blocks, false
333 : * otherwise.
334 : */
335 5 : bool is_dist(std::set<blockpair_type>& dist_blockpairs,
336 : std::set<block_index_type>& to_dist)
337 : {
338 5 : if (to_dist.empty())
339 : {
340 0 : return true;
341 : }
342 5 : std::set<block_index_type> truths = level2blocksidx[blocks[*to_dist.begin()].level];
343 5 : return is_dist(dist_blockpairs, to_dist, truths);
344 5 : }
345 :
346 :
347 : /**
348 : * \brief is_dist overloaded to also maintain the truth values computed at the end.
349 : */
350 17 : bool is_dist(const std::set<blockpair_type>& dist_blockpairs,const std::set<block_index_type>& to_dist, std::set<block_index_type>& truths)
351 : {
352 17 : if (to_dist.empty())
353 : {
354 9 : return true;
355 : }
356 :
357 8 : truths = level2blocksidx[blocks[*to_dist.begin()].level];
358 16 : for (blockpair_type b1_b2 : dist_blockpairs)
359 : {
360 8 : split_and_intersect(truths, b1_b2);
361 : }
362 18 : for (block_index_type b : to_dist)
363 : {
364 14 : if (truths.find(b) != truths.end())
365 : {
366 4 : return false;
367 : }
368 : }
369 4 : return true;
370 : }
371 :
372 :
373 12 : std::vector<mcrl2::state_formulas::state_formula> filtered_dist_conjunction(
374 : std::map<blockpair_type, mcrl2::state_formulas::state_formula>& Phi,
375 : std::set<block_index_type>& Tdist,
376 : std::set<block_index_type>& Truths)
377 : {
378 12 : std::vector<mcrl2::state_formulas::state_formula> returnPhi;
379 12 : std::set<blockpair_type> phi_pairs_og;
380 17 : for (auto& phi_pair : Phi) {
381 5 : phi_pairs_og.insert(phi_pair.first);
382 : }
383 :
384 17 : for (auto& phi_pair : Phi) {
385 : // Remove the phi_pair from the formula.
386 5 : phi_pairs_og.erase(phi_pair.first);
387 : // Only add conjunct, if it wouldn't be distinguishing without.
388 5 : if (!is_dist(phi_pairs_og, Tdist))
389 : {
390 4 : phi_pairs_og.insert(phi_pair.first);
391 4 : returnPhi.push_back(phi_pair.second);
392 : }
393 : }
394 12 : is_dist(phi_pairs_og, Tdist, Truths);
395 :
396 24 : return returnPhi;
397 12 : }
398 :
399 : // This function computes the distinguishing state formula for two blocks.
400 : // Precondition is that the blocks are not the same, are on the same level and have the same parent block.
401 11 : mcrl2::state_formulas::state_formula dist_formula(block_index_type block_index1, block_index_type block_index2)
402 : {
403 11 : assert(block_index1 != block_index2);
404 11 : if (blockpair2formula.find(std::make_pair(block_index1, block_index2)) != blockpair2formula.end())
405 : {
406 : // We computed this already ( probably won't happen much in practice but guarantees polynomial runtime).
407 1 : return blockpair2formula[std::make_pair(block_index1, block_index2)];
408 : }
409 :
410 10 : block block1 = blocks[block_index1];
411 10 : block block2 = blocks[block_index2];
412 :
413 : // make blocks same level
414 10 : assert(block1.level == block2.level); // This should be true, otherwise need to make them same level.
415 10 : assert(block1.parent_block_index == block2.parent_block_index); // This should be true, otherwise need to make them same level.)
416 :
417 10 : signature_type ds = block1.sig;
418 10 : signature_type dt = block2.sig;
419 :
420 : // Find a distinguishing observation s- tau ->> s' -a-> s''
421 10 : std::tuple<block_index_type, label_type, block_index_type> dist_obs;
422 10 : bool found_obs = false;
423 13 : for (auto path : ds)
424 : {
425 9 : if (!is_tau(std::get<1>(path)) or std::get<0>(path) != std::get<2>(path))
426 : {
427 9 : if (dt.find(path) == dt.end())
428 : {
429 6 : dist_obs = path;
430 6 : found_obs = true;
431 6 : break;
432 : }
433 : }
434 : }
435 : // If no such observation exists, we flip the blocks.
436 10 : if (!found_obs)
437 : {
438 4 : auto phi = mcrl2::state_formulas::not_(dist_formula(block2.block_index, block1.block_index));
439 4 : blockpair2formula[std::make_pair(block1.block_index, block2.block_index)] = phi;
440 : // Compute the truth values \sem{!\phi} = lvl2blocksidx[lvl] - \sem{\phi}
441 4 : std::set_difference(level2blocksidx[block1.level].begin(),
442 4 : level2blocksidx[block1.level].end(),
443 4 : blockpair2truths[std::make_pair(block2.block_index, block1.block_index)].begin(),
444 4 : blockpair2truths[std::make_pair(block2.block_index, block1.block_index)].end(),
445 4 : std::inserter(blockpair2truths[std::make_pair(block1.block_index, block2.block_index)],
446 4 : blockpair2truths[std::make_pair(block1.block_index, block2.block_index)].begin()));
447 4 : return phi;
448 4 : }
449 :
450 :
451 : // We have a distinguishing observation, start constructing the formula.
452 6 : label_type dist_label = std::get<1>(dist_obs);
453 6 : block_index_type B1 = std::get<0>(dist_obs);
454 6 : block_index_type B2 = std::get<2>(dist_obs);
455 : // Log the observation for debugging purposes.
456 6 : std::vector<std::pair<block_index_type, block_index_type>> T;
457 :
458 15 : for (auto path : dt)
459 : {
460 9 : if (std::get<1>(path) == dist_label and (!is_tau(dist_label) or std::get<0>(path) != std::get<2>(path)))
461 : {
462 : // we might have B_1 -\tau -> B_1, I don't think its a problem.
463 4 : T.push_back(std::make_pair(std::get<0>(path), std::get<2>(path)));
464 4 : if (is_tau(dist_label))
465 : {
466 : // the following observation: block2 -\tau->> path2 -(tau)-> path2.
467 4 : T.push_back(std::make_pair(std::get<2>(path), std::get<2>(path)));
468 : }
469 : }
470 : }
471 6 : if (is_tau(dist_label))
472 : {
473 : // the following observation: block2 -\tau->> path2 -(tau)-> path2.
474 2 : T.push_back(std::make_pair(block2.parent_block_index, block2.parent_block_index));
475 : }
476 :
477 : //Keep a copy of T for backwards filtering in postprocessing.
478 6 : std::set<blockpair_type> T_og;
479 16 : for (auto t : T)
480 : {
481 10 : T_og.insert(t);
482 : }
483 :
484 : // TODO: Remove this part and make T a set.
485 : // Sort T, such that the block with the highest distlevel in s'' get dealt with first.
486 : // This is a heuristic, no idea if it improves much or can be improved
487 6 : std::sort(T.begin(), T.end(),
488 92 : [this, B2](std::pair<block_index_type, block_index_type> a, std::pair<block_index_type, block_index_type> b)
489 : {
490 23 : if (a.second == B2) {
491 2 : return false;
492 : }
493 21 : if (b.second == B2)
494 : {
495 9 : return true;
496 : }
497 12 : auto alift = min_split_blockpair(a.second, B2);
498 12 : auto blift = min_split_blockpair(b.second, B2);
499 12 : return blocks[alift.first].level < blocks[blift.first].level;
500 : });
501 :
502 : // <tau*>(<dist_label> phi1 && phi2), We remember the original keys for truth values and backwards filtering.
503 6 : std::map<blockpair_type, mcrl2::state_formulas::state_formula> Phi1;
504 6 : std::map<blockpair_type, mcrl2::state_formulas::state_formula> Phi2;
505 :
506 : // Track truth values for the formula s -\tau -> Truths2 [phi2] -dist_label-> Truths1 [phi1]
507 : // This is a bit confusing, we flip order here in the path to the formula.
508 6 : std::set<block_index_type> Truths1 = level2blocksidx[block1.level - 1];
509 6 : std::set<block_index_type> Truths2 = level2blocksidx[block1.level - 1];
510 :
511 16 : while (!T.empty())
512 : {
513 5 : std::pair<block_index_type, block_index_type> Bt1_Bt2 = T.back();
514 : // We could pop_back here on T, but the computation of the truth also handles this.
515 5 : if (Bt1_Bt2.second != B2)
516 : {
517 4 : std::pair<block_index_type, block_index_type> liftedPair = min_split_blockpair(B2, Bt1_Bt2.second);
518 4 : Phi1[liftedPair] = dist_formula(liftedPair.first, liftedPair.second);
519 : // Update truthvalues for the formula <(dist_label)> phi1.
520 4 : split_and_intersect(Truths1, liftedPair);
521 : }
522 : else
523 : {
524 1 : std::pair<block_index_type, block_index_type> liftedPair = min_split_blockpair(B1, Bt1_Bt2.first);
525 1 : Phi2[liftedPair] = dist_formula(B1, Bt1_Bt2.first);
526 : // Update truthvalues for the formula phi2.
527 1 : split_and_intersect(Truths2, liftedPair);
528 : }
529 : // Remove observations (Bt1, Bt2) from T of which Bt2 is not in phi1 or Bt1 is not in phi2
530 5 : std::vector<std::pair<block_index_type, block_index_type>> T_new;
531 22 : for (auto bt1_bt2 : T)
532 : {
533 : // T_new only consists stuch that both Bt1 and Bt2 are still not distinguished.
534 17 : if (Truths1.find(bt1_bt2.second) != Truths1.end() && Truths2.find(bt1_bt2.first) != Truths2.end())
535 : {
536 7 : T_new.push_back(bt1_bt2);
537 : }
538 : }
539 5 : T = T_new;
540 : }
541 :
542 : // Backwards filtering, remove each formula and see if it is still distinguishing, starting with Phi2.
543 6 : std::set<block_index_type> Tset;
544 : //We assume Phi2.
545 16 : for (auto B_Bp : T_og)
546 : {
547 10 : if (Truths2.find(B_Bp.first) != Truths2.end()) {
548 7 : Tset.insert(B_Bp.second);
549 : }
550 : }
551 :
552 6 : std::vector<mcrl2::state_formulas::state_formula> returnPhi1 = filtered_dist_conjunction(Phi1, Tset, Truths1);
553 :
554 :
555 6 : Tset.clear();
556 : //Now we assume phi1.
557 16 : for (auto B_Bp : T_og)
558 : {
559 10 : if (Truths1.find(B_Bp.second) != Truths1.end()) {
560 2 : Tset.insert(B_Bp.first);
561 : }
562 : }
563 6 : std::vector<mcrl2::state_formulas::state_formula> returnPhi2 = filtered_dist_conjunction(Phi2, Tset, Truths2);
564 :
565 : //Done with formula, set the truth values for the formula.
566 : // Initialize the truth values for the formula
567 6 : blockpair2truths[std::make_pair(block_index1, block_index2)] = std::set<block_index_type>();
568 30 : for (block_index_type b : level2blocksidx[block1.level])
569 : {
570 24 : signature_type sig = blocks[b].sig;
571 46 : for (auto path : sig)
572 : {
573 31 : if (std::get<1>(path) == dist_label)
574 : {
575 15 : block_index_type Bt1 = std::get<0>(path);
576 15 : block_index_type Bt2 = std::get<2>(path);
577 15 : if (Truths1.find(Bt2) != Truths1.end() && Truths2.find(Bt1) != Truths2.end())
578 : {
579 9 : blockpair2truths[std::make_pair(block1.block_index, block2.block_index)].insert(b);
580 9 : break;
581 : }
582 : }
583 : }
584 : }
585 :
586 : // Consruct the regular formula for the diamond operator
587 6 : mcrl2::regular_formulas::regular_formula diamond = create_regular_formula(m_lts.action_label(dist_label));
588 : // If the action is tau, we need to add the tau_hat operator.
589 6 : if (is_tau(dist_label))
590 : {
591 : // we mimic <\hat{tau}> phi := <tau> phi || phi , by <tau+false*> phi.
592 2 : diamond = make_tau_hat(diamond);
593 : }
594 :
595 : // diamond formula <dist_label> phi1
596 12 : mcrl2::state_formulas::state_formula returnPhi = mcrl2::state_formulas::may(diamond , conjunction(returnPhi1));
597 : // diamond formula: <dist_label>phi1 && phi2
598 6 : if (!returnPhi2.empty())
599 : {
600 1 : returnPhi = mcrl2::state_formulas::and_(returnPhi, conjunction(returnPhi2));
601 : }
602 :
603 : // <tau*> (<dist_label> phi1 && phi2)
604 6 : blockpair2formula[std::make_pair(block1.block_index, block2.block_index)]
605 12 : = mcrl2::state_formulas::may(mcrl2::regular_formulas::trans_or_nil(
606 6 : create_regular_formula(m_lts.action_label(0))), returnPhi);
607 6 : return blockpair2formula[std::make_pair(block1.block_index, block2.block_index)];
608 10 : }
609 :
610 : };
611 :
612 : template <class LTS_TYPE>
613 2 : bool destructive_branching_bisimulation_compare_minimal_depth(LTS_TYPE& l1,
614 : LTS_TYPE& l2,
615 : const std::string& counter_example_file)
616 : {
617 2 : std::size_t init_l2 = l2.initial_state() + l1.num_states();
618 2 : mcrl2::lts::detail::merge(l1, l2);
619 2 : l2.clear(); // No use for l2 anymore.
620 :
621 : // First remove tau loops in case of branching bisimulation
622 2 : bool preserve_divergences = false;
623 2 : detail::scc_partitioner<LTS_TYPE> scc_part(l1);
624 2 : init_l2 = scc_part.get_eq_class(init_l2);
625 2 : scc_part.replace_transition_system(preserve_divergences);
626 :
627 : // Run a faster branching bisimulation algorithm as preprocessing, no preversing of loops.
628 2 : detail::bisim_partitioner_dnj branching_bisim_part(l1, true, preserve_divergences);
629 2 : init_l2 = branching_bisim_part.get_eq_class(init_l2);
630 2 : branching_bisim_part.finalize_minimized_LTS();
631 2 : if (branching_bisim_part.in_same_class(l1.initial_state(), init_l2))
632 : {
633 0 : return true;
634 : }
635 :
636 : //Start the new debugging to get minimal depth splitting information.
637 2 : branching_bisim_partitioner_minimal_depth<LTS_TYPE> branching_bisim_min(l1, init_l2);
638 :
639 : //Min-depth partitioner should agree with dnj.
640 2 : assert(!branching_bisim_min.in_same_class(l1.initial_state(), init_l2));
641 :
642 : // LTSs are not bisimilar, we can create a counter example.
643 2 : std::string filename = "Counterexample.mcf";
644 2 : if (!counter_example_file.empty())
645 : {
646 2 : filename = counter_example_file;
647 : }
648 :
649 2 : mcrl2::state_formulas::state_formula counter_example_formula
650 : = branching_bisim_min.dist_formula_mindepth(l1.initial_state(), init_l2);
651 :
652 2 : std::ofstream counter_file(filename);
653 2 : counter_file << mcrl2::state_formulas::pp(counter_example_formula);
654 2 : mCRL2log(mcrl2::log::info) << "Saved counterexample to: \"" << filename << "\"" << std::endl;
655 2 : return false;
656 2 : }
657 :
658 : } // namespace mcrl2::lts::detail
659 : #endif // MCRl2_LTS_LIBLTS_BRANCHING_BISIM_MINIMAL_DEPTH
|
