Mercurial > hg > Members > kono > jpf-core
view src/main/gov/nasa/jpf/util/event/Event.java @ 21:caa0924e093d
reshuffled Event hierarchy, introducing SystemEvent, with CheckEvent and
ControlEvent being subclasses of SystemEvent
added Loggable.setLogLevel
changed old UserHeuristic to use a Verify.heuristicValue instead of a
hardwired "Main" class with hardwired fields (which was just an outdated
leftover). Call Verify.setHeuristicValue() to control state priorities from the
SUT.
This also fixes the bug that UserHeuristic was not properly checking for
"Main" resolution.
author | Peter Mehlitz <pcmehlitz@gmail.com> |
---|---|
date | Fri, 10 Apr 2015 20:53:11 -0700 |
parents | b1790909ebb1 |
children |
line wrap: on
line source
/* * Copyright (C) 2014, United States Government, as represented by the * Administrator of the National Aeronautics and Space Administration. * All rights reserved. * * The Java Pathfinder core (jpf-core) platform is licensed under the * Apache License, Version 2.0 (the "License"); you may not use this file except * in compliance with the License. You may obtain a copy of the License at * * http://www.apache.org/licenses/LICENSE-2.0. * * Unless required by applicable law or agreed to in writing, software * distributed under the License is distributed on an "AS IS" BASIS, * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. * See the License for the specific language governing permissions and * limitations under the License. */ package gov.nasa.jpf.util.event; import gov.nasa.jpf.util.Misc; import gov.nasa.jpf.util.OATHash; import java.io.PrintStream; import java.util.ArrayList; import java.util.List; /** * class that represents an external stimulus to the SUT, which is produced by EventTree instances * (our environment models) * * Note that albeit concrete EventTree can provide their own, specialized Event types, this class * is generic enough that we don't declare it as abstract */ public class Event implements Cloneable { static final Object[] NO_ARGUMENTS = new Object[0]; //--- linkage protected Event next; protected Event prev; protected Event alt; //--- payload protected String name; protected Object[] arguments; protected Object source; // optional, set on demand to keep track of where an event came from public Event (String name){ this( name, NO_ARGUMENTS, null); } public Event (String name, Object source){ this( name, NO_ARGUMENTS, source); } public Event(String name, Object[] arguments) { this(name, arguments, null); } public Event(String name, Object[] arguments, Object source) { this.name = name; this.arguments = arguments != null ? arguments : NO_ARGUMENTS; this.source = source; } @Override public boolean equals (Object o){ if (o instanceof Event){ Event other = (Event)o; if (name.equals(other.name)){ return Misc.equals(arguments, other.arguments); } } return false; } @Override public int hashCode(){ int h = name.hashCode(); for (int i=0; i<arguments.length; i++){ h = OATHash.hashMixin(h, arguments[i].hashCode()); } return OATHash.hashFinalize(h); } protected void setNext (Event e){ next = e; e.prev = this; } protected void setPrev (Event e){ prev = e; if (alt != null){ alt.setPrev(e); } } protected void setAlt (Event e){ alt = e; if (prev != null) { 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; } public int getNumberOfAlternatives(){ int n = 0; for (Event e = alt; e != null; e = e.alt) { n++; } return n; } public boolean hasAlternatives(){ return (alt != null); } public List<Event> getAlternatives(){ List<Event> list = new ArrayList<Event>(); list.add(this); for (Event e = alt; e != null; e = e.alt) { list.add(e); } return list; } public Event unlinkedClone(){ try { Event e = (Event)super.clone(); e.next = e.prev = e.alt = null; return e; } catch (CloneNotSupportedException x) { throw new RuntimeException("event clone failed", x); } } public Event clone(){ try { return (Event) super.clone(); } catch (CloneNotSupportedException cnsx){ throw new RuntimeException("Event clone failed"); } } public Event deepClone(){ try { Event e = (Event)super.clone(); if (next != null) { e.next = next.deepClone(); e.next.prev = e; if (next.alt != null){ e.next.alt.prev = e; } } if (alt != null) { e.alt = alt.deepClone(); } return e; } catch (CloneNotSupportedException x) { throw new RuntimeException("event clone failed", x); } } public String getName(){ return name; } public Object[] getArguments(){ return arguments; } public Object getArgument(int idx){ if (idx < arguments.length){ return arguments[idx]; } return null; } public Event getNext(){ return next; } public Event getAlt(){ return alt; } public Event getPrev(){ return prev; } public Object getSource(){ return source; } public Event addNext (Event e){ boolean first = true; for (Event ee : endEvents()){ // this includes alternatives if (!first){ e = e.deepClone(); } else { first = false; // first one doesn't need a clone } ee.setNext(e); e.setPrev(ee); } return this; } public Event addAlternative (Event e){ Event ea ; for (ea = this; ea.alt != null; ea = ea.alt); ea.setAlt(e); if (next != null){ e.setNext( next.deepClone()); } return this; } protected static Event createClonedSequence (int firstIdx, int len, Event[] events){ Event base = events[firstIdx].unlinkedClone(); Event e = base; for (int i = firstIdx+1; i < len; i++) { Event ne = events[i].unlinkedClone(); e.setNext( ne); e = ne; } return base; } /** * extend this tree with a new path */ public void addPath (int pathLength, Event... path){ Event t = this; Event pe; outer: for (int i=0; i<pathLength; i++){ pe = path[i]; for (Event te = t; te != null; te = te.alt){ if (pe.equals(te)){ // prefix is in tree if (te.next == null){ // reached tree leaf if (++i < pathLength){ // but the path still has events Event tail = createClonedSequence( i, pathLength, path); te.setNext(tail); tail.setAlt( new NoEvent()); // preserve the tree path } return; } else { // there is a next in the tree t = te.next; if (i == pathLength-1){ // but the path is done, add a NoEvent as a next alternative to mark the end Event e = t.getLastAlt(); e.setAlt(new NoEvent()); return; } else { continue outer; } } } } //--- path prefix was not in tree, append as (last) alternative Event tail = createClonedSequence( i, pathLength, path); Event e = t.getLastAlt(); e.setAlt( tail); return; } } public Event getLastAlt (){ Event e; for (e=this; e.alt != null; e = e.alt); return e; } protected void collectEndEvents (List<Event> list, boolean includeNoEvents) { if (next != null) { next.collectEndEvents(list, includeNoEvents); } else { // base case: no next // strip trailing NoEvents if (prev == null){ list.add(this); // root NoEvents have to stay } else { // else we skip trailing NoEvents up to root Event ee = this; if (!includeNoEvents){ for (Event e=this; e.prev != null && (e instanceof NoEvent); e = e.prev){ ee = e.prev; } } list.add(ee); } } if (alt != null) { alt.collectEndEvents(list, includeNoEvents); } } public Event endEvent() { if (next != null) { return next.endEvent(); } else { return this; } } public List<Event> visibleEndEvents(){ List<Event> list = new ArrayList<Event>(); collectEndEvents(list, false); return list; } public List<Event> endEvents(){ List<Event> list = new ArrayList<Event>(); collectEndEvents(list, true); return list; } private void interleave (Event a, Event b, Event[] path, int pathLength, int i, Event result){ if (a == null && b == null){ // base case result.addPath(pathLength, path); } else { if (a != null) { path[i] = a; interleave(a.prev, b, path, pathLength, i - 1, result); } if (b != null) { path[i] = b; interleave(a, b.prev, path, pathLength, i - 1, result); } } } /** * this creates a new tree that contains all paths resulting from * all interleavings of all paths of this tree with the specified other events * * BEWARE: this is a combinatorial bomb that should only be used if we know all * paths are short */ public Event interleave (Event... otherEvents){ Event t = new NoEvent(); // we need a root for the new tree Event[] pathBuffer = new Event[32]; int mergedTrees = 0; for (Event o : otherEvents){ List<Event> endEvents = (mergedTrees++ > 0) ? t.visibleEndEvents() : visibleEndEvents(); for (Event ee1 : endEvents) { for (Event ee2 : o.visibleEndEvents()) { int n = ee1.getPathLength() + ee2.getPathLength(); if (n > pathBuffer.length){ pathBuffer = new Event[n]; } interleave(ee1, ee2, pathBuffer, n, n - 1, t); } } } return t.alt; } private void removeSource (Object src, Event[] path, int i, Event result){ if (alt != null){ alt.removeSource(src, path, i, result); } if (source != src){ path[i++] = this; } if (next != null){ next.removeSource(src, path, i, result); } else { // done, add path to result result.addPath( i, path); } } /** * remove all events from this tree that are from the specified source */ public Event removeSource (Object src){ Event base = new NoEvent(); // we need a root to add to int maxDepth = getMaxDepth(); Event[] pathBuffer = new Event[maxDepth]; removeSource( src, pathBuffer, 0, base); return base.alt; } private void printPath (PrintStream ps, boolean isLast){ if (prev != null){ prev.printPath(ps, false); } if (!isNoEvent()){ ps.print(name); if (!isLast){ ps.print(','); } } } public void printPath (PrintStream ps){ printPath(ps, true); } @Override public String toString(){ StringBuilder sb = new StringBuilder(); sb.append(name); if (arguments != NO_ARGUMENTS) { sb.append('('); boolean first = true; for (Object a : arguments) { if (first){ first = false; } else { sb.append(','); } sb.append(a.toString()); } sb.append(')'); } return sb.toString(); } /** * upwards path length */ public int getPathLength(){ int n=0; for (Event e=this; e != null; e = e.prev){ n++; } return n; } private int getMaxDepth (int depth){ int maxAlt = depth; int maxNext = depth; if (alt != null){ maxAlt = alt.getMaxDepth(depth); } if (next != null){ maxNext = next.getMaxDepth(depth + 1); } if (maxAlt > maxNext){ return maxAlt; } else { return maxNext; } } /** * maximum downwards tree depth */ public int getMaxDepth(){ return getMaxDepth(1); } public Event[] getPath(){ int n = getPathLength(); Event[] trace = new Event[n]; for (Event e=this; e != null; e = e.prev){ trace[--n] = e; } return trace; } public void printTree (PrintStream ps, int level) { for (int i = 0; i < level; i++) { ps.print(". "); } ps.print(this); //ps.print(" [" + prev + ']'); ps.println(); if (next != null) { next.printTree(ps, level + 1); } if (alt != null) { alt.printTree(ps, level); } } public boolean isEndOfTrace (String[] eventNames){ int n = eventNames.length-1; for (Event e=this; e!= null; e = e.prev){ if (e.getName().equals(eventNames[n])){ n--; } else { return false; } } return (n == 0); } protected void collectTrace (StringBuilder sb, String separator, boolean isLast){ if (prev != null){ prev.collectTrace(sb, separator, false); } if (!isNoEvent()){ sb.append(toString()); if (!isLast && separator != null){ sb.append(separator); } } } public String getPathString (String separator){ StringBuilder sb = new StringBuilder(); collectTrace( sb, separator, true); return sb.toString(); } public boolean isNoEvent(){ return false; } public boolean isSystemEvent(){ return false; } //--- generic processing interface public void process(Object source){ // 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 } }