From 75c00d3f11e45587f0919d4c7de84a2249d1567e Mon Sep 17 00:00:00 2001 From: rtrimana Date: Wed, 25 Sep 2019 13:52:48 -0700 Subject: [PATCH] Updating main.jpf; Cleaning up the StateReducer. --- main.jpf | 13 +- .../gov/nasa/jpf/listener/StateReducer.java | 140 +++++++++--------- 2 files changed, 75 insertions(+), 78 deletions(-) diff --git a/main.jpf b/main.jpf index c1e04ca..ce6708f 100644 --- a/main.jpf +++ b/main.jpf @@ -1,13 +1,15 @@ target = main # This is the listener that can detect variable write-after-write conflicts -listener=gov.nasa.jpf.listener.VariableConflictTracker +#listener=gov.nasa.jpf.listener.VariableConflictTracker +#listener=gov.nasa.jpf.listener.StateReducer +listener=gov.nasa.jpf.listener.VariableConflictTracker,gov.nasa.jpf.listener.StateReducer # Potentially conflicting variables # Alarms #variables=currentAlarm # Locks -#variables=currentLock +variables=currentLock # Thermostats #variables=currentHeatingSetpoint,thermostatSetpoint,currentCoolingSetpoint,thermostatOperatingState,thermostatFanMode,currentThermostatMode # Switches @@ -23,13 +25,16 @@ listener=gov.nasa.jpf.listener.VariableConflictTracker # Valves #variables=valve,valveLatestValue # Cameras -variables=image,alarmState +#variables=image,alarmState # Potentially conflicting apps (we default to App1 and App2 for now) apps=App1,App2 # Tracking the location.mode variable conflict -track_location_var_conflict=true +#track_location_var_conflict=true + +# Debug mode for StateReducer +debug_state_transition=true # Timeout in minutes (default is 0 which means no timeout) timeout=30 diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java index 5dbe79d..60782a9 100644 --- a/src/main/gov/nasa/jpf/listener/StateReducer.java +++ b/src/main/gov/nasa/jpf/listener/StateReducer.java @@ -33,60 +33,65 @@ import java.io.PrintWriter; import java.util.*; +// TODO: Fix for Groovy's model-checking +// TODO: This is a listener created to detect device conflicts and global variable conflicts /** - * simple tool to log state changes + * Simple listener tool to track remove unwanted ChoiceGenerators that are registered + * while an existing ChoiceGenerator is being explored. Multiple ChoiceGenerators of the same + * type could be registered spuriously during a while(true) loop. */ public class StateReducer extends ListenerAdapter { + private boolean debugMode; private final PrintWriter out; - volatile private String valueVarLock = ""; - volatile private String valueVarContact = ""; - volatile private String operation; - volatile private String detail; - volatile private int depth; - volatile private int id; - Transition transition; - Object annotation; - String label; - String output; - int stateId; - - - public StateReducer (Config conf, JPF jpf) { - out = new PrintWriter(System.out, true); + private String detail; + private int depth; + private int id; + private Transition transition; + + // Holds values that have appeared during CG advances + private HashSet cgChoiceSet; + private Integer choiceUpperBound; + private boolean isInitialized; + + public StateReducer (Config config, JPF jpf) { + debugMode = config.getBoolean("debug_state_transition", false); + if (debugMode) { + out = new PrintWriter(System.out, true); + } else { + out = null; + } + detail = null; + depth = 0; + id = 0; + transition = null; + cgChoiceSet = new HashSet<>(); + choiceUpperBound = 0; + isInitialized = false; } @Override public void stateRestored(Search search) { - id = search.getStateId(); - depth = search.getDepth(); - operation = "restored"; - transition = search.getTransition(); - if (transition != null) { - annotation = transition.getAnnotation(); - label = transition.getLabel(); - output = transition.getOutput(); - stateId = transition.getStateId(); + if (debugMode) { + id = search.getStateId(); + depth = search.getDepth(); + transition = search.getTransition(); + detail = null; + out.println("\n==> DEBUG: The state is restored to state with id: " + id + " -- Transition: " + transition + + " and depth: " + depth + "\n"); } - detail = null; - - out.println("\nThe state is restored to state with id: "+id+" Transition: "+transition+", with depth: "+depth+"##LockValue: "+valueVarLock+", ##ContactValue: "+valueVarContact +"\n"); } //--- the ones we are interested in @Override public void searchStarted(Search search) { - out.println("----------------------------------- search started"); + if (debugMode) { + out.println("\n==> DEBUG: ----------------------------------- search started" + "\n"); + } } - // Holds values that have appeared during CG advances - private HashSet cgChoiceSet = new HashSet<>(); - private Integer choiceUpperBound = 0; - private boolean isInitialized = false; - @Override public void choiceGeneratorSet (VM vm, ChoiceGenerator newCG) { - // Initialize with necessary information from the CG if (newCG instanceof IntIntervalGenerator) { IntIntervalGenerator iigCG = (IntIntervalGenerator) newCG; @@ -123,55 +128,42 @@ public class StateReducer extends ListenerAdapter { @Override public void stateAdvanced(Search search) { - String theEnd = null; - id = search.getStateId(); - depth = search.getDepth(); - operation = "forward"; - transition = search.getTransition(); - if (transition != null) { - annotation = transition.getAnnotation(); - label = transition.getLabel(); - output = transition.getOutput(); - stateId = transition.getStateId(); - } - if (search.isNewState()) { - detail = "new"; - } else { - detail = "visited"; - } - - if (search.isEndState()) { - out.println("This is the last state!"); - theEnd = "end"; - } - - //out.println("stateId: "+stateId+", output: "+output+", label: "+label); - 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"); + if (debugMode) { + id = search.getStateId(); + depth = search.getDepth(); + transition = search.getTransition(); + if (search.isNewState()) { + detail = "new"; + } else { + detail = "visited"; + } - if (search.isEndState()) { - detail += " end"; + if (search.isEndState()) { + out.println("\n==> DEBUG: This is the last state!\n"); + detail += " end"; + } + out.println("\n==> DEBUG: The state is forwarded to state with id: " + id + " with depth: " + depth + + " which is " + detail + " Transition: " + transition + "\n"); } } @Override public void stateBacktracked(Search search) { - id = search.getStateId(); - depth = search.getDepth(); - operation = "backtrack"; - transition = search.getTransition(); - if (transition != null) { - annotation = transition.getAnnotation(); - label = transition.getLabel(); - output = transition.getOutput(); - stateId = transition.getStateId(); + if (debugMode) { + id = search.getStateId(); + depth = search.getDepth(); + transition = search.getTransition(); + detail = null; + + out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition + + " and depth: " + depth + "\n"); } - detail = null; - - out.println("\nThe state is backtracked to state with id: "+id+" Transition: "+ transition+", with depth: "+depth+"##LockValue: "+valueVarLock+", ##ContactValue: "+valueVarContact +"\n"); } @Override public void searchFinished(Search search) { - out.println("----------------------------------- search finished"); + if (debugMode) { + out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n"); + } } } \ No newline at end of file -- 2.34.1