= 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]]

'''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]]

'''edu.udel.cis.vsl.civl.model.common.CommonModelFactory.java'''[[BR]]
processValues[[BR]]
scopeValues[[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'''[[BR]]

/CIVL/src/edu/udel/cis/vsl/civl/model/common/type/CommonType.java[[BR]]
dynamicType[[BR]]

/SARL/src/edu/udel/cis/vsl/sarl/reason/common/CommonReasoner.java[[BR]]
prover[[BR]]
validityCache[[BR]]

/SARL/src/edu/udel/cis/vsl/sarl/reason/common/SimpleReasoner.java[[BR]]
validityCache[[BR]]

/CIVL/src/edu/udel/cis/vsl/civl/semantics/common/CommonExecutor.java ? (setValue, setLocation)[[BR]]
stateFactory[[BR]]

/CIVL/src/edu/udel/cis/vsl/civl/state/common/immutable/ImmutableState.java (can be removed)[[BR]]
snapshotsQueues[[BR]]

/SARL/src/edu/udel/cis/vsl/sarl/number/real/RealNumberFactory.java[[BR]]
integerMap[[BR]]
rationalMap[[BR]]

/SARL/src/edu/udel/cis/vsl/sarl/reason/common/CommonReasonerFactory.java[[BR]]
reasonerCache[[BR]]

/SARL/src/edu/udel/cis/vsl/sarl/reason/common/ContextMinimizingReasonerFactory.java[[BR]]
reasonerMap[[BR]]

/SARL/src/edu/udel/cis/vsl/sarl/ideal/simplify/IdealSimplifier.java[[BR]]
fullContext[[BR]]
substitutionMap[[BR]]

/SARL/src/edu/udel/cis/vsl/sarl/preuniverse/common/ExpressionSubstituter.java[[BR]]
cache[[BR]]

/SARL/src/edu/udel/cis/vsl/sarl/reason/common/ContextMinimizingReasoner.java[[BR]]
validityCache[[BR]]
prover[[BR]]

/GMC/src/edu/udel/cis/vsl/gmc/ErrorLog.java[[BR]]
minimalCounterexampleSize[[BR]]
entryMap[[BR]]
searchTruncated[[BR]]

/SARL/src/edu/udel/cis/vsl/sarl/simplify/common/CommonContextPartition.java[[BR]]
minimalContextMap[[BR]]

/CIVL/src/edu/udel/cis/vsl/civl/semantics/common/CommonLibraryExecutorLoader.java[[BR]]
libraryExecutorCache[[BR]]

/CIVL/src/edu/udel/cis/vsl/civl/semantics/common/CommonLibraryEvaluatorLoader.java[[BR]]
libraryEvaluatorCache[[BR]]

/CIVL/src/edu/udel/cis/vsl/civl/dynamic/common/CommonSymbolicUtility.java[[BR]]
typeExpressionMap[[BR]]
typeExpressionMap2[[BR]]

/CIVL/src/edu/udel/cis/vsl/civl/kripke/common/CommonLibraryEnablerLoader.java[[BR]]
libraryEnablerCache[[BR]]