--- a/src/main/gov/nasa/jpf/search/heuristic/UserHeuristic.java	Mon Apr 06 12:08:03 2015 -0700
+++ b/src/main/gov/nasa/jpf/search/heuristic/UserHeuristic.java	Fri Apr 10 20:53:11 2015 -0700
@@ -20,41 +20,21 @@
 import gov.nasa.jpf.Config;
 import gov.nasa.jpf.vm.ClassLoaderInfo;
 import gov.nasa.jpf.vm.ElementInfo;
+import gov.nasa.jpf.vm.JPF_gov_nasa_jpf_vm_Verify;
 import gov.nasa.jpf.vm.VM;
 
 
 /**
- * heuristic state prioritizer that uses fields of the Main class under test
- * to determine priorities (i.e. priorities can be set by the program under test)
- *  
- * <2do> pcm - does this still make sense in light of MJI ? If we keep it, this
- * has to be moved to the Verify interface!
+ * heuristic state prioritizer that is controlled by the system under test, which can
+ * use Verify.get/set/resetHeuristicSearchValue() to compute priorities
  */
 public class UserHeuristic extends SimplePriorityHeuristic {
-  static final int defaultValue = 1000;
-
   public UserHeuristic (Config config, VM vm) {
     super(config, vm);
   }
 
   @Override
   protected int computeHeuristicValue () {
-    
-    // <2do> pcm - BAD, this is WAY too hardwired
-    ClassLoaderInfo systemLoader = ClassLoaderInfo.getCurrentSystemClassLoader();
-    ElementInfo ei = systemLoader.getElementInfo("Main");
-    if (ei != null) {
-      // this code is ugly because of the Reference interface
-      ElementInfo b = ei.getObjectField("buffer");
-
-      if (b != null) {
-        int current = b.getIntField("current");
-        int capacity = b.getIntField("capacity");
-
-        return (capacity - current);
-      }
-    }
-
-    return defaultValue;
+    return JPF_gov_nasa_jpf_vm_Verify.heuristicSearchValue;
   }
 }

--- a/src/main/gov/nasa/jpf/util/Loggable.java	Mon Apr 06 12:08:03 2015 -0700
+++ b/src/main/gov/nasa/jpf/util/Loggable.java	Fri Apr 10 20:53:11 2015 -0700
@@ -18,6 +18,8 @@
 
 package gov.nasa.jpf.util;
 
+import java.util.logging.Level;
+
 /**
  * convenience interface that mixes in JPFLogger interface methods
  */
@@ -26,6 +28,10 @@
   // the primitive method used by the defaults
   JPFLogger getLogger();
 
+  default void setLogLevel (Level newLevel){
+    getLogger().setLevel(newLevel);
+  }
+
   default void severe (String msg){
     getLogger().severe(msg);
   }

--- a/src/main/gov/nasa/jpf/util/event/CheckEvent.java	Mon Apr 06 12:08:03 2015 -0700
+++ b/src/main/gov/nasa/jpf/util/event/CheckEvent.java	Fri Apr 10 20:53:11 2015 -0700
@@ -26,31 +26,47 @@
  * This event type uses 'alt' for disjunction and 'next' for conjunction if
  * they point to CheckEvents
  */
