22 #include <spot/kripke/kripke.hh>
23 #include <spot/twacube/twacube.hh>
33 template<
typename SuccIterator,
typename State>
34 static void forward_iterators(kripkecube<State, SuccIterator>& sys,
36 SuccIterator* it_kripke,
37 std::shared_ptr<trans_index> it_prop,
42 SPOT_ASSERT(!(it_prop->done() && it_kripke->done()));
45 if (it_kripke->done())
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()))
64 while (!it_kripke->done())
66 while (!it_prop->done())
68 if (SPOT_UNLIKELY(twa->get_cubeset()
69 .intersect(twa->trans_data(it_prop, tid).cube_,
70 it_kripke->condition())))
Definition: automata.hh:27