From 035284874a20f0300992229d5c9e94e6e740fa3b Mon Sep 17 00:00:00 2001 From: amiraj Date: Thu, 17 Oct 2019 12:33:53 -0700 Subject: [PATCH] Add required variables of the new listener to the config file. --- main.jpf | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) 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 -- 2.34.1