= 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]]
count[[BR]]
ErrorSet[[BR]][[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]]
count[[BR]][[BR]]
'''edu.udel.cis.vsl.civl.model.common.CommonModelFactory.java'''[[BR]][[BR]]
'''edu.udel.cis.vsl.civl.model.common.ModelBuilderWorker.java'''[[BR]][[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'''