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.
18 package gov.nasa.jpf.listener;
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.JPF;
22 import gov.nasa.jpf.ListenerAdapter;
23 import gov.nasa.jpf.search.Search;
24 import gov.nasa.jpf.jvm.bytecode.*;
25 import gov.nasa.jpf.vm.*;
26 import gov.nasa.jpf.vm.bytecode.LocalVariableInstruction;
27 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
28 import gov.nasa.jpf.vm.bytecode.StoreInstruction;
29 import gov.nasa.jpf.vm.bytecode.WriteInstruction;
30 import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
32 import java.io.PrintWriter;
37 * simple tool to log state changes
39 public class StateReducer extends ListenerAdapter {
41 private final PrintWriter out;
42 volatile private String valueVarLock = "";
43 volatile private String valueVarContact = "";
44 volatile private String operation;
45 volatile private String detail;
46 volatile private int depth;
47 volatile private int id;
48 Transition transition;
55 public StateReducer (Config conf, JPF jpf) {
56 out = new PrintWriter(System.out, true);
60 public void stateRestored(Search search) {
61 id = search.getStateId();
62 depth = search.getDepth();
63 operation = "restored";
64 transition = search.getTransition();
65 if (transition != null) {
66 annotation = transition.getAnnotation();
67 label = transition.getLabel();
68 output = transition.getOutput();
69 stateId = transition.getStateId();
73 out.println("\nThe state is restored to state with id: "+id+" Transition: "+transition+", with depth: "+depth+"##LockValue: "+valueVarLock+", ##ContactValue: "+valueVarContact +"\n");
76 //--- the ones we are interested in
78 public void searchStarted(Search search) {
79 out.println("----------------------------------- search started");
82 // Holds values that have appeared during CG advances
83 private HashSet<Integer> cgChoiceSet = new HashSet<>();
84 private Integer choiceUpperBound = 0;
85 private boolean isInitialized = false;
88 public void choiceGeneratorSet (VM vm, ChoiceGenerator<?> newCG) {
90 // Initialize with necessary information from the CG
91 if (newCG instanceof IntIntervalGenerator) {
92 IntIntervalGenerator iigCG = (IntIntervalGenerator) newCG;
93 // Check if CG has been initialized, otherwise initialize it
95 Integer[] choices = iigCG.getChoices();
96 // Get the upper bound from the last element of the choices
97 choiceUpperBound = choices[choices.length - 1];
106 public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
107 // Check every choice generated and make sure that all the available choices
108 // are chosen first before repeating the same choice of value twice!
109 if (currentCG instanceof IntIntervalGenerator) {
110 IntIntervalGenerator iigCG = (IntIntervalGenerator) currentCG;
111 Integer nextChoice = iigCG.getNextChoice();
112 if (!cgChoiceSet.contains(nextChoice)) {
113 cgChoiceSet.add(nextChoice);
115 // Allow reinitialization after an upper bound is hit
116 // This means all available choices have been explored once during this iteration
117 if (cgChoiceSet.contains(choiceUpperBound)) {
118 isInitialized = false;
125 public void stateAdvanced(Search search) {
126 String theEnd = null;
127 id = search.getStateId();
128 depth = search.getDepth();
129 operation = "forward";
130 transition = search.getTransition();
131 if (transition != null) {
132 annotation = transition.getAnnotation();
133 label = transition.getLabel();
134 output = transition.getOutput();
135 stateId = transition.getStateId();
137 if (search.isNewState()) {
143 if (search.isEndState()) {
144 out.println("This is the last state!");
148 //out.println("stateId: "+stateId+", output: "+output+", label: "+label);
149 out.println("\nThe state is forwarded to state with id: "+id+", with depth: "+depth+" which is "+detail+" Transition: "+transition+" state: "+"% "+theEnd+"##LockValue: "+valueVarLock+", ##ContactValue: "+valueVarContact +"\n");
151 if (search.isEndState()) {
157 public void stateBacktracked(Search search) {
158 id = search.getStateId();
159 depth = search.getDepth();
160 operation = "backtrack";
161 transition = search.getTransition();
162 if (transition != null) {
163 annotation = transition.getAnnotation();
164 label = transition.getLabel();
165 output = transition.getOutput();
166 stateId = transition.getStateId();
170 out.println("\nThe state is backtracked to state with id: "+id+" Transition: "+ transition+", with depth: "+depth+"##LockValue: "+valueVarLock+", ##ContactValue: "+valueVarContact +"\n");
174 public void searchFinished(Search search) {
175 out.println("----------------------------------- search finished");