Mercurial > hg > Members > kono > jpf-core

comparison src/main/gov/nasa/jpf/util/script/EventGeneratorFactory.java @ 0:61d41facf527

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initial v8 import (history reset)
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Fri, 23 Jan 2015 10:14:01 -0800
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:61d41facf527
1 /*
2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
4 * All rights reserved.
5 *
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
8 * in compliance with the License. You may obtain a copy of the License at
9 *
10 * http://www.apache.org/licenses/LICENSE-2.0.
11 *
12 * Unless required by applicable law or agreed to in writing, software
13 * distributed under the License is distributed on an "AS IS" BASIS,
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15 * See the License for the specific language governing permissions and
16 * limitations under the License.
17 */
18
19 package gov.nasa.jpf.util.script;
20
21 import gov.nasa.jpf.Config;
22 import gov.nasa.jpf.ListenerAdapter;
23 import gov.nasa.jpf.search.Search;
24 import gov.nasa.jpf.util.DynamicObjectArray;
25 import gov.nasa.jpf.vm.ChoiceGenerator;
26 import gov.nasa.jpf.vm.SystemState;
27
28 import java.io.PrintWriter;
29 import java.util.ArrayList;
30 import java.util.Iterator;
31 import java.util.LinkedHashMap;
32
33 /**
34 * abstract root for backtrackable event generator factories
35 *
36 * <2do> - we don't support backtracking for sections yet! needs to be implemented for
37 * state charts
38 */
39 public abstract class EventGeneratorFactory extends ListenerAdapter
40 implements ElementProcessor, Iterable<EventGenerator> {
41
42 static final String DEFAULT = "default";
43
44 // helper class to store our internal state. For a simple script based system,
45 // storing the 'cur' index (into the queue) would do, but the queue might have been
46 // generated dynamically, so we need some container to store both
47 static class Memento {
48 ArrayList<EventGenerator> queue;
49 int cur; // cursor into queue
50
51 Memento (EventGeneratorFactory fact) {
52 queue = fact.queue;
53 cur = fact.cur;
54 }
55
56 void restore (EventGeneratorFactory fact) {
57 fact.queue = queue;
58 fact.cur = cur;
59 }
60 }
61
62
63 // <2do> this is lame - if we really want 'instructions' in the queue, rather
64 // than data (== CGs), then we should have a queue of general EventOp entries
65 // this is only used for unbounded REPEATs so far
66 // <2do> the nextCG is currently unconditionally reset in getNextChoiceGenerator()
67 // so we have to make sure we don't jump back if the jump target state was already
68 // visited, which we have to store in the Jump
69 static class Loop extends EventGenerator {
70
71 int startPos, endPos;
72
73 Loop (String id, int startPos, int endPos){
74 super(id);
75
76 this.startPos = startPos;
77 this.endPos = endPos;
78 }
79
80 int getStartPos() {
81 return startPos;
82 }
83
84 //--- those are all dummies - this isn't really a choice
85 @Override
86 public void advance() {}
87
88 @Override
89 public Class getChoiceType() {
90 return null;
91 }
92
93 @Override
94 public Object getNextChoice() {
95 return null;
96 }
97
98 @Override
99 public int getProcessedNumberOfChoices() {
100 return 0;
101 }
102
103 @Override
104 public int getTotalNumberOfChoices() {
105 return 0;
106 }
107
108 @Override
109 public boolean hasMoreChoices() {
110 return false;
111 }
112
113 @Override
114 public ChoiceGenerator randomize() {
115 return null;
116 }
117
118 @Override
119 public void reset() {}
120
121 }
122
123 /** the last returned position in the generator stream */
124 protected int cur;
125
126 /** this is where we store the cur positions for backtracking and restoring states */
127 DynamicObjectArray<Memento> states;
128
129 protected String scriptFileName;
130 protected Script script;
131 protected Config conf;
132
133 protected LinkedHashMap<String,ArrayList<EventGenerator>> sections;
134 protected ArrayList<EventGenerator> queue;
135
136 EventFactory efact;
137
138 protected EventGeneratorFactory () {
139 efact = null;
140 }
141
142 protected EventGeneratorFactory (EventFactory efact) {
143 this.efact = efact;
144 }
145
146 protected void init (String fname) throws ESParser.Exception {
147 cur = 0;
148 states = new DynamicObjectArray<Memento>();
149
150 sections = new LinkedHashMap<String,ArrayList<EventGenerator>>();
151 queue = new ArrayList<EventGenerator>();
152 sections.put(DEFAULT, queue);
153
154 ESParser parser= new ESParser(fname, efact);
155 script = parser.parse();
156 scriptFileName = fname;
157
158 script.process(this);
159 }
160
161 @Override
162 public Iterator<EventGenerator> iterator() {
163 return queue.iterator();
164 }
165
166 protected void addLoop (int startPos) {
167 queue.add( new Loop( "loop", startPos, queue.size()-1));
168 }
169
170 public abstract Class<?> getEventType();
171
172 /**
173 * reset the enumeration state of this factory
174 */
175 public void reset () {
176 cur = 0;
177 }
178
179 public String getScriptFileName() {
180 return scriptFileName;
181 }
182
183 public Script getScript() {
184 return script;
185 }
186
187 public boolean hasSection (String id) {
188 return sections.containsKey(id);
189 }
190
191 public ArrayList<EventGenerator> getSection (String id) {
192 return sections.get(id);
193 }
194
195 public ArrayList<EventGenerator> getDefaultSection () {
196 return sections.get(DEFAULT);
197 }
198
199 protected void setQueue (ArrayList<EventGenerator> q) {
200 if (queue != q) {
201 queue = q;
202 cur = 0;
203 }
204 }
205
206 protected EventGenerator getNextEventGenerator() {
207 EventGenerator cg;
208 int n = queue.size();
209
210 if (n == 0) {
211 return null; // nothing to do
212 }
213
214 if (cur < n) {
215 cg = getQueueItem(cur); // might clone the queue item
216
217 // <2do> - this is a BAD hot fix, but it's going away soon!
218 if (cg instanceof Loop) {
219 int tgtPos = ((Loop)cg).getStartPos();
220 cg = queue.get(tgtPos);
221
222 if (!cg.hasMoreChoices()) {
223 for (int i=tgtPos; i<cur; i++) {
224 queue.get(i).reset();
225 }
226 }
227
228 cur = tgtPos;
229 }
230
231 cg.setId(Integer.toString(cur));
232
233 // might be reused if we re-enter a section sequence or REPEAT body, so we have to reset
234 // <2do> - commenting this out leads to premature state matching on model loops
235 // (will be fixed by the revamped environment modeling)
236 //cg.reset();
237
238 cur++;
239 return cg;
240
241 } else {
242 return null; // nothing left
243 }
244 }
245
246 // we encapsulate this because it might require cloning
247 protected EventGenerator getQueueItem (int i) {
248 return queue.get(i);
249 }
250
251
252 public int getTotalNumberOfEvents() {
253 int total=0;
254 int last = 1;
255
256 for (EventGenerator cg : queue) {
257 int level = cg.getTotalNumberOfChoices() * last;
258 total += level;
259 last = level;
260 }
261
262 return total;
263 }
264
265 public void printOn (PrintWriter pw) {
266 for (EventGenerator eg : queue) {
267 pw.println(eg);
268 }
269 }
270
271 /************************************** SearchListener interface **************/
272 /* we need this after a backtrack and restore to determine the next CG to return
273 */
274
275 @Override
276 public void searchStarted (Search search) {
277 cur = 0;
278 }
279
280 @Override
281 public void stateAdvanced (Search search) {
282 int idx = search.getStateId();
283
284 if (idx >= 0) { // <??> why would it be notified for the init state?
285 Memento m = new Memento(this);
286 states.set(idx, m);
287 }
288 }
289
290 @Override
291 public void stateBacktracked (Search search) {
292 Memento m = states.get(search.getStateId());
293 m.restore(this);
294 // nextCg will be re-computed (->getNext), so there is no need to reset
295 }
296
297 @Override
298 public void stateRestored (Search search) {
299 Memento m = states.get(search.getStateId());
300 m.restore(this);
301
302 // nextCg is restored (not re-computed), so we need to reset
303 SystemState ss = search.getVM().getSystemState();
304 ChoiceGenerator cgNext = ss.getNextChoiceGenerator();
305 cgNext.reset();
306 }
307
308 }