← 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-18 06:46:59 UTC
  • mfrom: (44.1.3 placeBoundStatistics)
  • Revision ID: srba@cs.aau.dk-20140318064659-3klhn3ajw18vhsad
merged in branch adding place-bound statistics

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/Reachability/BreadthFirstReachabilitySearch.cpp
57
57
        
58
58
        if(query->evaluate(*s0, &net)){
59
59
                return ReachabilityResult(ReachabilityResult::Satisfied, "Query was satisfied",
60
 
                                                                  expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), s0->pathLength(), s0->trace());
 
60
                                                                  expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound(), s0->pathLength(), s0->trace());
61
61
        }
62
62
        
63
63
        State* ns = allocator.createState();
89
89
                                        if(query->evaluate(*ns, &net)){
90
90
                                                //ns->dumpTrace(net);
91
91
                                                return ReachabilityResult(ReachabilityResult::Satisfied,
92
 
                                                                                                "A state satisfying the query was found", expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), ns->pathLength(), ns->trace());
 
92
                                                                                                "A state satisfying the query was found", expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound(), ns->pathLength(), ns->trace());
93
93
                                        }
94
94
 
95
95
                                        queue.push_back(ns);
97
97
                                        if(!ns)
98
98
                                                return ReachabilityResult(ReachabilityResult::Unknown,
99
99
                                                                                                   "Memory bound exceeded",
100
 
                                                                                                   expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens());
 
100
                                                                                                   expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound());
101
101
                                }
102
102
                        }
103
103
                }
105
105
        }
106
106
 
107
107
        return ReachabilityResult(ReachabilityResult::NotSatisfied,
108
 
                                                "No state satisfying the query exists.", expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens());
 
108
                                                "No state satisfying the query exists.", expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound());
109
109
}
110
110
 
111
111
}}