From: amiraj Date: Thu, 17 Oct 2019 19:33:53 +0000 (-0700) Subject: Add required variables of the new listener to the config file. X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=035284874a20f0300992229d5c9e94e6e740fa3b;p=jpf-core.git Add required variables of the new listener to the config file. --- diff --git a/main.jpf b/main.jpf index 89d4f48..cfef551 100644 --- a/main.jpf +++ b/main.jpf @@ -1,11 +1,11 @@ target = main -#target = Rand # 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.StateReducerOld #listener=gov.nasa.jpf.listener.VariableConflictTracker,gov.nasa.jpf.listener.StateReducer +listener=gov.nasa.jpf.listener.ConflictTracker # Potentially conflicting variables # Alarms @@ -28,21 +28,26 @@ variables=currentLock #variables=valve,valveLatestValue # Cameras #variables=image,alarmState +# Location +#variables=locationMode # Potentially conflicting apps (we default to App1 and App2 for now) apps=App1,App2 +# Writer classes with manual input to detect direct-direct interactions +manualClasses=appTouch,AeonKeyFob,Button,NfcTouch,ThreeAxis + # Tracking the location.mode variable conflict #track_location_var_conflict=true # Debug mode for StateReducer -debug_state_transition=true -activate_state_reduction=true +#debug_state_transition=true +#activate_state_reduction=true # Timeout in minutes (default is 0 which means no timeout) timeout=30 -#search.class = gov.nasa.jpf.search.heuristic.RandomHeuristic +search.class = gov.nasa.jpf.search.heuristic.RandomHeuristic #search.heuristic.beam_search=true #search.class = gov.nasa.jpf.search.heuristic.UserHeuristic #search.class = gov.nasa.jpf.search.heuristic.BFSHeuristic