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;
36 // TODO: Fix for Groovy's model-checking
37 // TODO: This is a listener created to detect device conflicts and global variable conflicts
39 * Simple listener tool to track remove unwanted ChoiceGenerators that are registered
40 * while an existing ChoiceGenerator is being explored. Multiple ChoiceGenerators of the same
41 * type could be registered spuriously during a while(true) loop.
43 public class StateReducer extends ListenerAdapter {
45 private boolean debugMode;
46 private boolean stateReductionMode;
47 private final PrintWriter out;
48 private String detail;
51 private Transition transition;
53 // Holds values that have appeared during CG advances
54 private HashSet<Integer> cgChoiceSet;
55 private Integer choiceUpperBound;
56 private boolean isInitialized;
58 public StateReducer (Config config, JPF jpf) {
59 debugMode = config.getBoolean("debug_state_transition", false);
60 stateReductionMode = config.getBoolean("activate_state_reduction", true);
62 out = new PrintWriter(System.out, true);
70 cgChoiceSet = new HashSet<>();
72 isInitialized = false;
76 public void stateRestored(Search search) {
78 id = search.getStateId();
79 depth = search.getDepth();
80 transition = search.getTransition();
82 out.println("\n==> DEBUG: The state is restored to state with id: " + id + " -- Transition: " + transition +
83 " and depth: " + depth + "\n");
87 //--- the ones we are interested in
89 public void searchStarted(Search search) {
91 out.println("\n==> DEBUG: ----------------------------------- search started" + "\n");
96 public void choiceGeneratorSet (VM vm, ChoiceGenerator<?> newCG) {
97 if (stateReductionMode) {
98 // Initialize with necessary information from the CG
99 if (newCG instanceof IntIntervalGenerator) {
100 IntIntervalGenerator iigCG = (IntIntervalGenerator) newCG;
101 // Check if CG has been initialized, otherwise initialize it
102 if (!isInitialized) {
103 Integer[] choices = iigCG.getChoices();
104 // Get the upper bound from the last element of the choices
105 choiceUpperBound = choices[choices.length - 1];
106 isInitialized = true;
115 public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator<?> currentCG) {
116 if (stateReductionMode) {
117 // Check every choice generated and make sure that all the available choices
118 // are chosen first before repeating the same choice of value twice!
119 if (currentCG instanceof IntIntervalGenerator) {
120 IntIntervalGenerator iigCG = (IntIntervalGenerator) currentCG;
121 Integer nextChoice = iigCG.getNextChoice();
122 if (!cgChoiceSet.contains(nextChoice)) {
123 cgChoiceSet.add(nextChoice);
125 // Allow reinitialization after an upper bound is hit
126 // This means all available choices have been explored once during this iteration
127 if (cgChoiceSet.contains(choiceUpperBound)) {
128 isInitialized = false;
136 public void stateAdvanced(Search search) {
138 id = search.getStateId();
139 depth = search.getDepth();
140 transition = search.getTransition();
141 if (search.isNewState()) {
147 if (search.isEndState()) {
148 out.println("\n==> DEBUG: This is the last state!\n");
151 out.println("\n==> DEBUG: The state is forwarded to state with id: " + id + " with depth: " + depth +
152 " which is " + detail + " Transition: " + transition + "\n");
157 public void stateBacktracked(Search search) {
159 id = search.getStateId();
160 depth = search.getDepth();
161 transition = search.getTransition();
164 out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
165 " and depth: " + depth + "\n");
170 public void searchFinished(Search search) {
172 out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");