MACE_PRINT_HOSTNAME_ONLY = 1			# Required for perl to properly print Macekeys
MACE_LOG_LEVEL = 1				# This can be increased for more logging but should not be decreased

USE_UDP_REORDER = 0				# Whether to reorder UDP messages	  
USE_UDP_ERRORS = 0				# Whether to allow UDP errors
USE_NET_ERRORS = 0				# Whether to allow network (e.g. socket) errors 
SIM_NUM_FAILURES = 0				# Number of allowed application failures (e.g. reboots).  Negative numbers = inf.

USE_BEST_FIRST = 0				# Selects between the Search Random Util and Best First Util.  Best First maintains 
	       	 				#    state about the tree, so that when a particular prefix is encountered twice, it 
						#    does not need to be repeated.  This speeds up execution by about 5% but costs 
						#    extra memory.
MACE_PORT=10201	 				# Port for mace to use, unimportant for modelchecking
max_num_steps=80000				# This is the total length of an execution.  It approximates $\inf$
#search_print_mask=0				# "Granularity" of print, says how often (in number of steps) to print state about the 
#search_print_mask=15				#    current execution
search_print_mask=255
#search_print_mask=4095
PRINT_SEARCH_PREFIX=0				# When true, every path that reaches a live state is printed once the live state is
						#    reached.
USE_RANDOM_WALKS=1   				# Whether to use walks after tree search, necessary for liveness properties
USE_GUSTO=1					# Turns off bad things (failures, etc) at random walk part, adds weights to types of 
						#   events (application, network, timer)
USE_STATE_HASHES=0				# Helpful to turn on but may not work.  To test, run MC and search for "non printable" 
						#   in output
NUM_RANDOM_PATHS=40
#MAX_PATHS=20					# Number of paths to search for each path in "binary search" during last nail search
#MAX_PATHS=200
#MAX_PATHS=50000
#MAX_PATHS=1000000

COMPARE_CMC = 0					# For comparison with another modelchecker
RUN_CMC_MEM = 0					# For comparison with another modelchecker

RUN_DIVERGENCE_MONITOR = 0			# Used to detect loops in code (by detecting long-running transitions)
divergence_assert = 1				# Whether to assert on timeout of divergence monitor
divergence_timeout = 30				# Timeout for divergence monitor

CHECKED_SERVICE=HW2     			# Which service to run

#HW2                                            # Number of nodes and all parameters required by tested service
num_nodes=10					# MC needs to know how many nodes to simulate
queue_size=100000				# Used for TCP

SEARCH_DEPTH=5					# Bound for the iterative depth first search

MAX_PATHS = 1000