← Back to branch summary

~verifypn-cpn/verifypn/colored

« back to all changes in this revision

Viewing changes to PetriEngine/Reachability/BestFSCooling.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/BestFSCooling.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 "BestFSCooling.h"
 
20
 
 
21
#include "../PQL/PQL.h"
 
22
#include "../PQL/Contexts.h"
 
23
#include "../Structures/PriorityQueue.h"
 
24
#include "../Structures/EnhancedPriorityQueue.h"
 
25
#include "../Structures/StateSet.h"
 
26
#include "../Structures/StateAllocator.h"
 
27
 
 
28
#include <stdio.h>
 
29
#include <string.h>
 
30
#include <math.h>
 
31
 
 
32
using namespace PetriEngine::Structures;
 
33
using namespace PetriEngine::PQL;
 
34
 
 
35
namespace PetriEngine{
 
36
namespace Reachability{
 
37
 
 
38
ReachabilityResult BestFSCooling::reachable(const PetriNet &net,
 
39
                                                                                        const MarkVal *m0,
 
40
                                                                                        const VarVal *v0,
 
41
                                                                                        PQL::Condition *query){
 
42
        StateAllocator<> allocator(net);
 
43
 
 
44
        State* s0 = allocator.createState();
 
45
        memcpy(s0->marking(), m0, sizeof(MarkVal) * net.numberOfPlaces());
 
46
        memcpy(s0->valuation(), v0, sizeof(VarVal) * net.numberOfVariables());
 
47
 
 
48
        if(query->evaluate(*s0))
 
49
                return ReachabilityResult(ReachabilityResult::Satisfied, "Satisfied initially", 0, 0);
 
50
 
 
51
        //Initialize subclasses
 
52
        initialize(query, net);
 
53
 
 
54
        StateSet states(net);
 
55
        _states = &states;
 
56
        states.add(s0);
 
57
        //PriorityQueue<State*> queue;
 
58
        EnhancedPriorityQueue<State*> queue;
 
59
        queue.push(0, s0);
 
60
 
 
61
        //Allocate new state
 
62
        State* ns = allocator.createState();
 
63
        State* ns2 = allocator.createState();
 
64
 
 
65
        int count = 0;
 
66
        BigInt expandedStates = 0;
 
67
        BigInt exploredStates = 0;
 
68
        size_t max = 1;
 
69
        while(!queue.empty()){
 
70
                if(count++ & 1<<17){
 
71
                        count = 0;
 
72
                        if(queue.size() > max)
 
73
                                max = queue.size();
 
74
                        this->reportProgress((double)(max - queue.size()) / ((double)(max)));
 
75
                        if(this->abortRequested())
 
76
                                return ReachabilityResult(ReachabilityResult::Unknown,
 
77
                                                                                  "Query aborted!");
 
78
                }
 
79
 
 
80
                //Take something out of the queue
 
81
                double topP = queue.topPriority();
 
82
                State* s = queue.pop(depthFirst);
 
83
                expandedStates++;
 
84
 
 
85
                int heatFactor = (int)floor(topP / net.numberOfPlaces());
 
86
 
 
87
                // Attempt to fire each transition
 
88
                for(unsigned int t = 0; t < net.numberOfTransitions(); t++){
 
89
                        if(net.fire(t, s->marking(), s->valuation(), ns->marking(), ns->valuation())){
 
90
                                //If it's new
 
91
                                if(states.add(ns)){
 
92
                                        exploredStates++;
 
93
                                        //Set parent and transition for the state
 
94
                                        ns->setParent(s);
 
95
                                        ns->setTransition(t);
 
96
 
 
97
                                        //Test query
 
98
                                        if(query->evaluate(*ns))
 
99
                                                return ReachabilityResult(ReachabilityResult::Satisfied,
 
100
                                                                                                  "Query was satified!",
 
101
                                                                                                  expandedStates,
 
102
                                                                                                  exploredStates,
 
103
                                                                                                  ns->pathLength(),
 
104
                                                                                                  ns->trace());
 
105
 
 
106
                                        // Insert in queue, with given priority
 
107
                                        double bestp = priority(ns, query, net);
 
108
                                        queue.push(bestp, ns);
 
109
 
 
110
                                        //Do the cool step
 
111
                                        if(heatFactor > 1 && net.fire(t, s, ns2, heatFactor)){
 
112
                                                if(states.add(ns2)){
 
113
                                                        ns2->setTransition(t, heatFactor);
 
114
                                                        queue.push(priority(ns2, query, net), ns2);
 
115
                                                        ns2 = allocator.createState();
 
116
                                                }
 
117
                                        }
 
118
 
 
119
 
 
120
                                        //Allocate new stake, as states take ownership
 
121
                                        ns = allocator.createState();
 
122
                                }
 
123
                        }
 
124
                }
 
125
        }
 
126
 
 
127
        return ReachabilityResult(ReachabilityResult::NotSatisfied,
 
128
                                                          "Query cannot be satisfied!", expandedStates, exploredStates);
 
129
}
 
130
 
 
131
double BestFSCooling::priority(const Structures::State *state,
 
132
                                                           const PQL::Condition *query,
 
133
                                                           const PetriNet& net){
 
134
        PQL::DistanceContext context(net,
 
135
                                                                 _distanceStrategy,
 
136
                                                                 state->marking(),
 
137
                                                                 state->valuation(),
 
138
                                                                 _dm);
 
139
        double d = query->distance(context);
 
140
        if(_lookahead > 0){
 
141
                double d2 = lookaheadDistance(net, state, query, _lookahead);
 
142
                d = d < d2 ? d : d2;
 
143
        }
 
144
        return d;
 
145
}
 
146
 
 
147
void BestFSCooling::initialize(const PQL::Condition*,
 
148
                                                           const PetriNet& net){
 
149
        _dm = new Structures::DistanceMatrix(net);
 
150
}
 
151
 
 
152
double BestFSCooling::lookaheadDistance(const PetriNet& net,
 
153
                                                                                const Structures::State* state,
 
154
                                                                                const PQL::Condition* query,
 
155
                                                                                int depth){
 
156
        double min = -1;
 
157
        char d[StateAllocator<>::stateSize(net)];
 
158
        State* ns = (State*)d;
 
159
        StateAllocator<>::initializeState(ns, net);
 
160
        for(unsigned int t = 0; t < net.numberOfTransitions(); t++){
 
161
                if(net.fire(t, state, ns) && !_states->contains(ns)){
 
162
                        PQL::DistanceContext context(net,
 
163
                                                                                 _distanceStrategy,
 
164
                                                                                 ns->marking(),
 
165
                                                                                 ns->valuation(),
 
166
                                                                                 _dm);
 
167
                        double d = query->distance(context);
 
168
                        if(d < min || min == -1)
 
169
                                min = d;
 
170
                        if(depth - 1 > 0)
 
171
                                d = lookaheadDistance(net, ns, query, depth-1);
 
172
                        if(d < min || min == -1)
 
173
                                min = d;
 
174
                }
 
175
        }
 
176
        return min;
 
177
}
 
178
 
 
179
} // Reachability
 
180
} // PetriEngine