← Back to branch summary

~tapaal-dist/verifypn/LTSmin

« back to all changes in this revision

Viewing changes to PetriEngine/Reachability/BreadthFirstReachabilitySearch.cpp

  • Committer: Jiri Srba
  • Date: 2014-03-12 07:47:26 UTC
  • mfrom: (43.1.5 statistics)
  • Revision ID: srba@cs.aau.dk-20140312074726-1jjxr63r0ial6umm
merged in branch adding transition statistics to the output of the engine

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/Reachability/BreadthFirstReachabilitySearch.cpp
53
53
        int count = 0;
54
54
        BigInt expandedStates = 0;
55
55
        BigInt exploredStates = 1;
 
56
        std::vector<BigInt> enabledTransitionsCount (net.numberOfTransitions());
56
57
        
57
58
        if(query->evaluate(*s0, &net)){
58
59
                return ReachabilityResult(ReachabilityResult::Satisfied, "Query was satisfied",
59
 
                                                                  expandedStates, exploredStates, states.discovered(), states.maxTokens(), s0->pathLength(), s0->trace());
 
60
                                                                  expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), s0->pathLength(), s0->trace());
60
61
        }
61
62
        
62
63
        State* ns = allocator.createState();
80
81
                queue.pop_front();
81
82
                for(unsigned int t = 0; t < net.numberOfTransitions(); t++){
82
83
                        if(net.fire(t, s, ns, 1)){
 
84
                                enabledTransitionsCount[t]++;
83
85
                                if(states.add(ns)){
84
86
                                        exploredStates++;
85
87
                                        ns->setParent(s);
87
89
                                        if(query->evaluate(*ns, &net)){
88
90
                                                //ns->dumpTrace(net);
89
91
                                                return ReachabilityResult(ReachabilityResult::Satisfied,
90
 
                                                                                                "A state satisfying the query was found", expandedStates, exploredStates, states.discovered(), states.maxTokens(), ns->pathLength(), ns->trace());
 
92
                                                                                                "A state satisfying the query was found", expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), ns->pathLength(), ns->trace());
91
93
                                        }
92
94
 
93
95
                                        queue.push_back(ns);
95
97
                                        if(!ns)
96
98
                                                return ReachabilityResult(ReachabilityResult::Unknown,
97
99
                                                                                                   "Memory bound exceeded",
98
 
                                                                                                   expandedStates, exploredStates, states.discovered(), states.maxTokens());
 
100
                                                                                                   expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens());
99
101
                                }
100
102
                        }
101
103
                }
103
105
        }
104
106
 
105
107
        return ReachabilityResult(ReachabilityResult::NotSatisfied,
106
 
                                                "No state satisfying the query exists.", expandedStates, exploredStates, states.discovered(), states.maxTokens());
 
108
                                                "No state satisfying the query exists.", expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens());
107
109
}
108
110
 
109
111
}}