changeset 1:f6886b2bda4a

first set of post v7 patches general part of extendTransition optimization, which skips transition breaks (and hence state matching) if vm.extend_transitions is set, and the next CG has only a single choice that does not require a break (e.g. context switch). This is mainly meant to be a state space optimization, and complements the null return on the CG creator side, which is extension/domain specific and also cuts into observability from listeners (no CG - no CG notifications). Note this is only the first part of the patch and probably too general in most cases. The second part extends this with an interface that can control breaks dynamically (e.g. from listeners). Added a ChoiceGenerator.setCurrent() (empty by default) that can be used as a CG type specific hook to expand/modify choices once the CG becomes active Added the first part of the patch that allows SUT context expansion of EventChoiceGenerators, which is required to make the new event system work in situations that need to add additional events based on the current SUT state (e.g. statemachines with timeout events). Fix for INVOKEDYNAMIC causing a NPE for recycled/restored function objects (Nastaran's patch)
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Fri, 23 Jan 2015 11:08:46 -0800
parents 61d41facf527
children b920e6b1be83
files .hgignore src/main/gov/nasa/jpf/jvm/bytecode/INVOKEDYNAMIC.java src/main/gov/nasa/jpf/util/event/ContextEventExpander.java src/main/gov/nasa/jpf/util/event/Event.java src/main/gov/nasa/jpf/util/event/EventChoiceGenerator.java src/main/gov/nasa/jpf/util/event/NoEvent.java src/main/gov/nasa/jpf/util/script/Event.java src/main/gov/nasa/jpf/util/script/StringExpander.java src/main/gov/nasa/jpf/vm/ChoiceGenerator.java src/main/gov/nasa/jpf/vm/ChoiceGeneratorBase.java src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java src/main/gov/nasa/jpf/vm/SystemState.java src/main/gov/nasa/jpf/vm/ThreadInfo.java src/main/gov/nasa/jpf/vm/Verify.java src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_EventProducer.java src/tests/gov/nasa/jpf/test/mc/basic/ExtendTransitionTest.java src/tests/gov/nasa/jpf/test/mc/data/EventGeneratorTest.java
diffstat 17 files changed, 410 insertions(+), 390 deletions(-) [+]
line wrap: on
line diff
--- a/.hgignore	Fri Jan 23 10:14:01 2015 -0800
+++ b/.hgignore	Fri Jan 23 11:08:46 2015 -0800
@@ -9,5 +9,6 @@
 trace
 activity*.png
 *.class
+*.orig
 *~
 *.DS_Store
--- a/src/main/gov/nasa/jpf/jvm/bytecode/INVOKEDYNAMIC.java	Fri Jan 23 10:14:01 2015 -0800
+++ b/src/main/gov/nasa/jpf/jvm/bytecode/INVOKEDYNAMIC.java	Fri Jan 23 11:08:46 2015 -0800
@@ -19,6 +19,7 @@
 
 import gov.nasa.jpf.vm.BootstrapMethodInfo;
 import gov.nasa.jpf.vm.ClassInfo;
+import gov.nasa.jpf.vm.ElementInfo;
 import gov.nasa.jpf.vm.FunctionObjectFactory;
 import gov.nasa.jpf.vm.Instruction;
 import gov.nasa.jpf.vm.LoadOnJPFRequired;
@@ -53,6 +54,8 @@
   
   int funcObjRef = MJIEnv.NULL;
   
+  ElementInfo lastFuncObj = null;
+  
   public INVOKEDYNAMIC () {}
 
   protected INVOKEDYNAMIC (int bmIndex, String methodName, String descriptor){
@@ -90,7 +93,9 @@
   public Instruction execute (ThreadInfo ti) {
     StackFrame frame = ti.getModifiableTopFrame();
     
-    if(funcObjRef == MJIEnv.NULL) {
+    ElementInfo ei = ti.getHeap().get(funcObjRef);
+    
+    if(ei==null || ei!=lastFuncObj) {
       ClassInfo fiClassInfo;
 
       // First, resolve the functional interface
@@ -119,6 +124,7 @@
       Object[] freeVariableValues = frame.getArgumentsValues(ti, freeVariableTypes);
       
       funcObjRef = funcObjFactory.getFunctionObject(ti, fiClassInfo, samUniqueName, bmi, freeVariableTypeNames, freeVariableValues);
+      lastFuncObj = ti.getHeap().get(funcObjRef);
     }
     
     frame.pop(freeVariableTypes.length);
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/util/event/ContextEventExpander.java	Fri Jan 23 11:08:46 2015 -0800
@@ -0,0 +1,29 @@
+/*
+ * Copyright (C) 2015, 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.event;
+
+import java.util.Iterator;
+
+/**
+ * interface that is used to expand events from execution context 
+ */
+public interface ContextEventExpander {
+  
+  Iterator<Event> getEventIterator(Event e);
+}
--- a/src/main/gov/nasa/jpf/util/event/Event.java	Fri Jan 23 10:14:01 2015 -0800
+++ b/src/main/gov/nasa/jpf/util/event/Event.java	Fri Jan 23 11:08:46 2015 -0800
@@ -25,21 +25,22 @@
 import java.util.List;
 
 /**
- * class that represents an external stimulus to the SUT, which is produced by EnvironmentModel instances
+ * class that represents an external stimulus to the SUT, which is produced by EventTree instances
+ * (our environment models)
  * 
- * Note that albeit concrete EnvironmentModels can provide their own, specialized Event types, this class
+ * Note that albeit concrete EventTree can provide their own, specialized Event types, this class
  * is generic enough that we don't declare it as abstract
  */
 public class Event implements Cloneable {
 
   static final Object[] NO_ARGUMENTS = new Object[0];
   
-
   //--- linkage
   protected Event next;
   protected Event prev;
   protected Event alt;
 
+  //--- payload
   protected String name;
   protected Object[] arguments;
   
--- a/src/main/gov/nasa/jpf/util/event/EventChoiceGenerator.java	Fri Jan 23 10:14:01 2015 -0800
+++ b/src/main/gov/nasa/jpf/util/event/EventChoiceGenerator.java	Fri Jan 23 11:08:46 2015 -0800
@@ -19,6 +19,7 @@
 package gov.nasa.jpf.util.event;
 
 import gov.nasa.jpf.vm.ChoiceGeneratorBase;
+import java.util.Iterator;
 
 /**
  * ChoiceGenerator for Events.
@@ -30,15 +31,23 @@
   protected Event cur;
   protected int nProcessed;
   
+  protected ContextEventExpander ctx; // optional, can turn events into iterators based on execution context
+  protected Iterator<Event> curIt;
+  protected Event curItE;
+  
   public EventChoiceGenerator (String id, Event base){
+    this(id, base, null);
+  }
+  
+  public EventChoiceGenerator (String id, Event base, ContextEventExpander ctx) {
     super(id);
-    
     this.base = base;
+    this.ctx = ctx;
   }
   
   public EventChoiceGenerator getSuccessor (String id){
     if (cur == null){
-      return new EventChoiceGenerator(id, base.getNext());
+      return new EventChoiceGenerator(id, base.getNext(), ctx);
       
     } else {
       Event next = cur.getNext();
@@ -50,7 +59,7 @@
       }
       
       if (next != null){
-        return new EventChoiceGenerator( id, next);
+        return new EventChoiceGenerator( id, next, ctx);
       } else {
         return null; // done
       }
@@ -59,16 +68,22 @@
   
   @Override
   public Event getNextChoice () {
+    if (curItE != null){
+      return curItE;
+    }
+    
     return cur;
   }
 
-  @Override
-  public Class<Event> getChoiceType () {
-    return Event.class;
-  }
 
   @Override
   public boolean hasMoreChoices () {
+    if (curIt != null){
+      if (curIt.hasNext()){
+        return true;
+      }
+    }
+    
     if (cur == null){
       return (nProcessed == 0);
     } else {
@@ -78,14 +93,35 @@
 
   @Override
   public void advance () {
-    if (cur == null){
-      if (nProcessed == 0){
-        cur = base;
-        nProcessed = 1;
+    while (true){
+      if (curIt != null){  // do we have a context iterator
+        if (curIt.hasNext()){
+          curItE = curIt.next();
+          nProcessed++;
+          return;
+        } else {  // iterator was processed
+          curIt = null;
+          curItE = null;
+        }
       }
-    } else {
-      cur = cur.getAlt();
-      nProcessed++;
+
+      if (cur == null){
+        if (nProcessed == 0){
+          cur = base;
+          nProcessed = 1;
+        }
+      } else {
+        cur = cur.getAlt();
+        nProcessed++;
+      }
+
+      if (ctx != null && cur != null){
+        curIt = ctx.getEventIterator(cur);
+        if (curIt != null){
+          continue;
+        }
+      }
+      break;
     }
   }
 
@@ -130,4 +166,9 @@
     
     return sb.toString();
   }
+
+  @Override
+  public Class<Event> getChoiceType() {
+    return Event.class;
+  }
 }
--- a/src/main/gov/nasa/jpf/util/event/NoEvent.java	Fri Jan 23 10:14:01 2015 -0800
+++ b/src/main/gov/nasa/jpf/util/event/NoEvent.java	Fri Jan 23 11:08:46 2015 -0800
@@ -23,8 +23,10 @@
  */
 public class NoEvent extends Event {
   
+  public static NoEvent NO_EVENT = new NoEvent();
+  
   public NoEvent (){
-    super("NONE");
+    super("<NONE>");
   } 
   
   @Override
--- a/src/main/gov/nasa/jpf/util/script/Event.java	Fri Jan 23 10:14:01 2015 -0800
+++ b/src/main/gov/nasa/jpf/util/script/Event.java	Fri Jan 23 11:08:46 2015 -0800
@@ -19,6 +19,7 @@
 package gov.nasa.jpf.util.script;
 
 
+import gov.nasa.jpf.util.StringExpander;
 import java.util.ArrayList;
 import java.util.List;
 
@@ -103,7 +104,6 @@
    * this is an interesting little exercise since we have to cover all
    * combinations of parameter values, which would normally be a simple set
    * of nested loops, only that the number of parameters is a variable itself
-   * (I'm notoriously bad at this)
    */
   public List<Event> expand () {
     StringExpander ex = new StringExpander(id);
@@ -190,7 +190,7 @@
     if (c == '"' || c == '\'') { // String literal
       return s.substring(1,s.length()-1);
 
-    } else if (Character.isDigit(c)) { // ints and doubbles
+    } else if (Character.isDigit(c) || c == '-' || c == '+') { // ints and doubles
       if (s.indexOf('.') >=0) {
         return Double.parseDouble(s);
       } else {
--- a/src/main/gov/nasa/jpf/util/script/StringExpander.java	Fri Jan 23 10:14:01 2015 -0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,360 +0,0 @@
-/*
- * 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 java.util.LinkedList;
-import java.util.List;
-
-/**
- * utility class to expand regular expression like strings. We support
- * alternatives "<..|..>" and character categories "[.. X-Z ..]". Alternatives
- * can be nested, char categories can include '-' ranges
- *
- *  e.g. "a<B|X[0-1]Y>z" => aBz, aX0Yz, aX1Yz
- *
- * <2do> this is awfully connected to ESParser - we should really make it more generic
- * (this is the reason why it was moved from the general gov.nasa.jpf.util to
- * this package)
- */
-public class StringExpander {
-
-  public static final char META_CHAR = '`';  // starts a symbol
-
-  public static final char ALT_START_CHAR = '<';
-  public static final char ALT_END_CHAR   = '>';
-  public static final char ALT_CHAR = '|';
-
-  public static final char CAT_START_CHAR = '[';
-  public static final char CAT_END_CHAR = ']';
-  public static final char CAT_CHAR = '-';
-
-  static class Exception extends RuntimeException {
-    Exception(String details){
-      super(details);
-    }
-  }
-
-  static class Token {
-    String value;
-
-    Token (String value){
-      this.value = value;
-    }
-    int length() {
-      return value.length();
-    }
-    boolean isSymbol() {
-      return false;
-    }
-    @Override
-	public String toString(){
-      return value;
-    }
-
-  }
-  static class Symbol extends Token {
-    Symbol (String s){
-      super(s);
-    }
-    @Override
-	boolean isSymbol(){
-      return true;
-    }
-  }
-
-  // our symbol tokens
-  static final Symbol CAT_START = new Symbol("CAT_START");
-  static final Symbol CAT_END = new Symbol("CAT_END");
-
-  static final Symbol ALT_START = new Symbol("ALT_START");
-  static final Symbol ALT_END = new Symbol("ALT_END");
-  static final Symbol ALT = new Symbol("ALT");
-  static final Symbol EOS = new Symbol("END");
-
-  final String src;
-  final int len;
-
-  Token token;
-  int pos;
-
-/**
-    // a quoted symbol char version - doesn't look nice, but is more general
-  void nextToken () {
-
-    int i = pos;
-    int len = this.len;
-
-    if (i>=len){
-      token = EOS;
-
-    } else {
-      if (src.charAt(i) == META_CHAR){  // symbol
-        char c = src.charAt(++i);
-        switch (c){
-          case CAT_START_CHAR:       token = CAT_START; break;
-          case CAT_END_CHAR:         token = CAT_END; break;
-
-          case ALT_START_CHAR:       token = ALT_START; break;
-          case ALT_CHAR:             token = ALT; break;
-          case ALT_END_CHAR:         token = ALT_END; break;
-          default:
-            error("illegal symbol: " + c);
-        }
-        pos += 2;
-
-      } else { // string literal
-        int j = i + 1;
-        for (; j < len && src.charAt(j) != META_CHAR; j++);
-        pos = j;
-        token = new Token(src.substring(i, j));
-      }
-    }
-  }
-**/
-
-  private boolean isMetaChar(char c){
-    return ((c == CAT_START_CHAR) || (c == CAT_END_CHAR) ||
-            (c == ALT_START_CHAR) || (c == ALT_END_CHAR) || (c == ALT_CHAR));
-
-  }
-
-  void nextToken() {
-    int i = pos;
-    int len = this.len;
-
-    if (i>=len){
-      token = EOS;
-
-    } else {
-      char c = src.charAt(i);
-      switch (c){
-        case CAT_START_CHAR:       token = CAT_START;   pos++; break;
-        case CAT_END_CHAR:         token = CAT_END;     pos++; break;
-
-        case ALT_START_CHAR:       token = ALT_START;   pos++; break;
-        case ALT_CHAR:             token = ALT;         pos++; break;
-        case ALT_END_CHAR:         token = ALT_END;     pos++; break;
-
-        default:
-          int j = i + 1;
-          for (; j < len && !isMetaChar(src.charAt(j)); j++);
-          pos = j;
-          token = new Token(src.substring(i, j));
-      }
-    }
-  }
-
-  boolean match (Symbol sym){
-    if (token == sym){
-      nextToken();
-      return true;
-    } else {
-      return false;
-    }
-  }
-
-  public StringExpander (String src){
-    this.src = src;
-    this.len = src.length();
-    this.pos = 0;
-  }
-
-  List<String> addSeq (List<String> list, List<String> seq){
-    List<String> result = new LinkedList<String>();
-
-    if (list != null && list.size() > 0){
-      result.addAll(list);
-    }
-    result.addAll(seq);
-
-    return result;
-  }
-
-  List<String> addLiteral (List<String> list, String s){
-    List<String> result = new LinkedList<String>();
-
-    if (list == null || list.size() == 0){
-      result.add(s);
-
-    } else {
-      for (String e : list) {
-        result.add(e + s);
-      }
-    }
-
-    return result;
-  }
-
-  List<String> addAlt (List<String> list, List<String>alt){
-    List<String> result = new LinkedList<String>();
-
-    if (list == null || list.size() == 0){
-      result.addAll(alt);
-
-    } else {
-      for (String e : list) {
-        for (String p : alt) {
-          result.add(e + p);
-        }
-      }
-    }
-
-    return result;
-  }
-
-  List<String> addCat (List<String> list, char[] cat){
-    List<String> result = new LinkedList<String>();
-
-    if (list == null || list.size() == 0){
-      for (char c : cat){
-        result.add(Character.toString(c));
-      }
-
-    } else {
-      for (String e : list) {
-        for (char c : cat){
-          result.add(e + c);
-        }
-      }
-    }
-
-    return result;
-  }
-
-  void error (String msg){
-    throw new Exception(msg);
-  }
-
-  protected char[] createCategory(String cat){
-    char[] s = cat.toCharArray();
-    int l1 = s.length-1;
-    char[] d = s;
-
-
-    for (int i=0, j=0; i<s.length; i++){
-      char c = s[i];
-      if ((c == CAT_CHAR) && (i>0) && (i<l1)){
-        char c0 = s[i-1];
-        char c1 = s[i+1];
-        int  n = c1 - c0;
-
-        int len = j + n + (s.length-i-2);
-        char[] dNew = new char[len];
-        System.arraycopy(d, 0, dNew, 0, j);
-        d = dNew;
-
-        for (int k=c0+1; k<=c1; k++){
-          d[j++] = (char)k;
-        }
-        i++;
-
-      } else {
-        d[j++] = c;
-      }
-    }
-
-    return d;
-  }
-
-  // seq       :=  {LIT | cat | alt}*
-  // cat       :=  `[ LIT `]
-  // alt       :=  `< spec {`| spec}* `>
-
-  public List<String> expand() {
-    return seq();
-  }
-
-  List<String> seq() {
-    List<String> result = null;
-
-    for (nextToken(); token != EOS; ){
-      if (!token.isSymbol()){
-        result = addLiteral( result,token.value);
-        nextToken();
-
-      } else if (token == ALT_START){
-        result = addAlt( result, alt());
-
-      } else if (token == CAT_START){
-        result = addCat( result, cat());
-
-      } else {
-        break;
-      }
-    }
-
-    return result;
-  }
-
-
-  List<String> alt() {
-    List<String> result = null;
-
-    assert token == ALT_START;
-
-    do {
-      result = addSeq(result, seq());
-    } while (token == ALT);
-
-    if (!match(ALT_END)){
-      error("unterminated alternative");
-    }
-    return result;
-  }
-
-  char[] cat() {
-    char[] set = null;
-
-    assert token == CAT_START;
-
-    nextToken();
-    if (!token.isSymbol()){
-      set = createCategory(token.value);
-      nextToken();
-    }
-
-    if (!match(CAT_END)){
-      error("unterminated category");
-    }
-    return set;
-  }
-
-
-  public static void main (String[] args) {
-    //String a = "<B[0-3]C>";
-    String a = args[0];
-    System.out.println(a);
-    
-    StringExpander ex = new StringExpander(a);
-
-/**
-    for (ex.nextToken(); ex.token != EOS; ex.nextToken()){
-      System.out.println(ex.token);
-    }
-**/
-/**/
-    for (String s : ex.expand()) {
-      System.out.println(s);
-    }
-/**/
-/**
-    System.out.println(new String(ex.createCategory(args[0])));
-**/
-  }
-}
--- a/src/main/gov/nasa/jpf/vm/ChoiceGenerator.java	Fri Jan 23 10:14:01 2015 -0800
+++ b/src/main/gov/nasa/jpf/vm/ChoiceGenerator.java	Fri Jan 23 11:08:46 2015 -0800
@@ -35,6 +35,13 @@
   boolean hasMoreChoices();
 
   /**
+   * to be called before the first advance(). Can be used in implementors to
+   * initialize choices from context (similar to what listeners can do from
+   * choiceGeneratorSet() notifications)
+   */
+  void setCurrent();
+  
+  /**
    * advance to the next choice. This is the only method that really
    * advances our enumeration
    */
--- a/src/main/gov/nasa/jpf/vm/ChoiceGeneratorBase.java	Fri Jan 23 10:14:01 2015 -0800
+++ b/src/main/gov/nasa/jpf/vm/ChoiceGeneratorBase.java	Fri Jan 23 11:08:46 2015 -0800
@@ -308,6 +308,12 @@
     return n;
   }
   
+  @Override
+  public void setCurrent(){
+    // nothing, can be overridden by subclasses to do context specific initialization
+    // the first time this CG becomes the current one
+  }
+  
   // we can't put the advanceForCurrentInsn() here because it has to do
   // notifications, which are the SystemState responsibility
   /**
--- a/src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java	Fri Jan 23 10:14:01 2015 -0800
+++ b/src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java	Fri Jan 23 11:08:46 2015 -0800
@@ -297,6 +297,27 @@
     ti.breakTransition(reason);
   }
 
+  /**
+   * mostly for debugging purposes - this does not optimize away single choice CGs 
+   */
+  @MJI
+  public int breakTransition__Ljava_lang_String_2II__I (MJIEnv env, int clsObjRef, int reasonRef, int min, int max) {
+    ThreadInfo ti = env.getThreadInfo();
+    SystemState ss = env.getSystemState();
+    String reason = env.getStringObject(reasonRef);
+    
+    if (!ti.isFirstStepInsn()) { // first time around
+      IntChoiceGenerator cg = new IntIntervalGenerator( reason, min,max);
+      if (ss.setNextChoiceGenerator(cg)){
+        env.repeatInvocation();
+      }
+      return -1;
+      
+    } else {
+      return getNextChoice(ss, reason, IntChoiceGenerator.class, Integer.class);
+    } 
+  }
+
   @MJI
   public static boolean isCalledFromClass__Ljava_lang_String_2__Z (MJIEnv env, int clsObjRef,
                                            int clsNameRef) {
--- a/src/main/gov/nasa/jpf/vm/SystemState.java	Fri Jan 23 10:14:01 2015 -0800
+++ b/src/main/gov/nasa/jpf/vm/SystemState.java	Fri Jan 23 11:08:46 2015 -0800
@@ -19,6 +19,7 @@
 
 import gov.nasa.jpf.Config;
 import gov.nasa.jpf.JPFException;
+import gov.nasa.jpf.vm.choice.BreakGenerator;
 
 import java.io.PrintWriter;
 import java.util.LinkedHashMap;
@@ -223,6 +224,9 @@
   /** do we want executed insns to be recorded */
   boolean recordSteps;
 
+  /** do we want to extend transitions with non-rescheduling single choices */
+  boolean extendTransitions;
+  
   /**
    * Creates a new system state.
    */
@@ -239,6 +243,7 @@
       maxAllocGC = Integer.MAX_VALUE;
     }
 
+    extendTransitions = config.getBoolean("vm.extend_transitions", false);
     // recordSteps is set later by VM, first we need a reporter (which requires the VM)
   }
 
@@ -344,6 +349,7 @@
     return null;
   }
   
+  
   public <T extends ChoiceGenerator<?>> T[] getChoiceGeneratorsOfType (Class<T> cgType) {
     if (curCg != null){
       return curCg.getAllOfType(cgType);
@@ -363,6 +369,17 @@
     return null;
   }
 
+  public <T> ChoiceGenerator<T> getLastChoiceGeneratorOfChoiceType (String id, Class<T> choiceType){
+    for (ChoiceGenerator<?> cg = curCg; cg != null; cg = cg.getPreviousChoiceGenerator()){
+      if ((id == null || id.equals(cg.getId())) && choiceType.isAssignableFrom(cg.getChoiceType())) {
+        return (ChoiceGenerator<T>)cg;
+      }
+    }
+
+    return null;    
+  }
+
+  
   public <T extends ChoiceGenerator<?>> T getCurrentChoiceGeneratorOfType (Class<T> cgType) {
     for (ChoiceGenerator<?> cg = curCg; cg != null; cg = cg.getCascadedParent()){
       if (cgType.isAssignableFrom(cg.getClass())){
@@ -382,6 +399,16 @@
 
     return null;
   }
+  
+  public <T> ChoiceGenerator<T> getCurrentChoiceGeneratorForChoiceType (String id, Class<T> choiceType){
+    for (ChoiceGenerator<?> cg = curCg; cg != null; cg = cg.getCascadedParent()){
+      if ((id == null || id.equals(cg.getId())) && choiceType.isAssignableFrom(cg.getChoiceType())){
+        return (ChoiceGenerator<T>)cg;
+      }
+    }
+
+    return null;    
+  }
 
 
   public ChoiceGenerator<?> getCurrentChoiceGenerator (String id) {
@@ -703,9 +730,8 @@
       curCg = nextCg;
       nextCg = null;
 
-      // Hmm, that's a bit late (could be in setNextCG), but we keep it here
-      // for the sake of locality, and it's more consistent if it just refers
-      // to curCg, i.e. the CG that is actually going to be used
+      // these are hooks that can be used to do context specific CG initialization
+      curCg.setCurrent();
       notifyChoiceGeneratorSet(vm, curCg);
     }
 
@@ -734,6 +760,40 @@
     execThread.executeTransition(this);    
   }
 
+  /**
+   * check if we can extend the current transition without state storing/matching
+   * This is useful for non-cascaded single choice CGs that do not cause
+   * rescheduling. Such CGs are never backtracked to anyways (they are processed
+   * on their first advance).
+   * 
+   * NOTE: this is on top of CG type specific optimizations that are controlled
+   * by cg.break_single_choice (unset by default). If the respective CG creator
+   * is single choice aware it might not create / register a CG in the first
+   * place and we never get here. This is only called if somebody did create
+   * and register a CG
+   * 
+   * note also that we don't eliminate BreakGenerators since their only purpose
+   * in life is to explicitly cause transition breaks. We don't want to override
+   * the override here.
+   */
+  protected boolean extendTransition (){
+    if (extendTransitions){
+      ChoiceGenerator<?> ncg = nextCg;
+      if (ncg != null && ncg.getTotalNumberOfChoices() == 1 && !ncg.isCascaded()){
+        if (ncg instanceof ThreadChoiceGenerator){
+          if ((ncg instanceof BreakGenerator) || !((ThreadChoiceGenerator)ncg).contains(execThread)){
+            return false;
+          }
+        }
+
+        initializeNextTransition(execThread.getVM());
+        return true;
+      }
+    }
+    
+    return false;
+  }
+  
   protected void setExecThread( VM vm){
     ThreadChoiceGenerator tcg = getCurrentSchedulingPoint();
     if (tcg != null){
@@ -757,11 +817,17 @@
     while (true) {
       if (cg.hasMoreChoices()){
         cg.advance();
-
         isIgnored = false;
         vm.notifyChoiceGeneratorAdvanced(cg);
+        
         if (!isIgnored){
-          nAdvancedCGs++;
+          // this seems redundant, but the CG or the listener might actually skip choices,
+          // in which case we can't execute the next transition.
+          // NOTE - this causes backtracking
+          // <2do> it's debatable if we should treat this as a processed CG
+          if (cg.getNextChoice() != null){
+            nAdvancedCGs++;
+          }
           break;
         }
         
--- a/src/main/gov/nasa/jpf/vm/ThreadInfo.java	Fri Jan 23 10:14:01 2015 -0800
+++ b/src/main/gov/nasa/jpf/vm/ThreadInfo.java	Fri Jan 23 11:08:46 2015 -0800
@@ -1836,6 +1836,49 @@
    * this is the inner interpreter loop of JPF
    */
   protected void executeTransition (SystemState ss) throws JPFException {
+    Instruction pc;
+    outer:
+    while ((pc = getPC()) != null){
+      Instruction nextPc = null;
+
+      currentThread = this;
+      executedInstructions = 0;
+      pendingException = null;
+
+      if (isStopped()){
+        pc = throwStopException();
+        setPC(pc);
+      }
+
+      // this constitutes the main transition loop. It gobbles up
+      // insns until someone registered a ChoiceGenerator, there are no insns left,
+      // the transition was explicitly marked as ignored, or we have reached a
+      // max insn count and preempt the thread upon the next available backjump
+      while (pc != null) {
+        nextPc = executeInstruction();
+
+        if (ss.breakTransition()) {
+          if (ss.extendTransition()){
+            continue outer;
+            
+          } else {
+            if (executedInstructions == 0){ // a CG from a re-executed insn
+              if (isEmptyTransitionEnabled()){ // treat as a new state if empty transitions are enabled
+                ss.setForced(true);
+              }
+            }
+            return;
+          }
+
+        } else {        
+          pc = nextPc;
+        }
+      }
+    }
+  }
+
+  
+  protected void _executeTransition (SystemState ss) throws JPFException {
     Instruction pc = getPC();
     Instruction nextPc = null;
 
--- a/src/main/gov/nasa/jpf/vm/Verify.java	Fri Jan 23 10:14:01 2015 -0800
+++ b/src/main/gov/nasa/jpf/vm/Verify.java	Fri Jan 23 11:08:46 2015 -0800
@@ -262,6 +262,11 @@
 
   public static void breakTransition (String reason) {}
 
+ /** for testing and debugging purposes */
+  public static int breakTransition (String reason, int min, int max) {
+    return -1;
+  }
+
   /**
    * simple debugging aids to imperatively print the current path output of the SUT
    * (to be used with vm.path_output)
--- a/src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_EventProducer.java	Fri Jan 23 10:14:01 2015 -0800
+++ b/src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_EventProducer.java	Fri Jan 23 11:08:46 2015 -0800
@@ -23,6 +23,7 @@
 import gov.nasa.jpf.annotation.MJI;
 import gov.nasa.jpf.util.JPFLogger;
 import gov.nasa.jpf.util.event.CheckEvent;
+import gov.nasa.jpf.util.event.ContextEventExpander;
 import gov.nasa.jpf.util.event.Event;
 import gov.nasa.jpf.util.event.EventChoiceGenerator;
 import gov.nasa.jpf.util.event.EventTree;
@@ -40,9 +41,16 @@
   protected EventTree eventTree;
   protected Event event;
   
+  protected ContextEventExpander eventExpander;  // optional
+  
   public JPF_gov_nasa_jpf_EventProducer (Config config){
     eventTree = config.getEssentialInstance(EventTree.CONFIG_KEY, EventTree.class);
+    eventExpander = config.getInstance("event.expander", ContextEventExpander.class);
+    
     logger.info("event tree generated by: ", eventTree.getClass().getName());
+    if (eventExpander != null){
+      logger.info("using context event expander: ", eventExpander.getClass().getName());
+    }
   }
   
   //--- those can be used by subclasses to add additional processing steps during processNextEvent
@@ -79,7 +87,7 @@
   /**
    * this is our main purpose in life - processing events
    * 
-   * @returns true if there was another event, false if there isn't any event left on this path
+   * @return true if there was another event, false if there isn't any event left on this path
    */
   @MJI
   public boolean processNextEvent____Z (MJIEnv env, int objRef){
@@ -99,7 +107,7 @@
       if (cgPrev != null){
         cg = cgPrev.getSuccessor(CG_NAME);        
       } else {
-        cg = new EventChoiceGenerator( CG_NAME, eventTree.getRoot());
+        cg = new EventChoiceGenerator( CG_NAME, eventTree.getRoot(), eventExpander);
       }
       
       if ((cg = processNextCG(env, objRef, cg)) != null){
@@ -148,7 +156,7 @@
   
   @MJI(noOrphanWarning=true)
   public int getEventName____Ljava_lang_String_2 (MJIEnv env, int objRef){
-    if (event != null){
+    if (event != null && !(event instanceof NoEvent)){
       return env.newString( event.getName());
     } else {
       return MJIEnv.NULL;
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/tests/gov/nasa/jpf/test/mc/basic/ExtendTransitionTest.java	Fri Jan 23 11:08:46 2015 -0800
@@ -0,0 +1,75 @@
+/*
+ * 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.test.mc.basic;
+
+import gov.nasa.jpf.ListenerAdapter;
+import gov.nasa.jpf.util.test.TestJPF;
+import gov.nasa.jpf.vm.ChoiceGenerator;
+import gov.nasa.jpf.vm.Instruction;
+import gov.nasa.jpf.vm.ThreadInfo;
+import gov.nasa.jpf.vm.VM;
+import gov.nasa.jpf.vm.Verify;
+import org.junit.Test;
+
+/**
+ * regression test for extended transitions
+ */
+public class ExtendTransitionTest extends TestJPF {
+  
+  public static class CGListener extends ListenerAdapter {
+    @Override
+    public void choiceGeneratorRegistered (VM vm, ChoiceGenerator<?> nextCG, ThreadInfo currentThread, Instruction executedInstruction) {
+      System.out.println("CG registered: " + nextCG);
+    }
+
+    @Override
+    public void choiceGeneratorSet (VM vm, ChoiceGenerator<?> newCG) {
+      System.out.println("\nCG set: " + newCG + " by: " + newCG.getInsn());
+    }
+
+    @Override
+    public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
+      System.out.println("CG advanced: " + currentCG);
+    }
+
+    @Override
+    public void choiceGeneratorProcessed (VM vm, ChoiceGenerator<?> processedCG) {
+      System.out.println("CG processed: " + processedCG);
+    }  
+  }
+  
+  @Test
+  public void testExtendedStateTransitions(){
+    if (verifyNoPropertyViolation("+vm.extend_transitions=true", "+cg.break_single_choice=false", 
+            "+listener=" + getClass().getName() + "$CGListener")){
+      Verify.print("-- start\n");
+      for (int i=0; i<5; i++){
+        int n = Verify.breakTransition( "loop cycle", i, i);
+        Verify.print("i=", i);
+        Verify.print(", n=", n);
+        Verify.println();
+      }
+    }
+    
+    if (!isJPFRun()){
+      int nStates = VM.getVM().getStateCount();
+      System.out.println("nStates=" + nStates);
+    }
+  }
+}
--- a/src/tests/gov/nasa/jpf/test/mc/data/EventGeneratorTest.java	Fri Jan 23 10:14:01 2015 -0800
+++ b/src/tests/gov/nasa/jpf/test/mc/data/EventGeneratorTest.java	Fri Jan 23 11:08:46 2015 -0800
@@ -19,10 +19,15 @@
 package gov.nasa.jpf.test.mc.data;
 
 import gov.nasa.jpf.EventProducer;
+import gov.nasa.jpf.util.event.ContextEventExpander;
 import gov.nasa.jpf.util.event.Event;
+import gov.nasa.jpf.util.event.NoEvent;
 import gov.nasa.jpf.util.event.TestEventTree;
 import gov.nasa.jpf.util.test.TestJPF;
 import gov.nasa.jpf.vm.Verify;
+import java.util.ArrayList;
+import java.util.Iterator;
+import java.util.List;
 import org.junit.Test;
 
 /**
@@ -97,7 +102,7 @@
       printPaths();
     }
     
-     @Override
+    @Override
     public Event createEventTree() {
        Event[] options = { event("A"), event("B"), event("C") };
 
@@ -117,4 +122,68 @@
     }
   }
   
+  
+  //------------------------------------------------------------------------------------
+  public static class ExpandTree extends TestEventTree {
+    public ExpandTree (){
+      printTree();
+    }
+    
+    @Override
+    public Event createEventTree(){
+      return
+              sequence(
+                event("a"),
+                event("*"),
+                event("<opt>"),
+                event("b"));
+    }    
+  }
+
+  public static class MyEventExpander implements ContextEventExpander {
+    @Override
+    public Iterator<Event> getEventIterator (Event e){
+        String eventName = e.getName();
+      
+        if (eventName.equals("*")){
+          System.out.println("  expanding " + eventName + " to [X,Y]");
+          List<Event> list = new ArrayList<Event>();
+          list.add( new Event("X"));
+          list.add( new Event("Y"));
+          return list.iterator();
+          
+        } else if (eventName.equals("<opt>")){ // that's effectively event removal
+          System.out.println("  expanding " + eventName + " to [NoEvent]");
+          List<Event> list = new ArrayList<Event>();
+          list.add(new NoEvent());
+          return list.iterator();          
+        }
+
+        return null;
+    }
+  }
+
+  //@Test
+  public void testEventExpansion (){
+    if (verifyNoPropertyViolation("+event.class=.test.mc.data.EventGeneratorTest$ExpandTree",
+                                  "+event.expander=.test.mc.data.EventGeneratorTest$MyEventExpander",
+                                  "+log.info=event")){
+      EventProducer producer = new EventProducer();
+      StringBuilder sb = new StringBuilder();
+      
+      while (producer.processNextEvent()){
+        String eventName = producer.getEventName();
+        if (eventName != null){
+          sb.append(eventName);
+        }
+      }
+      
+      String trace = sb.toString();
+      System.out.print("--- got trace: ");
+      System.out.println(trace);
+    }
+  }
+  
+
+  
 }