Skip to content

Commit d9456a2

Browse files
lemmylemmy
committed
Rename German models by abstraction level
Use consistent Data, Control, and CMPWithMutex names across the specifications, TLC and Apalache models, manifest, and documentation. Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
1 parent be9e285 commit d9456a2

17 files changed

Lines changed: 67 additions & 47 deletions

specifications/GermanProtocol/APGerman.cfg renamed to specifications/GermanProtocol/APGermanCMPWithMutex.cfg

File renamed without changes.

specifications/GermanProtocol/APGerman.tla renamed to specifications/GermanProtocol/APGermanCMPWithMutex.tla

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
1-
----------------------------- MODULE APGerman -----------------------------
2-
(* Apalache type annotations for German.tla, applied via INSTANCE so the
1+
------------------------ MODULE APGermanCMPWithMutex ------------------------
2+
(* Apalache type annotations for GermanCMPWithMutex.tla, applied via INSTANCE so the
33
original spec remains free of tool-specific idiosyncrasies.
44
55
Nodes are modelled as an uninterpreted Apalache type (NODE); the abstract
66
environment node Other and the NoNode sentinel share that type so that
77
`curPtr \in NODE \cup {Other, NoNode}` is well typed.
88
99
Run bounded model checking for executions of at most 20 Next steps with:
10-
apalache-mc check --config=APGerman.cfg --length=20 APGerman.tla
11-
This completes in under 10 minutes on a 2021 M1 MacBook.
10+
apalache-mc check --config=APGermanCMPWithMutex.cfg --length=20 APGermanCMPWithMutex.tla
11+
This completes in about 20 minutes on a 2021 M1 MacBook.
1212
*)
1313

1414
CONSTANTS
@@ -39,9 +39,9 @@ VARIABLES
3939
\* @type: NODE;
4040
curPtr
4141

42-
INSTANCE German
42+
INSTANCE GermanCMPWithMutex
4343

44-
\* Concrete values for the constants used by APGerman.cfg.
44+
\* Concrete values for the constants used by APGermanCMPWithMutex.cfg.
4545
NodeVal == { "n1_OF_NODE", "n2_OF_NODE" }
4646
OtherVal == "other_OF_NODE"
4747
NoNodeVal == "noNode_OF_NODE"

specifications/GermanProtocol/APGermanCoherence.cfg renamed to specifications/GermanProtocol/APGermanControl.cfg

File renamed without changes.

specifications/GermanProtocol/APGermanCoherence.tla renamed to specifications/GermanProtocol/APGermanControl.tla

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
1-
------------------------- MODULE APGermanCoherence -------------------------
2-
(* Apalache type annotations for GermanCoherence.tla, applied via INSTANCE so
1+
--------------------------- MODULE APGermanControl ---------------------------
2+
(* Apalache type annotations for GermanControl.tla, applied via INSTANCE so
33
the original spec remains free of tool-specific idiosyncrasies.
44
55
Nodes are modelled as an uninterpreted Apalache type (NODE); the NoNode
66
sentinel shares that type so that `curPtr \in NODE \cup {NoNode}` is well
77
typed.
88
99
Run bounded model checking for executions of at most 20 Next steps with:
10-
apalache-mc check --config=APGermanCoherence.cfg --length=20 APGermanCoherence.tla
11-
This completes in under 10 minutes on a 2021 M1 MacBook.
10+
apalache-mc check --config=APGermanControl.cfg --length=20 APGermanControl.tla
11+
This completes in about 4 minutes on a 2021 M1 MacBook.
1212
*)
1313

1414
CONSTANTS
@@ -37,9 +37,9 @@ VARIABLES
3737
\* @type: NODE;
3838
curPtr
3939

40-
INSTANCE GermanCoherence
40+
INSTANCE GermanControl
4141

42-
\* Concrete values for the constants used by APGermanCoherence.cfg.
42+
\* Concrete values for the constants used by APGermanControl.cfg.
4343
NodeVal == { "n1_OF_NODE", "n2_OF_NODE" }
4444
NoNodeVal == "noNode_OF_NODE"
4545

specifications/GermanProtocol/APGermanWithMutex.cfg renamed to specifications/GermanProtocol/APGermanData.cfg

File renamed without changes.

specifications/GermanProtocol/APGermanWithMutex.tla renamed to specifications/GermanProtocol/APGermanData.tla

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
------------------------- MODULE APGermanWithMutex -------------------------
2-
(* Apalache type annotations for GermanWithMutex.tla, applied via INSTANCE so
1+
----------------------------- MODULE APGermanData -----------------------------
2+
(* Apalache type annotations for GermanData.tla, applied via INSTANCE so
33
the original spec remains free of tool-specific idiosyncrasies.
44
55
Nodes and data values are modelled as uninterpreted Apalache types (NODE,
@@ -8,8 +8,9 @@
88
Apalache does not verify the liveness properties (FairSpec) of the spec.
99
1010
Run bounded model checking for executions of at most 10 Next steps with:
11-
apalache-mc check --config=APGermanWithMutex.cfg --length=10 APGermanWithMutex.tla
12-
This completes quickly on a 2021 M1 MacBook; length 20 takes over 1.5 hours.
11+
apalache-mc check --config=APGermanData.cfg --length=10 APGermanData.tla
12+
This completes in about 20 seconds on a 2021 M1 MacBook; length 20 takes
13+
over 1.5 hours.
1314
*)
1415

1516
CONSTANTS
@@ -46,9 +47,9 @@ VARIABLES
4647
\* @type: DATA;
4748
auxData
4849

49-
INSTANCE GermanWithMutex
50+
INSTANCE GermanData
5051

51-
\* Concrete values for the constants used by APGermanWithMutex.cfg.
52+
\* Concrete values for the constants used by APGermanData.cfg.
5253
NodeVal == { "n1_OF_NODE", "n2_OF_NODE" }
5354
DataVal == { "d1_OF_DATA", "d2_OF_DATA" }
5455
NoDataVal == "noData_OF_DATA"

specifications/GermanProtocol/German.tla renamed to specifications/GermanProtocol/GermanCMPWithMutex.tla

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
-------------------------------- MODULE German --------------------------------
1+
-------------------------- MODULE GermanCMPWithMutex --------------------------
22
CONSTANTS
33
NODE,
44
Other,
@@ -133,7 +133,7 @@ ABS_RecvInvAck ==
133133
\* germanNoMutex.m omits it on purpose -- the deadlock-study model that needs
134134
\* no noninterference lemma -- so it admits the spurious "bogus InvAck from
135135
\* Other" counterexample to mutual exclusion. Dropping this one conjunct makes
136-
\* German.tla bisimilar to germanNoMutex.m.
136+
\* GermanCMPWithMutex.tla bisimilar to germanNoMutex.m.
137137
/\ \A j \in NODE :
138138
/\ cache[j] # "E"
139139
/\ chan2[j] # "GntE"

specifications/GermanProtocol/GermanCoherence.tla renamed to specifications/GermanProtocol/GermanControl.tla

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
---------------------------- MODULE GermanCoherence ----------------------------
1+
----------------------------- MODULE GermanControl -----------------------------
22
CONSTANTS
33
NODE,
44
NoNode

specifications/GermanProtocol/GermanWithMutex.tla renamed to specifications/GermanProtocol/GermanData.tla

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
----------------------------- MODULE GermanWithMutex -----------------------------
1+
------------------------------ MODULE GermanData ------------------------------
22
EXTENDS Naturals, FiniteSets
33

44
CONSTANTS
@@ -158,7 +158,7 @@ Spec == Init /\ [][Next]_vars
158158

159159
-------------------------------------------------------------------------------
160160

161-
Abstract == INSTANCE GermanCoherence WITH
161+
Abstract == INSTANCE GermanControl WITH
162162
cache <- [i \in NODE |-> cache[i].state],
163163
chan1 <- [i \in NODE |-> chan1[i].cmd],
164164
chan2 <- [i \in NODE |-> chan2[i].cmd],

specifications/GermanProtocol/MCGerman.cfg renamed to specifications/GermanProtocol/MCGermanCMPWithMutex.cfg

File renamed without changes.

0 commit comments

Comments
 (0)