2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
8 * in compliance with the License. You may obtain a copy of the License at
10 * http://www.apache.org/licenses/LICENSE-2.0.
12 * Unless required by applicable law or agreed to in writing, software
13 * distributed under the License is distributed on an "AS IS" BASIS,
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15 * See the License for the specific language governing permissions and
16 * limitations under the License.
19 package gov.nasa.jpf.util.event;
21 import gov.nasa.jpf.util.Misc;
22 import gov.nasa.jpf.util.OATHash;
23 import java.io.PrintStream;
24 import java.util.ArrayList;
25 import java.util.List;
28 * class that represents an external stimulus to the SUT, which is produced by EventTree instances
29 * (our environment models)
31 * Note that albeit concrete EventTree can provide their own, specialized Event types, this class
32 * is generic enough that we don't declare it as abstract
34 public class Event implements Cloneable {
36 static final Object[] NO_ARGUMENTS = new Object[0];
44 protected String name;
45 protected Object[] arguments;
47 protected Object source; // optional, set on demand to keep track of where an event came from
49 public Event (String name){
50 this( name, NO_ARGUMENTS, null);
53 public Event (String name, Object source){
54 this( name, NO_ARGUMENTS, source);
57 public Event(String name, Object[] arguments) {
58 this(name, arguments, null);
61 public Event(String name, Object[] arguments, Object source) {
63 this.arguments = arguments != null ? arguments : NO_ARGUMENTS;
70 public boolean equals (Object o){
71 if (o instanceof Event){
72 Event other = (Event)o;
74 if (name.equals(other.name)){
75 return Misc.equals(arguments, other.arguments);
83 public int hashCode(){
84 int h = name.hashCode();
86 for (int i=0; i<arguments.length; i++){
87 h = OATHash.hashMixin(h, arguments[i].hashCode());
90 return OATHash.hashFinalize(h);
93 protected void setNext (Event e){
98 protected void setPrev (Event e){
106 protected void setAlt (Event e){
114 public void setLinksFrom (Event other){
120 public Event replaceWithSequenceFrom (List<Event> list){
143 public Event replaceWithAlternativesFrom (List<Event> list){
164 public Event replaceWith (Event e){
172 protected void setSource (Object source){
173 this.source = source;
176 public int getNumberOfAlternatives(){
178 for (Event e = alt; e != null; e = e.alt) {
185 public boolean hasAlternatives(){
186 return (alt != null);
189 public List<Event> getAlternatives(){
190 List<Event> list = new ArrayList<Event>();
192 for (Event e = alt; e != null; e = e.alt) {
199 public Event unlinkedClone(){
201 Event e = (Event)super.clone();
202 e.next = e.prev = e.alt = null;
205 } catch (CloneNotSupportedException x) {
206 throw new RuntimeException("event clone failed", x);
211 public Event clone(){
213 return (Event) super.clone();
214 } catch (CloneNotSupportedException cnsx){
215 throw new RuntimeException("Event clone failed");
219 public Event deepClone(){
221 Event e = (Event)super.clone();
224 e.next = next.deepClone();
227 if (next.alt != null){
233 e.alt = alt.deepClone();
238 } catch (CloneNotSupportedException x) {
239 throw new RuntimeException("event clone failed", x);
243 public String getName(){
247 public Object[] getArguments(){
251 public Object getArgument(int idx){
252 if (idx < arguments.length){
253 return arguments[idx];
258 public Event getNext(){
262 public Event getAlt(){
266 public Event getPrev(){
270 public Object getSource(){
274 public Event addNext (Event e){
275 boolean first = true;
276 for (Event ee : endEvents()){ // this includes alternatives
280 first = false; // first one doesn't need a clone
289 public Event addAlternative (Event e){
291 for (ea = this; ea.alt != null; ea = ea.alt);
295 e.setNext( next.deepClone());
301 protected static Event createClonedSequence (int firstIdx, int len, Event[] events){
302 Event base = events[firstIdx].unlinkedClone();
305 for (int i = firstIdx+1; i < len; i++) {
306 Event ne = events[i].unlinkedClone();
315 * extend this tree with a new path
317 public void addPath (int pathLength, Event... path){
322 for (int i=0; i<pathLength; i++){
324 for (Event te = t; te != null; te = te.alt){
325 if (pe.equals(te)){ // prefix is in tree
327 if (te.next == null){ // reached tree leaf
328 if (++i < pathLength){ // but the path still has events
329 Event tail = createClonedSequence( i, pathLength, path);
331 tail.setAlt( new NoEvent()); // preserve the tree path
335 } else { // there is a next in the tree
338 if (i == pathLength-1){ // but the path is done, add a NoEvent as a next alternative to mark the end
339 Event e = t.getLastAlt();
340 e.setAlt(new NoEvent());
350 //--- path prefix was not in tree, append as (last) alternative
351 Event tail = createClonedSequence( i, pathLength, path);
352 Event e = t.getLastAlt();
359 public Event getLastAlt (){
361 for (e=this; e.alt != null; e = e.alt);
365 protected void collectEndEvents (List<Event> list, boolean includeNoEvents) {
367 next.collectEndEvents(list, includeNoEvents);
369 } else { // base case: no next
370 // strip trailing NoEvents
372 list.add(this); // root NoEvents have to stay
374 } else { // else we skip trailing NoEvents up to root
376 if (!includeNoEvents){
377 for (Event e=this; e.prev != null && (e instanceof NoEvent); e = e.prev){
386 alt.collectEndEvents(list, includeNoEvents);
390 public Event endEvent() {
392 return next.endEvent();
398 public List<Event> visibleEndEvents(){
399 List<Event> list = new ArrayList<Event>();
400 collectEndEvents(list, false);
405 public List<Event> endEvents(){
406 List<Event> list = new ArrayList<Event>();
407 collectEndEvents(list, true);
412 private void interleave (Event a, Event b, Event[] path, int pathLength, int i, Event result){
413 if (a == null && b == null){ // base case
414 result.addPath(pathLength, path);
419 interleave(a.prev, b, path, pathLength, i - 1, result);
424 interleave(a, b.prev, path, pathLength, i - 1, result);
430 * this creates a new tree that contains all paths resulting from
431 * all interleavings of all paths of this tree with the specified other events
433 * BEWARE: this is a combinatorial bomb that should only be used if we know all
436 public Event interleave (Event... otherEvents){
437 Event t = new NoEvent(); // we need a root for the new tree
439 Event[] pathBuffer = new Event[32];
442 for (Event o : otherEvents){
443 List<Event> endEvents = (mergedTrees++ > 0) ? t.visibleEndEvents() : visibleEndEvents();
445 for (Event ee1 : endEvents) {
446 for (Event ee2 : o.visibleEndEvents()) {
447 int n = ee1.getPathLength() + ee2.getPathLength();
448 if (n > pathBuffer.length){
449 pathBuffer = new Event[n];
452 interleave(ee1, ee2, pathBuffer, n, n - 1, t);
462 private void removeSource (Object src, Event[] path, int i, Event result){
465 alt.removeSource(src, path, i, result);
473 next.removeSource(src, path, i, result);
475 } else { // done, add path to result
476 result.addPath( i, path);
481 * remove all events from this tree that are from the specified source
483 public Event removeSource (Object src){
484 Event base = new NoEvent(); // we need a root to add to
485 int maxDepth = getMaxDepth();
486 Event[] pathBuffer = new Event[maxDepth];
488 removeSource( src, pathBuffer, 0, base);
493 private void printPath (PrintStream ps, boolean isLast){
495 prev.printPath(ps, false);
506 public void printPath (PrintStream ps){
511 public String toString(){
512 StringBuilder sb = new StringBuilder();
514 if (arguments != NO_ARGUMENTS) {
516 boolean first = true;
517 for (Object a : arguments) {
523 sb.append(a.toString());
527 return sb.toString();
532 * upwards path length
534 public int getPathLength(){
537 for (Event e=this; e != null; e = e.prev){
545 private int getMaxDepth (int depth){
550 maxAlt = alt.getMaxDepth(depth);
554 maxNext = next.getMaxDepth(depth + 1);
557 if (maxAlt > maxNext){
565 * maximum downwards tree depth
567 public int getMaxDepth(){
568 return getMaxDepth(1);
571 public Event[] getPath(){
572 int n = getPathLength();
573 Event[] trace = new Event[n];
575 for (Event e=this; e != null; e = e.prev){
582 public void printTree (PrintStream ps, int level) {
583 for (int i = 0; i < level; i++) {
588 //ps.print(" [" + prev + ']');
592 next.printTree(ps, level + 1);
596 alt.printTree(ps, level);
600 public boolean isEndOfTrace (String[] eventNames){
601 int n = eventNames.length-1;
603 for (Event e=this; e!= null; e = e.prev){
604 if (e.getName().equals(eventNames[n])){
614 protected void collectTrace (StringBuilder sb, String separator, boolean isLast){
616 prev.collectTrace(sb, separator, false);
620 sb.append(toString());
622 if (!isLast && separator != null){
623 sb.append(separator);
628 public String getPathString (String separator){
629 StringBuilder sb = new StringBuilder();
630 collectTrace( sb, separator, true);
631 return sb.toString();
634 public boolean isNoEvent(){
638 public boolean isSystemEvent(){
642 //--- generic processing interface
644 public void process(Object source){
645 // can be overridden by subclass if instance has sufficient context info
648 public void setProcessed(){
649 // can be overridden by subclass, e.g. to maintain event caches