← Back to branch summary

~verifypn-cpn/verifypn/colored

« back to all changes in this revision

Viewing changes to PetriEngine/Reachability/UltimateSearch.cpp

  • Committer: Jonas Finnemann Jensen
  • Date: 2011-09-15 13:30:00 UTC
  • Revision ID: jopsen@gmail.com-20110915133000-wnywm1odf82emiuw
Import of sources from github

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/Reachability/UltimateSearch.cpp
 
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>,
 
5
 * 
 
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.
 
10
 * 
 
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.
 
15
 * 
 
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/>.
 
18
 */
 
19
#include "UltimateSearch.h"
 
20
 
 
21
#include "../Structures/EnhancedPriorityQueue.h"
 
22
#include "../Structures/StateSet.h"
 
23
#include "../Structures/LimitedStateAllocator.h"
 
24
#include "../PQL/Contexts.h"
 
25
#include "../Structures/DistanceMatrix.h"
 
26
 
 
27
#include <string.h>
 
28
 
 
29
using namespace PetriEngine::Structures;
 
30
using namespace PetriEngine::PQL;
 
31
 
 
32
/** Define memory bound for ultimate search strategy */
 
33
#define ULTIMATE_MEMORY_BOUND                           1024*1024*1024
 
34
 
 
35
namespace PetriEngine{
 
36
namespace Reachability{
 
37
 
 
38
ReachabilityResult UltimateSearch::reachable(const PetriNet &net,
 
39
                                                                                         const MarkVal *m0,
 
40
                                                                                         const VarVal *v0,
 
41
                                                                                         PQL::Condition *query){
 
42
        // Test if it initally satisfied
 
43
        {
 
44
                if(query->evaluate(EvaluationContext(m0, v0)))
 
45
                        return ReachabilityResult(ReachabilityResult::Satisfied, "Satisifed initially", 0, 0, 0);
 
46
        }
 
47
 
 
48
        // Attempt to exclude by over-approx
 
49
        {
 
50
                ConstraintAnalysisContext context(net);
 
51
                query->findConstraints(context);
 
52
                if(context.canAnalyze){
 
53
                        bool isImpossible = true;
 
54
                        for(size_t i = 0; i < context.retval.size(); i++){
 
55
                                isImpossible &= context.retval[i]->isImpossible(net, m0, v0);
 
56
                                if(!isImpossible) break;
 
57
                        }
 
58
                        if(isImpossible)
 
59
                                return ReachabilityResult(ReachabilityResult::NotSatisfied,
 
60
                                                                                  "Excluded by over-approximation",
 
61
                                                                                  0, 0, 0);
 
62
                }
 
63
        }
 
64
 
 
65
        // Create allocator, stateset and queue
 
66
        LimitedStateAllocator<> allocator(net, _memorylimit);
 
67
        StateSet states(net);
 
68
        EnhancedPriorityQueue<State*> queue;
 
69
 
 
70
        // Create s0
 
71
        State s0;
 
72
        s0.setParent(NULL);
 
73
        s0.setTransition(0);
 
74
        s0.setMarking(const_cast<MarkVal*>(m0));
 
75
        s0.setValuation(const_cast<VarVal*>(v0));
 
76
 
 
77
        // Push s0
 
78
        queue.push(1, &s0);
 
79
        states.add(&s0);
 
80
 
 
81
        // Statistics
 
82
        BigInt expanded = 0, explored = 0;
 
83
        size_t max = 1;
 
84
        int count = 0;
 
85
 
 
86
        State* ns = allocator.createState();
 
87
 
 
88
        DistanceContext::DistanceStrategy flags = (DistanceContext::DistanceStrategy)(DistanceContext::AndSum | DistanceContext::OrExtreme);
 
89
 
 
90
        // Main-loop
 
91
        while(!queue.empty()){
 
92
                // Report progress
 
93
                if(count++ & 1<<17){
 
94
                        count = 0;
 
95
                        if(queue.size() > max)
 
96
                                max = queue.size();
 
97
                        this->reportProgress((double)(max - queue.size()) / ((double)(max)));
 
98
                        if(this->abortRequested())
 
99
                                return ReachabilityResult(ReachabilityResult::Unknown,
 
100
                                                                                  "Query aborted!");
 
101
                }
 
102
 
 
103
                // Pop from queue
 
104
                State* s = queue.pop(depthFirst);
 
105
                expanded++;
 
106
 
 
107
                // Try firing each transition
 
108
                for(unsigned int t = 0; t < net.numberOfTransitions(); t++){
 
109
                        if(net.fire(t, s, ns, 1, _kbound) && states.add(ns)){
 
110
                                // Update statistics
 
111
                                explored++;
 
112
                                ns->setParent(s);
 
113
                                ns->setTransition(t);
 
114
 
 
115
                                // Test query
 
116
                                if(query->evaluate(*ns)){
 
117
                                        return ReachabilityResult(ReachabilityResult::Satisfied,
 
118
                                                                                          "Query was satisfied",
 
119
                                                                                          expanded, explored, ns->pathLength(), ns->trace());
 
120
                                }
 
121
 
 
122
                                // Push new state on the queue
 
123
                                DistanceContext context(net,
 
124
                                                                                flags,
 
125
                                                                                ns->marking(),
 
126
                                                                                ns->valuation(),
 
127
                                                                                NULL);
 
128
                                queue.push(query->distance(context), ns);
 
129
 
 
130
                                // Allocate new state, abort if not possible
 
131
                                ns = allocator.createState();
 
132
                                if(!ns)
 
133
                                        return ReachabilityResult(ReachabilityResult::Unknown,
 
134
                                                                                          "Memory bound exceeded",
 
135
                                                                                          expanded, explored);
 
136
                        }
 
137
                }
 
138
        }
 
139
 
 
140
        return ReachabilityResult(ReachabilityResult::NotSatisfied,
 
141
                                                          "Query cannot be satisfied",
 
142
                                                          expanded, explored);
 
143
}
 
144
 
 
145
} // Reachability
 
146
} // PetriEngine
 
147