1
/* PeTe - Petri Engine exTremE
2
* Copyright (C) 2011 Jonas Finnemann Jensen <jopsen@gmail.com>,
3
* Thomas Søndersø Nielsen <primogens@gmail.com>,
4
* Lars Kærlund Østergaard <larsko@gmail.com>,
6
* This program is free software: you can redistribute it and/or modify
7
* it under the terms of the GNU General Public License as published by
8
* the Free Software Foundation, either version 3 of the License, or
9
* (at your option) any later version.
11
* This program is distributed in the hope that it will be useful,
12
* but WITHOUT ANY WARRANTY; without even the implied warranty of
13
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
14
* GNU General Public License for more details.
16
* You should have received a copy of the GNU General Public License
17
* along with this program. If not, see <http://www.gnu.org/licenses/>.
19
#include "StateSearch.h"
21
#include "../Structures/EnhancedPriorityQueue.h"
22
#include "../Structures/StateSet.h"
23
#include "../Structures/BoundedStateAllocator.h"
24
#include "../PQL/Contexts.h"
25
#include "../Structures/DistanceMatrix.h"
30
using namespace PetriEngine::Structures;
31
using namespace PetriEngine::PQL;
33
/** Define memory bound for ultimate search strategy */
34
#define ULTIMATE_MEMORY_BOUND 1024*1024*1024
36
namespace PetriEngine{
37
namespace Reachability{
39
ReachabilityResult StateSearch::reachable(const PetriNet &net,
42
PQL::Condition *query){
43
// Test if it initally satisfied
45
if(query->evaluate(EvaluationContext(m0, v0)))
46
return ReachabilityResult(ReachabilityResult::Satisfied, "Satisifed initially", 0, 0, 0);
49
// Attempt to exclude by over-approx
50
ConstraintAnalysisContext context(net);
51
query->findConstraints(context);
52
if(!context.canAnalyze)
53
return ReachabilityResult(ReachabilityResult::Unknown,
56
bool isImpossible = true;
57
for(size_t i = 0; i < context.retval.size(); i++){
58
isImpossible &= context.retval[i]->isImpossible(net, m0, v0);
59
if(!isImpossible) break;
62
return ReachabilityResult(ReachabilityResult::NotSatisfied,
63
"Excluded by over-approximation",
67
// Create allocator, stateset and queue
68
BoundedStateAllocator<ULTIMATE_MEMORY_BOUND> allocator(net);
70
EnhancedPriorityQueue<State*> queue;
76
s0.setMarking(const_cast<MarkVal*>(m0));
77
s0.setValuation(const_cast<VarVal*>(v0));
84
BigInt expanded = 0, explored = 0;
88
State* ns = allocator.createState();
91
while(!queue.empty()){
95
if(queue.size() > max)
97
this->reportProgress((double)(max - queue.size()) / ((double)(max)));
98
if(this->abortRequested())
99
return ReachabilityResult(ReachabilityResult::Unknown,
104
State* s = queue.pop(depthFirst);
107
// Try firing each transition
108
for(unsigned int t = 0; t < net.numberOfTransitions(); t++){
109
if(net.fire(t, s, ns) && states.add(ns)){
113
ns->setTransition(t);
116
if(query->evaluate(*ns)){
117
return ReachabilityResult(ReachabilityResult::Satisfied,
118
"Query was satisfied",
119
expanded, explored, ns->pathLength(), ns->trace());
122
bool isImpossible = true;
123
int smallest = INT_MAX;
124
for(size_t i = 0; i < context.retval.size(); i++){
125
int size = context.retval[i]->fireVectorSize(net, m0, v0);
127
isImpossible = false;
132
return ReachabilityResult(ReachabilityResult::NotSatisfied,
133
"Excluded by over-approximation",
135
queue.push(smallest, ns);
137
// Allocate new state, abort if not possible
138
ns = allocator.createState();
140
return ReachabilityResult(ReachabilityResult::Unknown,
141
"Memory bound exceeded",
147
return ReachabilityResult(ReachabilityResult::NotSatisfied,
148
"Query cannot be satisfied",