← Back to branch summary

~verifydtapn-contributers/verifydtapn/safety-games-boostrap

« back to all changes in this revision

Viewing changes to src/DiscreteVerification/VerificationTypes/SafetySynthesis.h

  • Committer: Peter Gjøl Jensen
  • Date: 2016-01-05 21:38:13 UTC
  • Revision ID: peter.gjoel@gmail.com-20160105213813-7cb1mpblhhz14zsk
Bootstrapping 

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/DiscreteVerification/VerificationTypes/SafetySynthesis.h
34
34
    typedef std::forward_list<depender_t> depends_t;
35
35
            
36
36
    enum MarkingState {
37
 
                        UNKNOWN,            // no successors generated yet
38
 
                        PROCESSED,          // Generated successors
39
 
                        MAYBE_WINNING,      // If no env strategy, then winning
40
 
                        LOOSING,            // env wins
41
 
                        WINNING};           // ctrl surely wins
 
37
                        // initial boostrapping calc
 
38
                        BS = 0,
 
39
                        UNKNOWN = 1,            // no successors generated yet
 
40
                        PROCESSED = 2,          // Generated successors
 
41
                        MAYBE_WINNING = 4,      // If no env strategy, then winning
 
42
                        LOOSING = 8,            // env wins
 
43
                        WINNING = 16,           // ctrl surely wins
 
44
    
 
45
                        // go through all
 
46
                        ALL = 32,
 
47
                        UNKNOWN_BS = 33,         // no successors generated yet
 
48
                        PROCESSED_BS = 34,       // Generated successors
 
49
                        MAYBE_WINNING_BS = 36,   // If no env strategy, then winning
 
50
                        LOOSING_BS = 40,         // env wins
 
51
                        WINNING_BS = 48,         // ctrl surely wins   
 
52
                        };                  
42
53
    
43
54
    struct SafetyMeta {
44
 
        MarkingState state;
 
55
        unsigned char state;
45
56
        bool urgent;
46
57
        bool waiting;                       // We only need stuff on waiting once
47
58
        size_t ctrl_children;                // Usefull.
62
73
    size_t discovered;
63
74
    size_t explored;
64
75
    unsigned int largest;
 
76
    MarkingState mode;
65
77
public:
66
78
    SafetySynthesis(
67
79
            TAPN::TimedArcPetriNet& tapn,