changeset 2:b920e6b1be83

second part of the jpf-statechart motivated event interface overhaul, providing dynamic (context specific) expansion of EventTrees from within EventChoiceGenerators. This adds a EventContext mechanism that can replace events on-the-fly during advance() (e.g. expand wildcard patterns) this also included the refined 'vm.extend.transitions' property, which is now a list of TypeSpecs (glob notation plus bounds) for CG types that should be subject to transition extension. We also support CheckExtendTransition attrs for CGs, which can be used to dynamically mark CGs. Note that each matching CG is still tested for non-rescheduling single choices small Type/FeatureSpec extension to make it applicable to java.lang.Class instances. There is no reason why we can't make use of this for native types
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Sat, 24 Jan 2015 18:19:08 -0800
parents f6886b2bda4a
children fdc263e5806b
files src/main/gov/nasa/jpf/util/FeatureSpec.java src/main/gov/nasa/jpf/util/Misc.java src/main/gov/nasa/jpf/util/TypeSpec.java src/main/gov/nasa/jpf/util/TypeSpecMatcher.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/EventContext.java src/main/gov/nasa/jpf/util/event/EventTree.java src/main/gov/nasa/jpf/util/event/NoEvent.java src/main/gov/nasa/jpf/util/event/PropagatingEventContext.java src/main/gov/nasa/jpf/vm/CheckExtendTransition.java src/main/gov/nasa/jpf/vm/SystemState.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 16 files changed, 322 insertions(+), 114 deletions(-) [+]
line wrap: on
line diff
--- a/src/main/gov/nasa/jpf/util/FeatureSpec.java	Fri Jan 23 11:08:46 2015 -0800
+++ b/src/main/gov/nasa/jpf/util/FeatureSpec.java	Sat Jan 24 18:19:08 2015 -0800
@@ -123,6 +123,28 @@
     return matchSuperTypes;
   }
 
+  public boolean isMatchingType (Class cls){
+    if (clsSpec.matches(cls.getName())){
+      return true;
+    }
+    
+    if (matchSuperTypes){
+      for (Class c = cls.getSuperclass(); c != null; c = c.getSuperclass()){
+        if (clsSpec.matches(c.getName())){
+          return true;
+        }
+      }
+    }
+    
+    for (Class ifc : cls.getInterfaces()){
+      if (clsSpec.matches(ifc.getName())) {
+        return true;
+      }      
+    }
+    
+    return false;
+  }
+  
   public boolean isMatchingType(ClassInfo ci){
     if (clsSpec.matches(ci.getName())){  // also takes care of '*'
       return true;
--- a/src/main/gov/nasa/jpf/util/Misc.java	Fri Jan 23 11:08:46 2015 -0800
+++ b/src/main/gov/nasa/jpf/util/Misc.java	Sat Jan 24 18:19:08 2015 -0800
@@ -77,6 +77,18 @@
     }
   };
 
+  @SuppressWarnings("unchecked")
+  public static <B, E extends B> Iterable<B> asBaseIterable (Collection<E> col){
+    Collection<B> base = (Collection)col;
+    return base;
+  }
+
+  @SuppressWarnings("unchecked")
+  public static <B, E extends B> Iterator<B> getBaseIterator (Collection<E> col){
+    Collection<B> base = (Collection)col;
+    return base.iterator();
+  }
+  
   public static <E> void addAll(Collection<E> target, Iterable<? extends E> src) {
     for (E e : src) target.add(e);
   }
--- a/src/main/gov/nasa/jpf/util/TypeSpec.java	Fri Jan 23 11:08:46 2015 -0800
+++ b/src/main/gov/nasa/jpf/util/TypeSpec.java	Sat Jan 24 18:19:08 2015 -0800
@@ -55,11 +55,17 @@
   public boolean matches (Object o){
     if (o instanceof ClassInfo){
       return matches( (ClassInfo) o);
+    } else if (o instanceof Class){
+      return matches( (Class)o);
     } else {
       return false;
     }
   }
   
+  public boolean matches (Class<?> cls){
+    return isMatchingType(cls);
+  }
+  
   public boolean matches (ClassInfo ci){
     return isMatchingType(ci);
   }
--- a/src/main/gov/nasa/jpf/util/TypeSpecMatcher.java	Fri Jan 23 11:08:46 2015 -0800
+++ b/src/main/gov/nasa/jpf/util/TypeSpecMatcher.java	Sat Jan 24 18:19:08 2015 -0800
@@ -43,6 +43,17 @@
     }
   }
   
