= Welcome to GMC = 

== Multi-Core Model Checking ==

Stateful classes in CIVL that may not be necessary to be stateful:[[BR]]

'''edu.udel.cis.vsl.civl.kripke.semantics.CommonEvaluator.java'''[[BR]]
boundVariableStack [[BR]]
originalState [[BR]]
originalPid [[BR]]
valueAtOrRemoteCount [[BR]]
''Possible solution'': spawn an EvaluatorWorker[[BR]][[BR]]
'''edu.udel.cis.vsl.civl.semantics.common.CommonExecutor.java'''[[BR]]
numSteps[[BR]]
''Possible solution'': Each thread has its own copy of Executor.[[BR]][[BR]]
'''edu.udel.cis.vsl.civl.kripke.common.CommonStateManager.java'''[[BR]]
maxProcs[[BR]]
maxCanonicId[[BR]]
numStatesExplored[[BR]]
stack[[BR]]
expandedStateIDs[[BR]]
ignoredHeapErrors[[BR]]

'''edu.udel.cis.vsl.civl.state.common.immutable.ImmutableStateFactory.java'''[[BR]]
processMap[[BR]]
scopeMap[[BR]]
stateCount[[BR]]
stateMap[[BR]]
savedCanonicStates[[BR]]
dyscopeSubMap[[BR]]

'''edu.udel.cis.vsl.sarl.object.common.CommonObjectFactory.java'''[[BR]]
objectMap[[BR]]
objectList[[BR]][[BR]]
'''edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverse.java'''[[BR]]
validCount[[BR]]
proverValidCount[[BR]]
int2bvConstants[[BR]][[BR]]
'''edu.udel.cis.vsl.civl.model.common.CommonModelFactory.java'''[[BR]]
inputVariables[[BR]]
domSizeVariableId[[BR]]
parProcsVariableId[[BR]]
anonymousVariableId[[BR]]
conditionalExpressionCounter[[BR]]
conditionalExpressions[[BR]]
identifiers[[BR]]
locationID[[BR]]
processValues[[BR]]
scopeID[[BR]]
scopeValues[[BR]]

'''edu.udel.cis.vsl.civl.model.common.ModelBuilderWorker.java'''[[BR]]
anonymousStructCounter[[BR]]
timeLibIncluded?[[BR]]
hasNextTimeCountCall?[[BR]]
parProcFunctions[[BR]]
runProcFunctions[[BR]]
bundleableEncountered[[BR]]
bundleableTypeList[[BR]]

'''edu.udel.cis.vsl.civl.semantics.common.UFExtender.java'''[[BR]]
''Possible Solution'':Initialize the field uninterpretedFunctions exactly once in constructor with all known abstract functions and never change again.[[BR]]
[[BR]]
'''edu.udel.cis.vsl.civl.kripke.common.OutputCollector.java'''