-public abstract class CheckEvent extends Event {
+public abstract class CheckEvent extends SystemEvent {
   
   protected CheckEvent (String name, Object... arguments){
     super(name, arguments);
   }
-  
-  public abstract boolean evaluate(MJIEnv env);
-  
-  public boolean check (MJIEnv env){
-    if (!evaluate(env)){
+
+  /**
+   * this is the single check condition for this event
+   */
+  public abstract boolean evaluate(MJIEnv env, int objRef);
+
+  /**
+   * conjunctions and disjunctions of this check event
+   */
+  public boolean check (MJIEnv env, int objRef){
+    if (!evaluate(env, objRef)){
       if (alt != null && alt instanceof CheckEvent){
-        return ((CheckEvent)alt).check(env);
+        return ((CheckEvent)alt).check(env, objRef);
       } else {
         return false;
       }
       
     } else {
       if (next != null && next instanceof CheckEvent){
-        return ((CheckEvent)next).check(env);
+        return ((CheckEvent)next).check(env, objRef);
       } else {
         return true;
       }
     }
   }
-  
+
+  /**
+   * generic check evaluation that throws assertions if failed
+   */
+  @Override
+  public void process (MJIEnv env, int objRef){
+    if (!check(env, objRef)){
+      env.throwAssertion("check event failed: " + this);
+    }
+  }
+
   public CheckEvent or (CheckEvent orCheck){
     addAlternative(orCheck);
     

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/util/event/ControlEvent.java	Fri Apr 10 20:53:11 2015 -0700
@@ -0,0 +1,31 @@
+/*
+ * 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 gov.nasa.jpf.vm.MJIEnv;
+
+/**
+ * pseudo event that is used to control the system under test execution
+ */
+public abstract class ControlEvent extends SystemEvent {
+
+  protected ControlEvent (String name, Object... arguments){
+    super(name, arguments);
+  }
+
+}

--- a/src/main/gov/nasa/jpf/util/event/Event.java	Mon Apr 06 12:08:03 2015 -0700
+++ b/src/main/gov/nasa/jpf/util/event/Event.java	Fri Apr 10 20:53:11 2015 -0700
@@ -247,6 +247,13 @@
   public Object[] getArguments(){
     return arguments;
   }
+
+  public Object getArgument(int idx){
+    if (idx < arguments.length){
+      return arguments[idx];
+    }
+    return null;
+  }
   
   public Event getNext(){
     return next;
@@ -627,10 +634,14 @@
   public boolean isNoEvent(){
     return false;
   }
-    
+
+  public boolean isSystemEvent(){
+    return false;
+  }
+
   //--- generic processing interface
   
-  public void process(){
+  public void process(Object source){
     // can be overridden by subclass if instance has sufficient context info
   }
   

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/util/event/SystemEvent.java	Fri Apr 10 20:53:11 2015 -0700
@@ -0,0 +1,40 @@
+/*
+ * 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 gov.nasa.jpf.vm.MJIEnv;
+
+/**
+ * event type that is not supposed to be handled by the SUT
+ */
+public abstract class SystemEvent extends Event {
+
+  protected SystemEvent (String name, Object... arguments){
+    super(name, arguments);
+  }
+
+  @Override
+  public boolean isSystemEvent(){
+    return true;
+  }
+
+  public void process (MJIEnv env, int objRef){
+    // nothing, optionally overridden by subclass
+  }
+
+}

--- a/src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java	Mon Apr 06 12:08:03 2015 -0700
+++ b/src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java	Fri Apr 10 20:53:11 2015 -0700
@@ -53,7 +53,7 @@
  * its use is supposed to be JPF global (without classloader namespaces)
  */
 public class JPF_gov_nasa_jpf_vm_Verify extends NativePeer {
-  static final int MAX_COUNTERS = 10;
+  static final int MAX_COUNTERS = 127;
 
   static boolean isInitialized;
   
@@ -61,6 +61,7 @@
   static int[] counter;
   static IntTable<String> map;
 
+  public static int heuristicSearchValue;
   
   static boolean supportIgnorePath;
   static boolean breakSingleChoice;
@@ -85,6 +86,8 @@
       breakSingleChoice = conf.getBoolean("cg.break_single_choice");
       enableAtomic = conf.getBoolean("cg.enable_atomic", true);
 
+      heuristicSearchValue = conf.getInt("search.heuristic.default_value");
+
       counter = null;
       map = null;
       
@@ -106,7 +109,7 @@
 
       RunRegistry.getDefaultRegistry().addListener( new RunListener() {
         @Override
-		public void reset (RunRegistry reg){
+		    public void reset (RunRegistry reg){
           isInitialized = false;
         }
       });
@@ -955,7 +958,7 @@
    */
   @MJI
   public static int random__I__I (MJIEnv env, int clsObjRef, int x) {
-   return getInt__II__I( env, clsObjRef, 0, x);
+   return getInt__II__I(env, clsObjRef, 0, x);
   }
 
   static void boring__Z__V (MJIEnv env, int clsObjRef, boolean b) {
@@ -986,6 +989,20 @@
     jpf.getSearch().terminate();
   }
 
+  @MJI public static void setHeuristicSearchValue__I__V (MJIEnv env, int clsObjRef, int val){
+    heuristicSearchValue =  val;
+  }
+
+  @MJI public static int getHeuristicSearchValue____I (MJIEnv env, int clsObjRef){
+    return heuristicSearchValue;
+  }
+
+  @MJI public static void resetHeuristicSearchValue____V (MJIEnv env, int clsObjRef){
+    heuristicSearchValue = config.getInt("search.heuristic.default_value");
+  }
+
+
+
   @MJI
   public static boolean isTraceReplay____Z (MJIEnv env, int clsObjRef) {
     return env.getVM().isTraceReplay();

--- a/src/main/gov/nasa/jpf/vm/MJIEnv.java	Mon Apr 06 12:08:03 2015 -0700
+++ b/src/main/gov/nasa/jpf/vm/MJIEnv.java	Fri Apr 10 20:53:11 2015 -0700
@@ -109,6 +109,10 @@
     heap.gc();
   }
 
+  public void forceState (){
+    getSystemState().setForced(true);
+  }
+
   public void ignoreTransition () {
     getSystemState().setIgnored(true);
   }

--- a/src/main/gov/nasa/jpf/vm/Verify.java	Mon Apr 06 12:08:03 2015 -0700
+++ b/src/main/gov/nasa/jpf/vm/Verify.java	Fri Apr 10 20:53:11 2015 -0700
@@ -535,7 +535,20 @@
   public static void terminateSearch () {
     // native
   }
-  
+
+  public static void setHeuristicSearchValue (int n){
+    // native - to control UserHeuristic
+  }
+
+  public static void resetHeuristicSearchValue (){
+    // native - to control UserHeuristic
+  }
+
+  public static int getHeuristicSearchValue (){
+    // native - to control UserHeuristic
+    return 0;
+  }
+
   public static void setProperties (String... p) {
     // native
   }

--- a/src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_EventProducer.java	Mon Apr 06 12:08:03 2015 -0700
+++ b/src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_EventProducer.java	Fri Apr 10 20:53:11 2015 -0700
@@ -74,7 +74,7 @@
    * evaluate a pseudo event that checks properties 
    */
   protected boolean checkEvent (MJIEnv env, int objRef){
-    return ((CheckEvent)event).check(env);
+    return ((CheckEvent)event).check(env, objRef);
   }
   
   /**