---- MODULE MC ----
EXTENDS Fischer, TLC

\* MV CONSTANT declarations@modelParameterConstants
CONSTANTS
p1, p2, p3
----

\* MV CONSTANT definitions Procs
const_1728918948504241000 == 
{p1, p2, p3}
----

\* CONSTANT definitions @modelParameterConstants:1epsilon
const_1728918948504242000 == 
3
----

\* CONSTANT definitions @modelParameterConstants:2Times
const_1728918948504243000 == 
0..8
----

\* CONSTANT definitions @modelParameterConstants:3delta
const_1728918948504244000 == 
2
----

=============================================================================
\* Modification History
\* Created Mon Oct 14 17:15:48 CEST 2024 by lamport
