--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/util/script/EventGeneratorFactory.java	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,308 @@
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+
+package gov.nasa.jpf.util.script;
+
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.ListenerAdapter;
+import gov.nasa.jpf.search.Search;
+import gov.nasa.jpf.util.DynamicObjectArray;
+import gov.nasa.jpf.vm.ChoiceGenerator;
+import gov.nasa.jpf.vm.SystemState;
+
+import java.io.PrintWriter;
+import java.util.ArrayList;
+import java.util.Iterator;
+import java.util.LinkedHashMap;
+
+/**
+ * abstract root for backtrackable event generator factories
+ *
+ * <2do> - we don't support backtracking for sections yet! needs to be implemented for
+ * state charts
+ */
+public abstract class EventGeneratorFactory extends ListenerAdapter
+                                         implements ElementProcessor, Iterable<EventGenerator> {
+
+  static final String DEFAULT = "default";
+
+  // helper class to store our internal state. For a simple script based system,
+  // storing the 'cur' index (into the queue) would do, but the queue might have been
+  // generated dynamically, so we need some container to store both
+  static class Memento {
+    ArrayList<EventGenerator> queue;
+    int cur; // cursor into queue
+
+    Memento (EventGeneratorFactory fact) {
+      queue = fact.queue;
+      cur = fact.cur;
+    }
+
+    void restore (EventGeneratorFactory fact) {
+      fact.queue = queue;
+      fact.cur = cur;
+    }
+  }
+
+
+  // <2do> this is lame - if we really want 'instructions' in the queue, rather
+  // than data (== CGs), then we should have a queue of general EventOp entries
+  // this is only used for unbounded REPEATs so far
+  // <2do> the nextCG is currently unconditionally reset in getNextChoiceGenerator()
+  // so we have to make sure we don't jump back if the jump target state was already
+  // visited, which we have to store in the Jump
+  static class Loop extends EventGenerator {
+
+    int startPos, endPos;
+
+    Loop (String id, int startPos,  int endPos){
+      super(id);
+      
+      this.startPos = startPos;
+      this.endPos = endPos;
+    }
+
+    int getStartPos() {
+      return startPos;
+    }
+
+    //--- those are all dummies - this isn't really a choice
+    @Override
+	public void advance() {}
+
+    @Override
+	public Class getChoiceType() {
+      return null;
+    }
+
+    @Override
+	public Object getNextChoice() {
+      return null;
+    }
+
+    @Override
+	public int getProcessedNumberOfChoices() {
+      return 0;
+    }
+
+    @Override
+	public int getTotalNumberOfChoices() {
+      return 0;
+    }
+
+    @Override
+	public boolean hasMoreChoices() {
+      return false;
+    }
+
+    @Override
+	public ChoiceGenerator randomize() {
+      return null;
+    }
+
+    @Override
+	public void reset() {}
+
+  }
+
+  /** the last returned position in the generator stream */
+  protected int cur;
+
+  /** this is where we store the cur positions for backtracking and restoring states */
+  DynamicObjectArray<Memento> states;
+
+  protected String scriptFileName;
+  protected Script script;
+  protected Config conf;
+
+  protected LinkedHashMap<String,ArrayList<EventGenerator>> sections;
+  protected ArrayList<EventGenerator> queue;
+
+  EventFactory efact;
+
+  protected EventGeneratorFactory () {
+    efact = null;
+  }
+
+  protected EventGeneratorFactory (EventFactory efact) {
+    this.efact = efact;
+  }
+
+  protected void init (String fname) throws ESParser.Exception {
+    cur = 0;
+    states = new DynamicObjectArray<Memento>();
+
+    sections = new LinkedHashMap<String,ArrayList<EventGenerator>>();
+    queue = new ArrayList<EventGenerator>();
+    sections.put(DEFAULT, queue);
+
+    ESParser parser= new ESParser(fname, efact);
+    script = parser.parse();
+    scriptFileName = fname;
+
+    script.process(this);
+  }
+
+  @Override
+  public Iterator<EventGenerator> iterator() {
+    return queue.iterator();
+  }
+
+  protected void addLoop (int startPos) {
+    queue.add( new Loop( "loop", startPos, queue.size()-1));
+  }
+
+  public abstract Class<?> getEventType();
+
+  /**
+   * reset the enumeration state of this factory
+   */
+  public void reset () {
+    cur = 0;
+  }
+
+  public String getScriptFileName() {
+    return scriptFileName;
+  }
+
+  public Script getScript() {
+    return script;
+  }
+
+  public boolean hasSection (String id) {
+    return sections.containsKey(id);
+  }
+
+  public ArrayList<EventGenerator> getSection (String id) {
+    return sections.get(id);
+  }
+
+  public ArrayList<EventGenerator> getDefaultSection () {
+    return sections.get(DEFAULT);
+  }
+
+  protected void setQueue (ArrayList<EventGenerator> q) {
+    if (queue != q) {
+      queue = q;
+      cur = 0;
+    }
+  }
+
+  protected EventGenerator getNextEventGenerator() {
+    EventGenerator cg;
+    int n = queue.size();
+
+    if (n == 0) {
+      return null; // nothing to do
+    }
+
+    if (cur < n) {
+      cg = getQueueItem(cur); // might clone the queue item
+
+      // <2do> - this is a BAD hot fix, but it's going away soon!
+      if (cg instanceof Loop) {
+        int tgtPos = ((Loop)cg).getStartPos();
+        cg = queue.get(tgtPos);
+
+        if (!cg.hasMoreChoices()) {
+          for (int i=tgtPos; i<cur; i++) {
+            queue.get(i).reset();
+          }
+        }
+
+        cur = tgtPos;
+      }
+
+      cg.setId(Integer.toString(cur));
+
+      // might be reused if we re-enter a section sequence or REPEAT body, so we have to reset
+      // <2do> - commenting this out leads to premature state matching on model loops
+      // (will be fixed by the revamped environment modeling)
+      //cg.reset();
+
+      cur++;
+      return cg;
+
+    } else {
+      return null; // nothing left
+    }
+  }
+
+  // we encapsulate this because it might require cloning
+  protected EventGenerator getQueueItem (int i) {
+    return queue.get(i);
+  }
+
+
+  public int getTotalNumberOfEvents() {
+    int total=0;
+    int last = 1;
+
+    for (EventGenerator cg : queue) {
+       int level = cg.getTotalNumberOfChoices() * last;
+       total += level;
+       last = level;
+    }
+
+    return total;
+  }
+
+  public void printOn (PrintWriter pw) {
+    for (EventGenerator eg : queue) {
+      pw.println(eg);
+    }
+  }
+
+  /************************************** SearchListener interface **************/
+  /* we need this after a backtrack and restore to determine the next CG to return
+   */
+
+  @Override
+  public void searchStarted (Search search) {
+    cur = 0;
+  }
+
+  @Override
+  public void stateAdvanced (Search search) {
+    int idx = search.getStateId();
+
+    if (idx >= 0) { // <??> why would it be notified for the init state?
+      Memento m = new Memento(this);
+      states.set(idx, m);
+    }
+  }
+
+  @Override
+  public void stateBacktracked (Search search) {
+    Memento m = states.get(search.getStateId());
+    m.restore(this);
+    // nextCg will be re-computed (->getNext), so there is no need to reset
+  }
+
+  @Override
+  public void stateRestored (Search search) {
+    Memento m = states.get(search.getStateId());
+    m.restore(this);
+
+    // nextCg is restored (not re-computed), so we need to reset
+    SystemState ss = search.getVM().getSystemState();
+    ChoiceGenerator cgNext = ss.getNextChoiceGenerator();
+    cgNext.reset();
+  }
+
+}