1 package gov.nasa.jpf.search.heuristic; 20 21 import gov.nasa.jpf.Config; 22 import gov.nasa.jpf.VM; 23 import gov.nasa.jpf.jvm.TrailInfo; 24 25 26 32 public class Interleaving implements Heuristic { 33 private int[] threads; 34 HeuristicSearch search; 35 VM vm; 36 int threadHistoryLimit; 37 38 public Interleaving (Config config, HeuristicSearch hSearch) { 39 vm = hSearch.getVM(); 40 search = hSearch; 41 42 threadHistoryLimit = config.getInt("search.heuristic.thread_history_limit", -1); 43 } 44 45 public int heuristicValue () { 46 int aliveThreads = vm.getAliveThreadCount(); 47 48 int lastRun = ((TrailInfo) vm.getLastTransition()).getThread(); 49 int h_value = 0; 50 51 if (aliveThreads > 1) { 52 for (int i = 0; i < threads.length; i++) { 53 if (lastRun == threads[i]) { 54 h_value += ((threads.length - i) * aliveThreads); 55 } 56 } 57 } 58 59 int newSize = threads.length + 1; 60 61 if ((threadHistoryLimit > 0) && 62 (newSize > threadHistoryLimit)) { 63 newSize = threadHistoryLimit; 64 } 65 66 int[] newThreads = new int[newSize]; 67 newThreads[0] = lastRun; 68 69 for (int i = 1; i < newSize; i++) { 70 newThreads[i] = threads[i - 1]; 71 } 72 73 search.getNew().otherData = newThreads; 74 75 return h_value; 76 } 77 78 public void processParent () { 79 Object oldValue = search.getOld().otherData; 80 81 if (oldValue == null) { 82 threads = new int[0]; 83 } else { 84 threads = (int[]) oldValue; 85 } 86 } 87 } 88 | Popular Tags |