Members/kono/jpf-core: src/main/gov/nasa/jpf/search/Search.java annotate

author	Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date	Fri, 23 Jan 2015 10:14:01 -0800
parents
children

rev	line source
0 61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	1 /*
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	2 * Copyright (C) 2014, United States Government, as represented by the
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	3 * Administrator of the National Aeronautics and Space Administration.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	4 * All rights reserved.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	5 *
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	6 * The Java Pathfinder core (jpf-core) platform is licensed under the
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	7 * Apache License, Version 2.0 (the "License"); you may not use this file except
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	8 * in compliance with the License. You may obtain a copy of the License at
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	9 *
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	10 * http://www.apache.org/licenses/LICENSE-2.0.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	11 *
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	12 * Unless required by applicable law or agreed to in writing, software
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	13 * distributed under the License is distributed on an "AS IS" BASIS,
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	15 * See the License for the specific language governing permissions and
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	16 * limitations under the License.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	17 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	18 package gov.nasa.jpf.search;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	19
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	20 import gov.nasa.jpf.Config;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	21 import gov.nasa.jpf.ConfigChangeListener;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	22 import gov.nasa.jpf.Error;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	23 import gov.nasa.jpf.JPF;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	24 import gov.nasa.jpf.JPFException;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	25 import gov.nasa.jpf.JPFListenerException;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	26 import gov.nasa.jpf.Property;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	27 import gov.nasa.jpf.State;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	28 import gov.nasa.jpf.report.Reporter;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	29 import gov.nasa.jpf.util.IntVector;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	30 import gov.nasa.jpf.util.JPFLogger;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	31 import gov.nasa.jpf.util.Misc;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	32 import gov.nasa.jpf.vm.VM;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	33 import gov.nasa.jpf.vm.Path;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	34 import gov.nasa.jpf.vm.ThreadList;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	35 import gov.nasa.jpf.vm.Transition;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	36
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	37 import java.util.ArrayList;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	38 import java.util.List;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	39 import java.util.concurrent.atomic.AtomicBoolean;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	40
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	41 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	42 * the mother of all search classes. Mostly takes care of listeners, keeping
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	43 * track of state attributes and errors. This class mainly keeps the
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	44 * general search info like depth, configured properties etc.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	45 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	46 public abstract class Search {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	47
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	48 protected static JPFLogger log = JPF.getLogger("gov.nasa.jpf.search");
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	49
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	50 /** error encountered during last transition, null otherwise */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	51 protected Error currentError = null;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	52 protected ArrayList<Error> errors = new ArrayList<Error>();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	53
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	54 protected int depth = 0;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	55 protected VM vm;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	56
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	57 protected ArrayList<Property> properties;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	58
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	59 protected boolean matchDepth;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	60 protected long minFreeMemory;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	61 protected int depthLimit;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	62 protected boolean getAllErrors;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	63
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	64 // message explaining the last search constraint hit
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	65 protected String lastSearchConstraint;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	66
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	67 // these states control the search loop
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	68 protected boolean done = false;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	69 protected boolean doBacktrack = false;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	70
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	71 // do we have a probe request
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	72 protected AtomicBoolean notifyProbeListeners = new AtomicBoolean(false);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	73
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	74 /** search listeners. We keep them in a simple array to avoid
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	75 creating objects on each notification */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	76 protected SearchListener[] listeners = new SearchListener[0];
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	77
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	78 /** this is a special SearchListener that is always notified last, so that
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	79 * PublisherExtensions can be sure the notification has been processed by all listeners */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	80 protected Reporter reporter;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	81
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	82 protected final Config config; // to later-on access settings that are only used once (not ideal)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	83
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	84 // don't forget to unregister or we have a HUGE memory leak if the same Config object is
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	85 // reused for several JPF runs
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	86 class ConfigListener implements ConfigChangeListener {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	87
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	88 @Override
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	89 public void propertyChanged(Config config, String key, String oldValue, String newValue) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	90 // Different Config instance
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	91 if (!config.equals(Search.this.config)) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	92 return;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	93 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	94
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	95 // Check if Search configuration changed
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	96 if (key.startsWith("search.")){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	97 String k = key.substring(7);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	98 if ("match_depth".equals(k) \|\|
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	99 "min_free".equals(k) \|\|
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	100 "multiple_errors".equals(k)){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	101 initialize(config);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	102 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	103 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	104 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	105
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	106 @Override
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	107 public void jpfRunTerminated (Config config){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	108 config.removeChangeListener(this);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	109 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	110 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	111
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	112 /** storage to keep track of state depths */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	113 protected final IntVector stateDepth = new IntVector();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	114
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	115 protected Search (Config config, VM vm) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	116 this.vm = vm;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	117 this.config = config;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	118
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	119 initialize( config);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	120
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	121 properties = getProperties(config);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	122 if (properties.isEmpty()) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	123 log.severe("no property");
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	124 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	125
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	126 config.addChangeListener( new ConfigListener());
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	127 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	128
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	129 protected void initialize( Config conf){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	130 depthLimit = conf.getInt("search.depth_limit", Integer.MAX_VALUE);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	131 matchDepth = conf.getBoolean("search.match_depth");
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	132 minFreeMemory = conf.getMemorySize("search.min_free", 1024<<10);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	133 getAllErrors = conf.getBoolean("search.multiple_errors");
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	134 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	135
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	136 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	137 * called after the JPF run is finished. Shouldn't be public, but is called by JPF
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	138 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	139 public void cleanUp(){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	140 // nothing here, the ConfigListener removes itself
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	141 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	142
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	143 public Config getConfig() {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	144 return config;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	145 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	146
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	147 public abstract void search ();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	148
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	149 public void setReporter(Reporter reporter){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	150 this.reporter = reporter;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	151 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	152
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	153 public void addListener (SearchListener newListener) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	154 log.info("SearchListener added: ", newListener);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	155 listeners = Misc.appendElement(listeners, newListener);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	156 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	157
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	158 public boolean hasListenerOfType (Class<?> listenerCls) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	159 return Misc.hasElementOfType(listeners, listenerCls);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	160 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	161
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	162 public <T> T getNextListenerOfType(Class<T> type, T prev){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	163 return Misc.getNextElementOfType(listeners, type, prev);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	164 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	165
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	166
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	167 public void removeListener (SearchListener removeListener) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	168 listeners = Misc.removeElement(listeners, removeListener);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	169 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	170
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	171
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	172 public void addProperty (Property newProperty) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	173 properties.add(newProperty);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	174 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	175
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	176 public void removeProperty (Property oldProperty) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	177 properties.remove(oldProperty);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	178 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	179
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	180 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	181 * return set of configured properties
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	182 * note there is a name clash here - JPF 'properties' have nothing to do with
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	183 * Java properties (java.util.Properties)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	184 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	185 protected ArrayList<Property> getProperties (Config config) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	186 Class<?>[] argTypes = { Config.class, Search.class };
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	187 Object[] args = { config, this };
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	188
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	189 ArrayList<Property> list = config.getInstances("search.properties", Property.class,
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	190 argTypes, args);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	191
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	192 return list;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	193 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	194
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	195 // check for property violation, return true if not done
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	196 protected boolean hasPropertyTermination () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	197 if (currentError != null){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	198 if (done){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	199 return true;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	200 } else { // we search for multiple errors, so we ignore and go on
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	201 doBacktrack = true;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	202 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	203 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	204
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	205 return false;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	206 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	207
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	208 // this should only be called once per transition, otherwise it keeps adding the same error
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	209 protected boolean checkPropertyViolation () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	210 for (Property p : properties) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	211 if (!p.check(this, vm)) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	212 error(p, vm.getClonedPath(), vm.getThreadList());
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	213 return true;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	214 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	215 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	216
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	217 return false;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	218 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	219
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	220 public List<Error> getErrors () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	221 return errors;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	222 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	223
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	224 public int getNumberOfErrors(){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	225 return errors.size();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	226 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	227
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	228 public String getLastSearchConstraint() {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	229 return lastSearchConstraint;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	230 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	231
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	232 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	233 * request a probe
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	234 *
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	235 * This does not do the actual listener notification, it only stores
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	236 * the request, which is then processed from within JPFs inner execution loop.
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	237 * As a consequence, probeSearch() can be called async, and searchProbed() listeners
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	238 * don't have to bother with synchronization or inconsistent JPF states (notification
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	239 * happens from within JPFs main thread after a completed Instruction execution)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	240 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	241 public void probeSearch(){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	242 notifyProbeListeners.set(true);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	243 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	244
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	245 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	246 * this does the actual notification and resets the request, hence this call
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	247 * should only happen from within JPFs main thread
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	248 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	249 public void checkAndResetProbeRequest(){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	250 if (notifyProbeListeners.compareAndSet(true, false)){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	251 notifySearchProbed();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	252 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	253 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	254
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	255 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	256 * @return error encountered during last transition (null otherwise)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	257 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	258 public Error getCurrentError(){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	259 return currentError;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	260 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	261
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	262 public Error getLastError() {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	263 int i=errors.size()-1;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	264 if (i >=0) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	265 return errors.get(i);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	266 } else {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	267 return null;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	268 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	269 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	270
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	271 public boolean hasErrors(){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	272 return !errors.isEmpty();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	273 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	274
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	275 public VM getVM() {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	276 return vm;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	277 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	278
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	279 public boolean isEndState () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	280 return vm.isEndState();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	281 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	282
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	283 public boolean isErrorState(){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	284 return (currentError != null);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	285 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	286
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	287 public boolean hasNextState () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	288 return !isEndState();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	289 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	290
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	291 public boolean transitionOccurred(){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	292 return vm.transitionOccurred();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	293 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	294
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	295 public boolean isNewState () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	296 boolean isNew = vm.isNewState();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	297
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	298 if (matchDepth) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	299 int id = vm.getStateId();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	300
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	301 if (isNew) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	302 setStateDepth(id, depth);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	303 } else {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	304 return depth < getStateDepth(id);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	305 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	306 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	307
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	308 return isNew;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	309 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	310
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	311 public boolean isVisitedState () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	312 return !isNewState();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	313 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	314
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	315 public boolean isIgnoredState(){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	316 return vm.isIgnoredState();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	317 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	318
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	319 public boolean isProcessedState(){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	320 return vm.getChoiceGenerator().isProcessed();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	321 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	322
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	323 public boolean isDone(){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	324 return done;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	325 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	326
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	327 public int getDepth () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	328 return depth;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	329 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	330
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	331 public String getSearchConstraint () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	332 return lastSearchConstraint;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	333 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	334
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	335 public Transition getTransition () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	336 return vm.getLastTransition();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	337 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	338
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	339 public int getStateId () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	340 return vm.getStateId();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	341 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	342
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	343 public int getPurgedStateId () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	344 return -1; // a lot of Searches don't purge any states
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	345 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	346
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	347
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	348 /**
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	349 * this is somewhat redundant to SystemState.setIgnored(), but we don't
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	350 * want to mix the case of overriding state matching with backtracking when
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	351 * searching for multiple errors
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	352 */
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	353 public boolean requestBacktrack () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	354 return doBacktrack = true;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	355 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	356
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	357
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	358 protected boolean checkAndResetBacktrackRequest() {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	359 if (doBacktrack){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	360 doBacktrack = false;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	361 return true;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	362 } else {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	363 return false;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	364 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	365 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	366
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	367 public boolean supportsBacktrack () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	368 return true;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	369 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	370
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	371 public boolean supportsRestoreState () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	372 // not supported by default
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	373 return false;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	374 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	375
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	376 public int getDepthLimit () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	377 return depthLimit;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	378 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	379
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	380 public void setDepthLimit(int limit){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	381 depthLimit = limit;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	382 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	383
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	384 protected SearchState getSearchState () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	385 return new SearchState(this);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	386 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	387
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	388 // can be used by SearchListeners to create path-less errors (liveness)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	389 public void error (Property property) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	390 error(property, null, null);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	391 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	392
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	393 public void error (Property property, Path path, ThreadList threadList) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	394
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	395 if (getAllErrors) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	396 // otherwise we are going to overwrite it if we go on
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	397 try {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	398 property = property.clone();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	399 path = path.clone();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	400 threadList = (ThreadList) threadList.clone(); // this makes it a snapshot (deep) clone
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	401 } catch (CloneNotSupportedException cnsx){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	402 throw new JPFException("failed to clone error information: " + cnsx);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	403 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	404 done = false;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	405
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	406 } else {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	407 done = true;
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	408 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	409
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	410 currentError = new Error(errors.size()+1, property, path, threadList);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	411
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	412 errors.add(currentError);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	413
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	414 // we should not reset the property until listeners have been notified
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	415 // (the listener might be the property itself, in which case it could get
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	416 // confused if propertyViolated() notifications happen after a reset)
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	417 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	418
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	419 public void resetProperties(){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	420 for (Property p : properties) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	421 p.reset();
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	422 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	423 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	424
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	425 protected void notifyStateAdvanced () {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	426 try {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	427 for (int i = 0; i < listeners.length; i++) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	428 listeners[i].stateAdvanced(this);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	429 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	430 if (reporter != null){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	431 // reporter always comes last to ensure all listeners have been notified
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	432 reporter.stateAdvanced(this);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	433 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	434 } catch (Throwable t) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	435 throw new JPFListenerException("exception during stateAdvanced() notification", t);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	436 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	437 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	438
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	439 protected void notifyStateProcessed() {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	440 try {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	441 for (int i = 0; i < listeners.length; i++) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	442 listeners[i].stateProcessed(this);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	443 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	444 if (reporter != null){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	445 reporter.stateProcessed(this);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	446 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	447 } catch (Throwable t) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	448 throw new JPFListenerException("exception during stateProcessed() notification", t);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	449 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	450 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	451
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	452 protected void notifyStateStored() {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	453 try {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	454 for (int i = 0; i < listeners.length; i++) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	455 listeners[i].stateStored(this);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	456 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	457 if (reporter != null){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	458 reporter.stateStored(this);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	459 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	460 } catch (Throwable t) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	461 throw new JPFListenerException("exception during stateStored() notification", t);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	462 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	463 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	464
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	465 protected void notifyStateRestored() {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	466 try {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	467 for (int i = 0; i < listeners.length; i++) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	468 listeners[i].stateRestored(this);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	469 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	470 if (reporter != null){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	471 reporter.stateRestored(this);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	472 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	473 } catch (Throwable t) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	474 throw new JPFListenerException("exception during stateRestored() notification", t);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	475 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	476 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	477
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	478 protected void notifyStateBacktracked() {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	479 try {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	480 for (int i = 0; i < listeners.length; i++) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	481 listeners[i].stateBacktracked(this);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	482 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	483 if (reporter != null){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	484 reporter.stateBacktracked(this);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	485 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	486 } catch (Throwable t) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	487 throw new JPFListenerException("exception during stateBacktracked() notification", t);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	488 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	489 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	490
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	491 protected void notifyStatePurged() {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	492 try {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	493 for (int i = 0; i < listeners.length; i++) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	494 listeners[i].statePurged(this);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	495 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	496 if (reporter != null){
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	497 reporter.statePurged(this);
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	498 }
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	499 } catch (Throwable t) {
61d41facf527 initial v8 import (history reset) Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> parents: diff changeset	500 throw new JPFListenerException("exception during statePurged() notification", t);

0

61d41facf527 initial v8 import (history reset)