+  public boolean matches (Class<?> cls){
+    for (int i=0; i<mypeSpecs.length; i++){
+      if (mypeSpecs[i].matches(cls)){
+        return true;
+      }
+    }
+    
+    return false;
+  }
+  
+  
   public boolean matches (ClassInfo ci){
     for (int i=0; i<mypeSpecs.length; i++){
       if (mypeSpecs[i].matches(ci)){
--- a/src/main/gov/nasa/jpf/util/event/ContextEventExpander.java	Fri Jan 23 11:08:46 2015 -0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-/*
- * 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 11:08:46 2015 -0800
+++ b/src/main/gov/nasa/jpf/util/event/Event.java	Sat Jan 24 18:19:08 2015 -0800
@@ -110,7 +110,65 @@
       e.setPrev(prev);
     }
   }
+  
+  public void setLinksFrom (Event other){
+    prev = other.prev;
+    next = other.next;
+    alt = other.alt;
+  }
 
+  public Event replaceWithSequenceFrom (List<Event> list){
+    Event eLast = null;
+    
+    for (Event e: list){
+      if (eLast == null){
+        e.prev = prev;
+        e.alt = alt;
+      } else {
+        e.prev = eLast;
+        eLast.next = e;
+      }
+      
+      eLast = e;
+    }
+    
+    if (eLast != null){
+      eLast.next = next;
+      return list.get(0);
+    } else {
+      return null;
+    }
+  }
+  
+  public Event replaceWithAlternativesFrom (List<Event> list){
+    Event eLast = null;
+    for (Event e: list){
+      e.prev = prev;
+      e.next = next;
+      
+      if (eLast != null){
+        eLast.alt = e;
+      }
+      
+      eLast = e;
+    }
+    
+    if (eLast != null){
+      eLast.alt = alt;
+      return list.get(0);
+    } else {
+      return null;
+    }
+  }
+
+  public Event replaceWith (Event e){
+    e.prev = prev;
+    e.next = next;
+    e.alt = alt;
+    
+    return e;
+  }
+  
   protected void setSource (Object source){
     this.source = source;
   }
@@ -547,4 +605,14 @@
   public boolean isNoEvent(){
     return false;
   }
+    
+  //--- generic processing interface
+  
+  public void process(){
+    // can be overridden by subclass if instance has sufficient context info
+  }
+  
+  public void setProcessed(){
+    // can be overridden by subclass, e.g. to maintain event caches
+  }
 }
--- a/src/main/gov/nasa/jpf/util/event/EventChoiceGenerator.java	Fri Jan 23 11:08:46 2015 -0800
+++ b/src/main/gov/nasa/jpf/util/event/EventChoiceGenerator.java	Sat Jan 24 18:19:08 2015 -0800
@@ -18,8 +18,10 @@
 
 package gov.nasa.jpf.util.event;
 
+import gov.nasa.jpf.util.Predicate;
 import gov.nasa.jpf.vm.ChoiceGeneratorBase;
-import java.util.Iterator;
+import gov.nasa.jpf.vm.SystemState;
+
 
 /**
  * ChoiceGenerator for Events.
@@ -31,21 +33,59 @@
   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;
+  protected EventContext ctx; // optional, can replace/expand events during execution
+  
+  /**
+   * convenience method to get successors from current CG chain 
+   */
+  public static EventChoiceGenerator getNext (SystemState ss, String id, Event base, EventContext ctx){
+    EventChoiceGenerator cgPrev = ss.getLastChoiceGeneratorOfType(EventChoiceGenerator.class);
+    if (cgPrev == null){
+      return new EventChoiceGenerator( id, base, ctx);
+    } else {
+      return cgPrev.getSuccessor(id, ctx);
+    }
+  }
   
   public EventChoiceGenerator (String id, Event base){
     this(id, base, null);
   }
   
-  public EventChoiceGenerator (String id, Event base, ContextEventExpander ctx) {
+  public EventChoiceGenerator (String id, Event base, EventContext ctx) {
     super(id);
     this.base = base;
     this.ctx = ctx;
   }
   
+  public void setContextExpander (EventContext ctx){
+    this.ctx = ctx;
+  }
+  
+  public boolean containsMatchingChoice (Predicate<Event> predicate){
+    for (Event e = base; e != null; e = e.getAlt()){
+      if (predicate.isTrue(e)){
+        return true;
+      }
+    }
+    return false;
+  }
+  
+  public void addChoice (Event newEvent){
+    for (Event e = base; e != null;){
+      Event eAlt = e.getAlt();
+      if (eAlt == null){
+        e.setAlt(newEvent);
+        return;
+      }
+      e = eAlt;
+    }
+  }
+  
   public EventChoiceGenerator getSuccessor (String id){
+    return getSuccessor(id, null);
+  }
+  
+  public EventChoiceGenerator getSuccessor (String id, EventContext ctx){
     if (cur == null){
       return new EventChoiceGenerator(id, base.getNext(), ctx);
       
@@ -68,22 +108,12 @@
   
   @Override
   public Event getNextChoice () {
-    if (curItE != null){
-      return curItE;
-    }
-    
     return cur;
   }
 
 
   @Override
   public boolean hasMoreChoices () {
-    if (curIt != null){
-      if (curIt.hasNext()){
-        return true;
-      }
-    }
-    
     if (cur == null){
       return (nProcessed == 0);
     } else {
@@ -93,35 +123,21 @@
 
   @Override
   public void advance () {
-    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;
-        }
+    if (cur == null){
+      if (nProcessed == 0){
+        cur = base;
+        nProcessed = 1;
       }
-
-      if (cur == null){
-        if (nProcessed == 0){
-          cur = base;
-          nProcessed = 1;
-        }
-      } else {
-        cur = cur.getAlt();
-        nProcessed++;
+    } else {
+      cur = cur.getAlt();
+      nProcessed++;
+    }
+    
+    if (ctx != null){
+      Event newCur = ctx.map(cur);
+      if (newCur != cur){
+        cur = newCur;
       }
-
-      if (ctx != null && cur != null){
-        curIt = ctx.getEventIterator(cur);
-        if (curIt != null){
-          continue;
-        }
-      }
-      break;
     }
   }
 
@@ -145,14 +161,14 @@
   @Override
   public String toString() {
     StringBuilder sb = new StringBuilder(getClass().getName());
-    sb.append("[id=\"");
+    sb.append("{id:\"");
     sb.append(id);
     sb.append('"');
 
-    sb.append(",isCascaded:");
-    sb.append(Boolean.toString(isCascaded));
+    //sb.append(",isCascaded:");
+    //sb.append(Boolean.toString(isCascaded));
 
-    sb.append(",{");
+    sb.append(",[");
     for (Event e=base; e!= null; e = e.getAlt()){
       if (e != base){
         sb.append(',');
@@ -162,7 +178,9 @@
       }
       sb.append(e.toString());
     }
-    sb.append("}]");
+    sb.append("],cur:");
+    sb.append(cur);
+    sb.append("}");
     
     return sb.toString();
   }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/util/event/EventContext.java	Sat Jan 24 18:19:08 2015 -0800
@@ -0,0 +1,26 @@
+/*
+ * 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;
+
+/**
+ * functional interface that is used to expand events from execution context 
+ */
+public interface EventContext {
+  Event map (Event original);
+}
--- a/src/main/gov/nasa/jpf/util/event/EventTree.java	Fri Jan 23 11:08:46 2015 -0800
+++ b/src/main/gov/nasa/jpf/util/event/EventTree.java	Sat Jan 24 18:19:08 2015 -0800
@@ -44,7 +44,7 @@
  */
 public class EventTree extends EventConstructor {
   
-  public static final String CONFIG_KEY = "event.class";
+  public static final String CONFIG_KEY = "event.tree.class";
   
   protected Event root;
 
--- a/src/main/gov/nasa/jpf/util/event/NoEvent.java	Fri Jan 23 11:08:46 2015 -0800
+++ b/src/main/gov/nasa/jpf/util/event/NoEvent.java	Sat Jan 24 18:19:08 2015 -0800
@@ -23,7 +23,8 @@
  */
 public class NoEvent extends Event {
   
-  public static NoEvent NO_EVENT = new NoEvent();
+  // we don't have a singleton since we couldn't detect at compile time if
+  // links are going to be modified
   
   public NoEvent (){
     super("<NONE>");
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/util/event/PropagatingEventContext.java	Sat Jan 24 18:19:08 2015 -0800
@@ -0,0 +1,27 @@
+/*
+ * 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;
+
+/**
+ * an EventContext that is invariant and hence can be automatically
+ * propagated along the path
+ */
+public interface PropagatingEventContext extends EventContext {
+  // no additional methods, just a type
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/vm/CheckExtendTransition.java	Sat Jan 24 18:19:08 2015 -0800
@@ -0,0 +1,36 @@
+/*
+ * 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.vm;
+
+import gov.nasa.jpf.SystemAttribute;
+
+/**
+ * system attribute to dynamically mark ChoiceGenerators for transition extension checks
+ */
+public class CheckExtendTransition implements SystemAttribute {
+  
+  static final CheckExtendTransition singleton = new CheckExtendTransition();
+  
+  public static void mark (ChoiceGenerator<?> cg){
+    cg.addAttr(singleton);
+  }
+  
+  public static boolean isMarked (ChoiceGenerator<?> cg){
+    return (cg != null) && cg.hasAttr(CheckExtendTransition.class);
+  }
+}
--- a/src/main/gov/nasa/jpf/vm/SystemState.java	Fri Jan 23 11:08:46 2015 -0800
+++ b/src/main/gov/nasa/jpf/vm/SystemState.java	Sat Jan 24 18:19:08 2015 -0800
@@ -19,6 +19,7 @@
 
 import gov.nasa.jpf.Config;
 import gov.nasa.jpf.JPFException;
+import gov.nasa.jpf.util.TypeSpecMatcher;
 import gov.nasa.jpf.vm.choice.BreakGenerator;
 
 import java.io.PrintWriter;
@@ -224,8 +225,8 @@
   /** do we want executed insns to be recorded */
   boolean recordSteps;
 
-  /** do we want to extend transitions with non-rescheduling single choices */
-  boolean extendTransitions;
+  /** CG types for which we extend transitions if the CG has only non-rescheduling single choices */
+  TypeSpecMatcher extendTransitions;
   
   /**
    * Creates a new system state.
@@ -243,7 +244,7 @@
       maxAllocGC = Integer.MAX_VALUE;
     }
 
-    extendTransitions = config.getBoolean("vm.extend_transitions", false);
+    extendTransitions = TypeSpecMatcher.create(config.getStringArray("vm.extend_transitions"));
     // recordSteps is set later by VM, first we need a reporter (which requires the VM)
   }
 
@@ -777,17 +778,20 @@
    * 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;
+    ChoiceGenerator<?> ncg = nextCg;
+    if (ncg != null){
+      if (CheckExtendTransition.isMarked(ncg) ||
+              ((extendTransitions != null) && extendTransitions.matches(ncg.getClass()))){
+        if (ncg.getTotalNumberOfChoices() == 1 && !ncg.isCascaded()){
+          if (ncg instanceof ThreadChoiceGenerator){
+            if ((ncg instanceof BreakGenerator) || !((ThreadChoiceGenerator) ncg).contains(execThread)){
+              return false;
+            }
           }
+
+          initializeNextTransition(execThread.getVM());
+          return true;
         }
-
-        initializeNextTransition(execThread.getVM());
-        return true;
       }
     }
     
--- a/src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_EventProducer.java	Fri Jan 23 11:08:46 2015 -0800
+++ b/src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_EventProducer.java	Sat Jan 24 18:19:08 2015 -0800
@@ -23,7 +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.EventContext;
 import gov.nasa.jpf.util.event.Event;
 import gov.nasa.jpf.util.event.EventChoiceGenerator;
 import gov.nasa.jpf.util.event.EventTree;
@@ -41,15 +41,15 @@
   protected EventTree eventTree;
   protected Event event;
   
-  protected ContextEventExpander eventExpander;  // optional
+  protected EventContext ctx;  // optional
   
   public JPF_gov_nasa_jpf_EventProducer (Config config){
     eventTree = config.getEssentialInstance(EventTree.CONFIG_KEY, EventTree.class);
-    eventExpander = config.getInstance("event.expander", ContextEventExpander.class);
+    ctx = config.getInstance("event.context.class", EventContext.class);
     
     logger.info("event tree generated by: ", eventTree.getClass().getName());
-    if (eventExpander != null){
-      logger.info("using context event expander: ", eventExpander.getClass().getName());
+    if (ctx != null){
+      logger.info("using context event: ", ctx.getClass().getName());
     }
   }
   
@@ -105,9 +105,9 @@
     if (!ti.isFirstStepInsn()){      
       EventChoiceGenerator cgPrev = ss.getLastChoiceGeneratorOfType(EventChoiceGenerator.class);
       if (cgPrev != null){
-        cg = cgPrev.getSuccessor(CG_NAME);        
+        cg = cgPrev.getSuccessor(CG_NAME, ctx);        
       } else {
-        cg = new EventChoiceGenerator( CG_NAME, eventTree.getRoot(), eventExpander);
+        cg = new EventChoiceGenerator( CG_NAME, eventTree.getRoot(), ctx);
       }
       
       if ((cg = processNextCG(env, objRef, cg)) != null){
--- a/src/tests/gov/nasa/jpf/test/mc/basic/ExtendTransitionTest.java	Fri Jan 23 11:08:46 2015 -0800
+++ b/src/tests/gov/nasa/jpf/test/mc/basic/ExtendTransitionTest.java	Sat Jan 24 18:19:08 2015 -0800
@@ -19,6 +19,7 @@
 package gov.nasa.jpf.test.mc.basic;
 
 import gov.nasa.jpf.ListenerAdapter;
+import gov.nasa.jpf.search.Search;
 import gov.nasa.jpf.util.test.TestJPF;
 import gov.nasa.jpf.vm.ChoiceGenerator;
 import gov.nasa.jpf.vm.Instruction;
@@ -52,11 +53,16 @@
     public void choiceGeneratorProcessed (VM vm, ChoiceGenerator<?> processedCG) {
       System.out.println("CG processed: " + processedCG);
     }  
+    
+    @Override
+    public void stateAdvanced (Search search){
+      System.out.println("!!! state advanced - this should not happen");
+    }
   }
   
   @Test
   public void testExtendedStateTransitions(){
-    if (verifyNoPropertyViolation("+vm.extend_transitions=true", "+cg.break_single_choice=false", 
+    if (verifyNoPropertyViolation("+vm.extend_transitions=*", "+cg.break_single_choice=false", 
             "+listener=" + getClass().getName() + "$CGListener")){
       Verify.print("-- start\n");
       for (int i=0; i<5; i++){
@@ -70,6 +76,7 @@
     if (!isJPFRun()){
       int nStates = VM.getVM().getStateCount();
       System.out.println("nStates=" + nStates);
+      assertTrue(nStates == 0);
     }
   }
 }
--- a/src/tests/gov/nasa/jpf/test/mc/data/EventGeneratorTest.java	Fri Jan 23 11:08:46 2015 -0800
+++ b/src/tests/gov/nasa/jpf/test/mc/data/EventGeneratorTest.java	Sat Jan 24 18:19:08 2015 -0800
@@ -19,7 +19,7 @@
 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.EventContext;
 import gov.nasa.jpf.util.event.Event;
 import gov.nasa.jpf.util.event.NoEvent;
 import gov.nasa.jpf.util.event.TestEventTree;
@@ -67,7 +67,7 @@
       Verify.resetCounter(0);
     }
     
-    if (verifyNoPropertyViolation("+event.class=.test.mc.data.EventGeneratorTest$SimpleTree", "+log.info=event")){
+    if (verifyNoPropertyViolation("+event.tree.class=.test.mc.data.EventGeneratorTest$SimpleTree", "+log.info=event")){
       EventProducer producer = new EventProducer();
       StringBuilder sb = new StringBuilder();
       
@@ -110,9 +110,9 @@
      }
   }
   
-  //@Test
+  @Test
   public void testAnyCombination (){
-    if (verifyNoPropertyViolation("+event.class=.test.mc.data.EventGeneratorTest$CombinationTree", "+log.info=event")){
+    if (verifyNoPropertyViolation("+event.tree.class=.test.mc.data.EventGeneratorTest$CombinationTree", "+log.info=event")){
       EventProducer producer = new EventProducer();
       StringBuilder sb = new StringBuilder();
       
@@ -140,9 +140,9 @@
     }    
   }
 
-  public static class MyEventExpander implements ContextEventExpander {
+  public static class MyEventContext implements EventContext {
     @Override
-    public Iterator<Event> getEventIterator (Event e){
+    public Event map (Event e){
         String eventName = e.getName();
       
         if (eventName.equals("*")){
@@ -150,23 +150,22 @@
           List<Event> list = new ArrayList<Event>();
           list.add( new Event("X"));
           list.add( new Event("Y"));
-          return list.iterator();
+          return e.replaceWithAlternativesFrom(list);
           
-        } 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();          
+        } else if (eventName.equals("<opt>")){
+          System.out.println("  skipping " + eventName);
+          // that's effectively event removal without changing the structure of the tree
+          return e.replaceWith(new NoEvent()); 
         }
 
-        return null;
+        return e;
     }
   }
 
-  //@Test
+  @Test
   public void testEventExpansion (){
-    if (verifyNoPropertyViolation("+event.class=.test.mc.data.EventGeneratorTest$ExpandTree",
-                                  "+event.expander=.test.mc.data.EventGeneratorTest$MyEventExpander",
+    if (verifyNoPropertyViolation("+event.tree.class=.test.mc.data.EventGeneratorTest$ExpandTree",
+                                  "+event.context.class=.test.mc.data.EventGeneratorTest$MyEventContext",
                                   "+log.info=event")){
       EventProducer producer = new EventProducer();
       StringBuilder sb = new StringBuilder();