X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=main.jpf;h=0293eb94063e37278851ba893921fc18c0ec0909;hp=1742858e130baaffe384f5c7351e02d818030057;hb=9a81d9c1be0c32296b1553a2a772951336c130a1;hpb=fe469f1f483c9d9fa6513c4391425553dc7cf605 diff --git a/main.jpf b/main.jpf index 1742858..0293eb9 100644 --- a/main.jpf +++ b/main.jpf @@ -5,12 +5,9 @@ target = main #listener=gov.nasa.jpf.listener.StateReducer #listener=gov.nasa.jpf.listener.StateReducerOld #listener=gov.nasa.jpf.listener.VariableConflictTracker,gov.nasa.jpf.listener.StateReducer -#listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducer -##listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.StateReducer -##listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.DPORStateReducer -listener=gov.nasa.jpf.listener.ConflictTrackerOld +#listener=gov.nasa.jpf.listener.ConflictTrackerOld #listener=gov.nasa.jpf.listener.DPORStateReducer -#listener=gov.nasa.jpf.listener.DPORStateReducer,gov.nasa.jpf.listener.ConflictTrackerOld +listener=gov.nasa.jpf.listener.DPORStateReducer,gov.nasa.jpf.listener.ConflictTrackerOld # Potentially conflicting variables # Alarms @@ -26,11 +23,11 @@ variables=currentLock #variables=colorChanged,currentHue,currentSaturation,currentLevel,currentSwitch,colorTemperature # Dimmers #variables=currentSwitch,currentLevel -# Speeches +# Speech Synthesizers #variables=level,oneUser # Music players #variables=status,duration,level,trackDescription,trackData,mute -# Relay switch +# Relay switches #variables=currentSwitch # Valves #variables=valve,valveLatestValue @@ -44,14 +41,16 @@ apps=App1,App2 # Debug mode for ConflictTracker # We do not report any conflicts if the value is true -debug_mode=true +#debug_mode=true # Debug mode for StateReducer printout_state_transition=true -activate_state_reduction=false +#activate_state_reduction=false +file_output=moreStatistics # Timeout in minutes (default is 0 which means no timeout) -timeout=1440 +#timeout=1440 +timeout=30 #search.class = gov.nasa.jpf.search.heuristic.RandomHeuristic #search.heuristic.beam_search=true