forked from tlaplus/Examples
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathMC.tla
More file actions
26 lines (21 loc) · 638 Bytes
/
MC.tla
File metadata and controls
26 lines (21 loc) · 638 Bytes
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
---- MODULE MC ----
EXTENDS SingleLaneBridge, TLC
\* CONSTANT definitions @modelParameterConstants:0CarsRight
const_1615720459299211000 ==
{"r1","r2"}
----
\* CONSTANT definitions @modelParameterConstants:1CarsLeft
const_1615720459299212000 ==
{"l1","l2"}
----
\* CONSTANT definitions @modelParameterConstants:2Bridge
const_1615720459299213000 ==
{4,5}
----
\* CONSTANT definitions @modelParameterConstants:3Positions
const_1615720459299214000 ==
{1,2,3,4,5,6,7,8}
----
=============================================================================
\* Modification History
\* Last modified Sun Oct 10 22:023:42 CEST 2021 by youne