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