← Back to branch summary

~tapaal-ltl/verifypn/resumable-suc-generator

« back to all changes in this revision

Viewing changes to include/LTL/BuchiSuccessorGenerator.h

  • Committer: Nikolaj Jensen Ulrik
  • Date: 2020-10-05 10:15:17 UTC
  • Revision ID: nikolaj@njulrik.dk-20201005101517-470ai9qv2lukms08
Seemingly working NDFS algorithm

Show diffs side-by-side

added added

removed removed

Lines of Context:
include/LTL/BuchiSuccessorGenerator.h
13
13
 
14
14
#include <spot/twa/twagraph.hh>
15
15
#include <utility>
 
16
#include <memory>
16
17
 
17
18
namespace LTL {
18
19
    class BuchiSuccessorGenerator {
23
24
 
24
25
        void prepare(size_t state) {
25
26
            auto curstate = aut.buchi->state_from_number(state);
26
 
            succ = aut.buchi->succ_iter(curstate);
 
27
            succ = std::unique_ptr<spot::twa_succ_iterator>{aut.buchi->succ_iter(curstate)};
27
28
            succ->first();
28
29
        }
29
30
 
30
31
        bool next(size_t &state, bdd &cond) {
31
32
            if (!succ->done()) {
32
33
                state = aut.buchi->state_number(succ->dst());
 
34
#ifdef PRINTF_DEBUG
 
35
                std::cerr << "buchi state " << state << std::endl;
 
36
#endif
33
37
                cond = succ->cond();
34
38
                succ->next();
35
39
                return true;
51
55
 
52
56
    private:
53
57
        Structures::BuchiAutomaton aut;
54
 
        spot::twa_succ_iterator *succ;
 
58
        std::unique_ptr<spot::twa_succ_iterator> succ;
55
59
    };
56
60
}
57
61
#endif //VERIFYPN_BUCHISUCCESSORGENERATOR_H