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.PropertyListenerAdapter;
22 import gov.nasa.jpf.search.Search;
23 import gov.nasa.jpf.vm.VM;
24 import gov.nasa.jpf.vm.SystemState;
26 import java.util.ArrayList;
27 import java.util.HashSet;
31 * If there is a cycle in the states of the program, JPF doesn't execute the
32 * already visited states. A cycle in the states may represent the ability for
33 * the program to hang. This property finds and outputs cycles in the states
34 * so that they may be investigated.
36 * The following might need to be added to listener property...
37 * gov.nasa.jpf.tools.SimpleIdleFilter
38 * gov.nasa.jpf.tools.IdleFilter
41 public class NoStateCycles extends PropertyListenerAdapter {
43 private final HashSet<Integer> m_inStack = new HashSet<Integer>();
44 private final ArrayList<Integer> m_stack = new ArrayList<Integer>();
46 private int m_cycleFound = -1;
47 private int m_stackPos = -1;
49 public NoStateCycles(Config config) {
50 if (!config.getString("search.class").equals("gov.nasa.jpf.search.DFSearch"))
51 config.throwException("search.class must be gov.nasa.jpf.search.DFSearch"); // Or any class which does a depth first search.
55 public void stateAdvanced(Search search) {
59 state = search.getVM().getSystemState();
60 if (state.isInitState())
65 if ((m_stackPos < 0) && (m_inStack.contains(id))) {
68 for (m_stackPos = m_stack.size() - 1; m_stackPos >= 0; m_stackPos--)
69 if (m_stack.get(m_stackPos).equals(id))
78 public void stateBacktracked(Search search) {
82 pos = m_stack.size() - 1;
83 id = m_stack.remove(pos);
86 if (m_stackPos >= pos)
91 public boolean check(Search search, VM vm) {
92 return(m_cycleFound < 0);
96 public void reset () {
101 public String getErrorMessage () {
102 StringBuilder result;
105 result = new StringBuilder();
106 result.append("States:\n");
108 for (i = m_stack.size() - 1; i >= 0; i--) {
115 if (id == m_cycleFound)
119 return(result.toString());
123 public String getExplanation () {
124 return("Finds cycles in states. A cycle suggests that the program might be able to hang.");