21#include <spot/kripke/kripke.hh>
22#include <spot/twacube/twacube.hh>
32 template<
typename SuccIterator,
typename State>
33 static void forward_iterators(kripkecube<State, SuccIterator>& sys,
35 SuccIterator* it_kripke,
36 std::shared_ptr<trans_index> it_prop,
41 SPOT_ASSERT(!(it_prop->done() && it_kripke->done()));
44 if (it_kripke->done())
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()))
63 while (!it_kripke->done())
65 while (!it_prop->done())
67 if (SPOT_UNLIKELY(twa->get_cubeset()
68 .intersect(twa->trans_data(it_prop, tid).cube_,
69 it_kripke->condition())))
Definition: automata.hh:26