---- MODULE MC ----
EXTENDS lock_free_stack_ABA, TLC

\* CONSTANT definitions @modelParameterConstants:1MAX_STACK_SIZE
const_1555008012169145000 == 
2
----

\* CONSTANT definitions @modelParameterConstants:2MAX_ITER_THR_A
const_1555008012169146000 == 
3
----

\* CONSTANT definitions @modelParameterConstants:3MAX_ITER_THR_B
const_1555008012169147000 == 
2
----

\* SPECIFICATION definition @modelBehaviorSpec:0
spec_1555008012169149000 ==
Spec
----
=============================================================================
\* Modification History
\* Created Thu Apr 11 14:40:12 EDT 2019 by gene