Initial import
[jpf-core.git] / src / main / gov / nasa / jpf / util / event / Event.java
1 /*
2  * Copyright (C) 2014, United States Government, as represented by the
3  * Administrator of the National Aeronautics and Space Administration.
4  * All rights reserved.
5  *
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
9  * 
10  *        http://www.apache.org/licenses/LICENSE-2.0. 
11  *
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.
17  */
18
19 package gov.nasa.jpf.util.event;
20
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;
26
27 /**
28  * class that represents an external stimulus to the SUT, which is produced by EventTree instances
29  * (our environment models)
30  * 
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
33  */
34 public class Event implements Cloneable {
35
36   static final Object[] NO_ARGUMENTS = new Object[0];
37   
38   //--- linkage
39   protected Event next;
40   protected Event prev;
41   protected Event alt;
42
43   //--- payload
44   protected String name;
45   protected Object[] arguments;
46   
47   protected Object source;  // optional, set on demand to keep track of where an event came from
48
49   public Event (String name){
50     this( name, NO_ARGUMENTS, null);
51   }
52
53   public Event (String name, Object source){
54     this( name, NO_ARGUMENTS, source);
55   }  
56   
57   public Event(String name, Object[] arguments) {
58     this(name, arguments, null);
59   }
60   
61   public Event(String name, Object[] arguments, Object source) {
62     this.name = name;
63     this.arguments = arguments != null ? arguments : NO_ARGUMENTS;
64     this.source = source;
65   }
66
67   
68   
69   @Override
70   public boolean equals (Object o){
71     if (o instanceof Event){
72       Event other = (Event)o;
73       
74       if (name.equals(other.name)){
75         return Misc.equals(arguments, other.arguments);
76       }
77     }
78     
79     return false;
80   }
81   
82   @Override
83   public int hashCode(){
84     int h = name.hashCode();
85     
86     for (int i=0; i<arguments.length; i++){
87       h = OATHash.hashMixin(h, arguments[i].hashCode());
88     }
89     
90     return OATHash.hashFinalize(h);
91   }
92   
93   protected void setNext (Event e){
94     next = e;
95     e.prev = this;
96   }
97
98   protected void setPrev (Event e){
99     prev = e;
100
101     if (alt != null){
102       alt.setPrev(e);
103     }
104   }
105
106   protected void setAlt (Event e){
107     alt = e;
108
109     if (prev != null) {
110       e.setPrev(prev);
111     }
112   }
113   
114   public void setLinksFrom (Event other){
115     prev = other.prev;
116     next = other.next;
117     alt = other.alt;
118   }
119
120   public Event replaceWithSequenceFrom (List<Event> list){
121     Event eLast = null;
122     
123     for (Event e: list){
124       if (eLast == null){
125         e.prev = prev;
126         e.alt = alt;
127       } else {
128         e.prev = eLast;
129         eLast.next = e;
130       }
131       
132       eLast = e;
133     }
134     
135     if (eLast != null){
136       eLast.next = next;
137       return list.get(0);
138     } else {
139       return null;
140     }
141   }
142   
143   public Event replaceWithAlternativesFrom (List<Event> list){
144     Event eLast = null;
145     for (Event e: list){
146       e.prev = prev;
147       e.next = next;
148       
149       if (eLast != null){
150         eLast.alt = e;
151       }
152       
153       eLast = e;
154     }
155     
156     if (eLast != null){
157       eLast.alt = alt;
158       return list.get(0);
159     } else {
160       return null;
161     }
162   }
163
164   public Event replaceWith (Event e){
165     e.prev = prev;
166     e.next = next;
167     e.alt = alt;
168     
169     return e;
170   }
171   
172   protected void setSource (Object source){
173     this.source = source;
174   }
175   
176   public int getNumberOfAlternatives(){
177     int n = 0;
178     for (Event e = alt; e != null; e = e.alt) {
179       n++;
180     }
181
182     return n;
183   }
184
185   public boolean hasAlternatives(){
186     return (alt != null);
187   }
188   
189   public List<Event> getAlternatives(){
190     List<Event> list = new ArrayList<Event>();
191     list.add(this);
192     for (Event e = alt; e != null; e = e.alt) {
193       list.add(e);
194     }
195     return list;
196   }
197   
198   
199   public Event unlinkedClone(){
200     try {
201       Event e = (Event)super.clone();
202       e.next = e.prev = e.alt = null;
203       return e;
204
205     } catch (CloneNotSupportedException x) {
206       throw new RuntimeException("event clone failed", x);
207     }
208     
209   }
210
211   public Event clone(){
212     try {
213       return (Event) super.clone();
214     } catch (CloneNotSupportedException cnsx){
215       throw new RuntimeException("Event clone failed");
216     }
217   }
218
219   public Event deepClone(){
220     try {
221       Event e = (Event)super.clone();
222
223       if (next != null) {
224         e.next = next.deepClone();
225         e.next.prev = e;
226
227         if (next.alt != null){
228           e.next.alt.prev = e;
229         }
230       }
231
232       if (alt != null) {
233         e.alt = alt.deepClone();
234       }
235
236       return e;
237
238     } catch (CloneNotSupportedException x) {
239       throw new RuntimeException("event clone failed", x);
240     }
241   }
242
243   public String getName(){
244     return name;
245   }
246
247   public Object[] getArguments(){
248     return arguments;
249   }
250
251   public Object getArgument(int idx){
252     if (idx < arguments.length){
253       return arguments[idx];
254     }
255     return null;
256   }
257   
258   public Event getNext(){
259     return next;
260   }
261   
262   public Event getAlt(){
263     return alt;
264   }
265   
266   public Event getPrev(){
267     return prev;
268   }
269   
270   public Object getSource(){
271     return source;
272   }
273   
274   public Event addNext (Event e){
275     boolean first = true;
276     for (Event ee : endEvents()){  // this includes alternatives
277       if (!first){
278         e = e.deepClone();
279       } else {
280         first = false;      // first one doesn't need a clone
281       }
282       ee.setNext(e);
283       e.setPrev(ee);
284     }
285
286     return this;
287   }
288
289   public Event addAlternative (Event e){
290     Event ea ;
291     for (ea = this; ea.alt != null; ea = ea.alt);
292     ea.setAlt(e);
293
294     if (next != null){
295       e.setNext( next.deepClone());
296     }
297
298     return this;
299   }
300   
301   protected static Event createClonedSequence (int firstIdx, int len, Event[] events){
302     Event base = events[firstIdx].unlinkedClone();
303     Event e = base;
304
305     for (int i = firstIdx+1; i < len; i++) {
306       Event ne = events[i].unlinkedClone();
307       e.setNext( ne);
308       e = ne;
309     }
310     
311     return base;
312   }
313   
314   /**
315    * extend this tree with a new path 
316    */
317   public void addPath (int pathLength, Event... path){
318     Event t = this;
319     Event pe;
320     
321     outer:
322     for (int i=0; i<pathLength; i++){
323       pe = path[i];
324       for (Event te = t; te != null; te = te.alt){
325         if (pe.equals(te)){      // prefix is in tree
326           
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);
330               te.setNext(tail);
331               tail.setAlt( new NoEvent()); // preserve the tree path
332             }
333             return;
334             
335           } else { // there is a next in the tree
336             t = te.next;
337             
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());
341               return;
342               
343             } else {
344               continue outer;
345             }
346           }
347         }
348       }
349       
350       //--- path prefix was not in tree, append as (last) alternative
351       Event tail = createClonedSequence( i, pathLength, path);
352       Event e = t.getLastAlt();
353       e.setAlt( tail);
354       
355       return;
356     }
357   }
358
359   public Event getLastAlt (){
360     Event e;
361     for (e=this; e.alt != null; e = e.alt);
362     return e;
363   }
364   
365   protected void collectEndEvents (List<Event> list, boolean includeNoEvents) {
366     if (next != null) {
367       next.collectEndEvents(list, includeNoEvents);
368       
369     } else { // base case: no next
370       // strip trailing NoEvents 
371       if (prev == null){
372         list.add(this); // root NoEvents have to stay
373         
374       } else { // else we skip trailing NoEvents up to root
375         Event ee = this;
376         if (!includeNoEvents){
377           for (Event e=this; e.prev != null && (e instanceof NoEvent); e = e.prev){
378             ee = e.prev;
379           }
380         }
381         list.add(ee);
382       }
383     }
384
385     if (alt != null) {
386       alt.collectEndEvents(list, includeNoEvents);
387     }
388   }
389
390   public Event endEvent() {
391     if (next != null) {
392       return next.endEvent();
393     } else {
394       return this;
395     }
396   }
397
398   public List<Event> visibleEndEvents(){
399     List<Event> list = new ArrayList<Event>();
400     collectEndEvents(list, false);
401     return list;
402   }
403  
404   
405   public List<Event> endEvents(){
406     List<Event> list = new ArrayList<Event>();
407     collectEndEvents(list, true);
408     return list;
409   }
410   
411  
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);
415       
416     } else {
417       if (a != null) {
418         path[i] = a;
419         interleave(a.prev, b, path, pathLength, i - 1, result);
420       }
421
422       if (b != null) {
423         path[i] = b;
424         interleave(a, b.prev, path, pathLength, i - 1, result);
425       }
426     }
427   }
428   
429   /**
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
432    * 
433    * BEWARE: this is a combinatorial bomb that should only be used if we know all
434    * paths are short
435    */
436   public Event interleave (Event... otherEvents){
437     Event t = new NoEvent(); // we need a root for the new tree
438     
439     Event[] pathBuffer = new Event[32];
440     int mergedTrees = 0;
441     
442     for (Event o : otherEvents){
443       List<Event> endEvents = (mergedTrees++ > 0) ? t.visibleEndEvents() : visibleEndEvents();
444
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];
450           }
451
452           interleave(ee1, ee2, pathBuffer, n, n - 1, t);
453         }
454       }
455     }
456         
457     return t.alt;
458   }
459   
460   
461   
462   private void removeSource (Object src, Event[] path, int i, Event result){
463     
464     if (alt != null){
465       alt.removeSource(src, path, i, result);
466     }
467     
468     if (source != src){
469       path[i++] = this;
470     }
471     
472     if (next != null){
473       next.removeSource(src, path, i, result);
474       
475     } else { // done, add path to result
476       result.addPath( i, path);
477     }
478   }
479   
480   /**
481    * remove all events from this tree that are from the specified source 
482    */
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];
487     
488     removeSource( src, pathBuffer, 0, base);
489     
490     return base.alt;
491   }
492   
493   private void printPath (PrintStream ps, boolean isLast){
494     if (prev != null){
495       prev.printPath(ps, false);
496     }
497     
498     if (!isNoEvent()){
499       ps.print(name);
500       if (!isLast){
501         ps.print(',');
502       }
503     }
504   }
505   
506   public void printPath (PrintStream ps){
507     printPath(ps, true);
508   }
509
510   @Override
511   public String toString(){
512     StringBuilder sb = new StringBuilder();
513     sb.append(name);
514     if (arguments != NO_ARGUMENTS) {
515       sb.append('(');
516       boolean first = true;
517       for (Object a : arguments) {
518         if (first){
519           first = false;
520         } else {
521           sb.append(',');
522         }
523         sb.append(a.toString());
524       }
525       sb.append(')');
526     }
527     return sb.toString();
528   }
529
530   
531   /**
532    * upwards path length 
533    */
534   public int getPathLength(){
535     int n=0;
536     
537     for (Event e=this; e != null; e = e.prev){
538       n++;
539     }
540     
541     return n;
542   }
543   
544   
545   private int getMaxDepth (int depth){
546     int maxAlt = depth;
547     int maxNext = depth;
548     
549     if (alt != null){
550       maxAlt = alt.getMaxDepth(depth);
551     }
552     
553     if (next != null){
554       maxNext = next.getMaxDepth(depth + 1);
555     }
556     
557     if (maxAlt > maxNext){
558       return maxAlt;
559     } else {
560       return maxNext;
561     }
562   }
563   
564   /**
565    * maximum downwards tree depth 
566    */
567   public int getMaxDepth(){
568     return getMaxDepth(1);
569   }
570   
571   public Event[] getPath(){
572     int n = getPathLength();
573     Event[] trace = new Event[n];
574     
575     for (Event e=this; e != null; e = e.prev){
576       trace[--n] = e;
577     }
578     
579     return trace;
580   }
581   
582   public void printTree (PrintStream ps, int level) {
583     for (int i = 0; i < level; i++) {
584       ps.print(". ");
585     }
586     
587     ps.print(this);
588     //ps.print(" [" + prev + ']');
589     ps.println();
590
591     if (next != null) {
592       next.printTree(ps, level + 1);
593     }
594
595     if (alt != null) {
596       alt.printTree(ps, level);
597     }
598   }
599   
600   public boolean isEndOfTrace (String[] eventNames){
601     int n = eventNames.length-1;
602     
603     for (Event e=this; e!= null; e = e.prev){
604       if (e.getName().equals(eventNames[n])){
605         n--;
606       } else {
607         return false;
608       }
609     }
610     
611     return (n == 0);
612   }
613   
614   protected void collectTrace (StringBuilder sb, String separator, boolean isLast){
615     if (prev != null){
616       prev.collectTrace(sb, separator, false);    
617     }
618
619     if (!isNoEvent()){
620       sb.append(toString());
621       
622       if (!isLast && separator != null){
623         sb.append(separator);        
624       }
625     }
626   }
627   
628   public String getPathString (String separator){
629     StringBuilder sb = new StringBuilder();
630     collectTrace( sb, separator, true);
631     return sb.toString();
632   }
633   
634   public boolean isNoEvent(){
635     return false;
636   }
637
638   public boolean isSystemEvent(){
639     return false;
640   }
641
642   //--- generic processing interface
643   
644   public void process(Object source){
645     // can be overridden by subclass if instance has sufficient context info
646   }
647   
648   public void setProcessed(){
649     // can be overridden by subclass, e.g. to maintain event caches
650   }
651 }