spot 2.12.2
intersect.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) by the Spot authors, see the AUTHORS file for details.
3//
4// This file is part of Spot, a model checking library.
5//
6// Spot is free software; you can redistribute it and/or modify it
7// under the terms of the GNU General Public License as published by
8// the Free Software Foundation; either version 3 of the License, or
9// (at your option) any later version.
10//
11// Spot is distributed in the hope that it will be useful, but WITHOUT
12// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14// License for more details.
15//
16// You should have received a copy of the GNU General Public License
17// along with this program. If not, see <http://www.gnu.org/licenses/>.
18
19#pragma once
20
21#include <spot/kripke/kripke.hh>
22#include <spot/twacube/twacube.hh>
23#include <queue>
24
25namespace spot
26{
32 template<typename SuccIterator, typename State>
33 static void forward_iterators(kripkecube<State, SuccIterator>& sys,
34 twacube_ptr twa,
35 SuccIterator* it_kripke,
36 std::shared_ptr<trans_index> it_prop,
37 bool just_visited,
38 unsigned tid)
39 {
40 (void) sys; // System is useless, but the API is clearer
41 SPOT_ASSERT(!(it_prop->done() && it_kripke->done()));
42
43 // Sometimes kripke state may have no successors.
44 if (it_kripke->done())
45 return;
46
47 // The state has just been visited and the 2 iterators intersect.
48 // There is no need to move iterators forward.
49 SPOT_ASSERT(!(it_prop->done()));
50 if (just_visited && twa->get_cubeset()
51 .intersect(twa->trans_data(it_prop, tid).cube_,
52 it_kripke->condition()))
53 return;
54
55 // Otherwise we have to compute the next valid successor (if it exits).
56 // This requires two loops. The most inner one is for the twacube since
57 // its costless
58 if (it_prop->done())
59 it_prop->reset();
60 else
61 it_prop->next();
62
63 while (!it_kripke->done())
64 {
65 while (!it_prop->done())
66 {
67 if (SPOT_UNLIKELY(twa->get_cubeset()
68 .intersect(twa->trans_data(it_prop, tid).cube_,
69 it_kripke->condition())))
70 return;
71 it_prop->next();
72 }
73 it_prop->reset();
74 it_kripke->next();
75 }
76 }
77}
Definition: automata.hh:26

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.4