--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/listener/NoStateCycles.java	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,126 @@
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+package gov.nasa.jpf.listener;
+
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.PropertyListenerAdapter;
+import gov.nasa.jpf.search.Search;
+import gov.nasa.jpf.vm.VM;
+import gov.nasa.jpf.vm.SystemState;
+
+import java.util.ArrayList;
+import java.util.HashSet;
+
+
+/**
+ * If there is a cycle in the states of the program, JPF doesn't execute the
+ * already visited states.  A cycle in the states may represent the ability for
+ * the program to hang.  This property finds and outputs cycles in the states
+ * so that they may be investigated.
+ *
+ * The following might need to be added to listener property...
+ *   gov.nasa.jpf.tools.SimpleIdleFilter
+ *   gov.nasa.jpf.tools.IdleFilter
+ */
+
+public class NoStateCycles extends PropertyListenerAdapter {
+
+  private final HashSet<Integer>   m_inStack = new HashSet<Integer>();
+  private final ArrayList<Integer> m_stack   = new ArrayList<Integer>();
+
+  private int m_cycleFound = -1;
+  private int m_stackPos   = -1;
+
+  public NoStateCycles(Config config) {
+    if (!config.getString("search.class").equals("gov.nasa.jpf.search.DFSearch"))
+      config.throwException("search.class must be gov.nasa.jpf.search.DFSearch");   // Or any class which does a depth first search.
+  }
+
+  @Override
+   public void stateAdvanced(Search search) {
+     SystemState state;
+     Integer id;
+
+     state = search.getVM().getSystemState();
+     if (state.isInitState())
+       return;
+
+     id = state.getId();
+
+     if ((m_stackPos < 0) && (m_inStack.contains(id))) {
+       m_cycleFound = id;
+
+       for (m_stackPos = m_stack.size() - 1; m_stackPos >= 0; m_stackPos--)
+         if (m_stack.get(m_stackPos).equals(id))
+           break;
+     }
+
+     m_stack.add(id);
+     m_inStack.add(id);
+   }
+
+  @Override
+   public void stateBacktracked(Search search) {
+     Integer id;
+     int pos;
+
+     pos = m_stack.size() - 1;
+     id  = m_stack.remove(pos);
+     m_inStack.remove(id);
+
+     if (m_stackPos >= pos)
+       m_stackPos = -1;
+   }
+
+  @Override
+   public boolean check(Search search, VM vm) {
+     return(m_cycleFound < 0);
+   }
+
+   @Override
+   public void reset () {
+     m_cycleFound = -1;
+   }
+
+   @Override
+  public String getErrorMessage () {
+     StringBuilder result;
+     int i, id;
+
+     result = new StringBuilder();
+     result.append("States:\n");
+
+     for (i = m_stack.size() - 1; i >= 0; i--) {
+       id = m_stack.get(i);
+
+       result.append("  ");
+       result.append(id);
+       result.append('\n');
+
+       if (id == m_cycleFound)
+         break;
+     }
+
+     return(result.toString());
+   }
+
+   @Override
+  public String getExplanation () {
+     return("Finds cycles in states.  A cycle suggests that the program might be able to hang.");
+   }
+}