projects
/
jpf-core.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
3ff801c
)
Add required variables of the new listener to the config file.
author
amiraj
<amiraj.95@uci.edu>
Thu, 17 Oct 2019 19:33:53 +0000
(12:33 -0700)
committer
amiraj
<amiraj.95@uci.edu>
Thu, 17 Oct 2019 19:33:53 +0000
(12:33 -0700)
main.jpf
patch
|
blob
|
history
diff --git
a/main.jpf
b/main.jpf
index 89d4f48473ce962affae7a169ecfaf8c71a4167e..cfef551bc29338a9abf72d472ea41f4975d12145 100644
(file)
--- a/
main.jpf
+++ b/
main.jpf
@@
-1,11
+1,11
@@
target = main
target = main
-#target = Rand
# This is the listener that can detect variable write-after-write conflicts
# 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.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
# Potentially conflicting variables
# Alarms
@@
-28,21
+28,26
@@
variables=currentLock
#variables=valve,valveLatestValue
# Cameras
#variables=image,alarmState
#variables=valve,valveLatestValue
# Cameras
#variables=image,alarmState
+# Location
+#variables=locationMode
# Potentially conflicting apps (we default to App1 and App2 for now)
apps=App1,App2
# 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
# 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
# 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
#search.heuristic.beam_search=true
#search.class = gov.nasa.jpf.search.heuristic.UserHeuristic
#search.class = gov.nasa.jpf.search.heuristic.BFSHeuristic