Skip to content

Commit 8b1a53f

Browse files
ahelwerahelwer
committed
Translate specs to unicode for baseline
Signed-off-by: Andrew Helwer <[email protected]>
1 parent 05511f3 commit 8b1a53f

File tree

292 files changed

+17461
-17518
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

292 files changed

+17461
-17518
lines changed

‎specifications/Bakery-Boulangerie/Bakery.tla

Lines changed: 232 additions & 232 deletions
Large diffs are not rendered by default.

‎specifications/Bakery-Boulangerie/Boulanger.tla

Lines changed: 257 additions & 257 deletions
Large diffs are not rendered by default.

‎specifications/Bakery-Boulangerie/MCBakery.tla

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
---------------------------- MODULE MCBakery --------------------------------
22
EXTENDS Bakery
33
CONSTANT MaxNat
4-
ASSUME MaxNat \in Nat
5-
NatOverride == 0 .. MaxNat
4+
ASSUME MaxNat ∈ ℕ
5+
NatOverride ≜ 0 ‥ MaxNat
66
=============================================================================
7-

‎specifications/Bakery-Boulangerie/MCBoulanger.tla

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,7 @@
11
--------------------------- MODULE MCBoulanger ------------------------------
22
EXTENDS Boulanger
33
CONSTANT MaxNat
4-
ASSUME MaxNat \in Nat
5-
NatOverride == 0 .. MaxNat
6-
StateConstraint == \A process \in Procs : num[process] < MaxNat
4+
ASSUME MaxNat ∈ ℕ
5+
NatOverride ≜ 0 ‥ MaxNat
6+
StateConstraint ≜ ∀ process ∈ Procs : num[process] < MaxNat
77
=============================================================================
8-

‎specifications/CarTalkPuzzle/CarTalkPuzzle.tla

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -42,8 +42,8 @@ CONSTANTS N, P
4242
(* such that P(v) is true, if such a value exists. *)
4343
(***************************************************************************)
4444
RECURSIVE Sum(_,_)
45-
Sum(f,S) == IF S = {} THEN 0
46-
ELSE LET x == CHOOSE x \in S : TRUE
45+
Sum(f,S) ≜ IF S = {} THEN 0
46+
ELSE LET x ≜ CHOOSE x ∈ S : TRUE
4747
IN f[x] + Sum(f, S \ {x})
4848

4949
(***************************************************************************)
@@ -62,8 +62,8 @@ Sum(f,S) == IF S = {} THEN 0
6262
(* In TLA+, [S -> T] is the set of all functions with domain S and range a *)
6363
(* subset of T. \A and \E are the universal and existential quantifiers. *)
6464
(***************************************************************************)
65-
Break == {B \in [1..P -> 1..N] : Sum(B, 1..P) = N
66-
/\ \A i \in 1..P : \A j \in (i+1)..P : B[i] =< B[j]}
65+
Break ≜ {B ∈ [1‥P → 1‥N] : Sum(B, 1‥P) = N
66+
∧ ∀ i ∈ 1‥P : ∀ j ∈ (i+1)‥P : B[i] ≤ B[j]}
6767

6868
(***************************************************************************)
6969
(* To weigh a quantity of corn, we can put some of the weights on the same *)
@@ -74,22 +74,22 @@ Break == {B \in [1..P -> 1..N] : Sum(B, 1..P) = N
7474
(* piece numbers (numbers in 1..P), so Sum(B, S) is the weight of the *)
7575
(* pieces in S. *)
7676
(***************************************************************************)
77-
IsRepresentation(w, B, S, T) == S \cap T = {}
78-
/\ w + Sum(B,S) = Sum(B,T)
77+
IsRepresentation(w, B, S, T) ≜ S ∩ T = {}
78+
∧ w + Sum(B,S) = Sum(B,T)
7979
(***************************************************************************)
8080
(* I now define IsSolution(B) to be true iff break B solves the problem, *)
8181
(* meaning that it can be used to balance any weight in 1..N. *)
8282
(* *)
8383
(* SUBSET S is the set of all subsets of S (the power set of S). *)
8484
(***************************************************************************)
85-
IsSolution(B) == \A w \in 1..N :
86-
\E S, T \in SUBSET (1..P) : IsRepresentation(w, B, S, T)
85+
IsSolution(B) ≜ ∀ w ∈ 1‥N :
86+
∃ S, T ∈ SUBSET (1‥P) : IsRepresentation(w, B, S, T)
8787

8888
(***************************************************************************)
8989
(* I define AllSolutions to be the set of all breaks B that solve the *)
9090
(* problem. *)
9191
(***************************************************************************)
92-
AllSolutions == { B \in Break : IsSolution(B) }
92+
AllSolutions ≜ { B ∈ Break : IsSolution(B) }
9393

9494
(***************************************************************************)
9595
(* We can now have TLC compute the solution to the problem as follows. We *)
@@ -148,13 +148,13 @@ AllSolutions == { B \in Break : IsSolution(B) }
148148
(* [w \in 1..N |-> F(w)] is the N tuple with F(i) as element i. *)
149149
(* *)
150150
(***************************************************************************)
151-
ExpandSolutions ==
152-
LET PiecesFor(w, B) == CHOOSE ST \in (SUBSET (1..P)) \X (SUBSET (1..P)) :
151+
ExpandSolutions ≜
152+
LET PiecesFor(w, B) ≜ CHOOSE ST ∈ (SUBSET (1‥P)) × (SUBSET (1‥P)) :
153153
IsRepresentation(w, B, ST[1], ST[2])
154-
Image(S, B) == {B[x] : x \in S}
155-
SolutionFor(w, B) == << w,
154+
Image(S, B) ≜ {B[x] : x ∈ S}
155+
SolutionFor(w, B) ≜ ⟨ w,
156156
Image(PiecesFor(w, B)[1], B),
157-
Image(PiecesFor(w, B)[2], B) >>
158-
IN { [w \in 1..N |-> SolutionFor(w, B)] : B \in AllSolutions }
157+
Image(PiecesFor(w, B)[2], B) ⟩
158+
IN { [w ∈ 1‥N ↦ SolutionFor(w, B)] : B ∈ AllSolutions }
159159
===============================================================================
160-
Created by Leslie Lamport on 26 October 2011
160+
Created by Leslie Lamport on 26 October 2011

‎specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_1/CarTalkPuzzle.tla

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -42,8 +42,8 @@ CONSTANTS N, P
4242
(* such that P(v) is true, if such a value exists. *)
4343
(***************************************************************************)
4444
RECURSIVE Sum(_,_)
45-
Sum(f,S) == IF S = {} THEN 0
46-
ELSE LET x == CHOOSE x \in S : TRUE
45+
Sum(f,S) ≜ IF S = {} THEN 0
46+
ELSE LET x ≜ CHOOSE x ∈ S : TRUE
4747
IN f[x] + Sum(f, S \ {x})
4848

4949
(***************************************************************************)
@@ -62,8 +62,8 @@ Sum(f,S) == IF S = {} THEN 0
6262
(* In TLA+, [S -> T] is the set of all functions with domain S and range a *)
6363
(* subset of T. \A and \E are the universal and existential quantifiers. *)
6464
(***************************************************************************)
65-
Break == {B \in [1..P -> 1..N] : Sum(B, 1..P) = N
66-
/\ \A i \in 1..P : \A j \in (i+1)..P : B[i] =< B[j]}
65+
Break ≜ {B ∈ [1‥P → 1‥N] : Sum(B, 1‥P) = N
66+
∧ ∀ i ∈ 1‥P : ∀ j ∈ (i+1)‥P : B[i] ≤ B[j]}
6767

6868
(***************************************************************************)
6969
(* To weigh a quantity of corn, we can put some of the weights on the same *)
@@ -74,16 +74,16 @@ Break == {B \in [1..P -> 1..N] : Sum(B, 1..P) = N
7474
(* piece numbers (numbers in 1..P), so Sum(B, S) is the weight of the *)
7575
(* pieces in S. *)
7676
(***************************************************************************)
77-
IsRepresentation(w, B, S, T) == S \cap T = {}
78-
/\ w + Sum(B,S) = Sum(B,T)
77+
IsRepresentation(w, B, S, T) ≜ S ∩ T = {}
78+
∧ w + Sum(B,S) = Sum(B,T)
7979
(***************************************************************************)
8080
(* I now define IsSolution(B) to be true iff break B solves the problem, *)
8181
(* meaning that it can be used to balance any weight in 1..N. *)
8282
(* *)
8383
(* SUBSET S is the set of all subsets of S (the power set of S). *)
8484
(***************************************************************************)
85-
IsSolution(B) == \A w \in 1..N :
86-
\E S, T \in SUBSET (1..P) : IsRepresentation(w, B, S, T)
85+
IsSolution(B) ≜ ∀ w ∈ 1‥N :
86+
∃ S, T ∈ SUBSET (1‥P) : IsRepresentation(w, B, S, T)
8787
==========
8888
(***************************************************************************)
8989
(* I define AllSolutions to be the set of all breaks B that solve the *)
@@ -155,4 +155,4 @@ ExpandSolutions ==
155155
Image(PiecesFor(w, B)[2], B) >>
156156
IN { [w \in 1..N |-> SolutionFor(w, B)] : B \in AllSolutions }
157157
===============================================================================
158-
Created by Leslie Lamport on 26 October 2011
158+
Created by Leslie Lamport on 26 October 2011

‎specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_1/MC.tla

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,26 +2,26 @@
22
EXTENDS CarTalkPuzzle, TLC
33

44
\* CONSTANT definitions @modelParameterConstants:0N
5-
const_131986752160123000 ==
5+
const_131986752160123000 ≜
66
40
77
----
88

99
\* CONSTANT definitions @modelParameterConstants:1P
10-
const_131986752161624000 ==
10+
const_131986752161624000 ≜
1111
4
1212
----
1313

1414
\* Constant expression definition @modelExpressionEval
15-
const_expr_131986752163225000 ==
15+
const_expr_131986752163225000 ≜
1616
\* ExpandSolutions
1717
\* CHOOSE B \in Break : IsSolution(B)
18-
<<3^5 - 1, 40 + 3^4>>
18+
⟨3^5 - 1, 40 + 3^4⟩
1919
----
2020

2121
\* Constant expression ASSUME statement @modelExpressionEval
22-
ASSUME PrintT(<<"$!@$!@$!@$!@$!",const_expr_131986752163225000>>)
22+
ASSUME PrintT(⟨"$!@$!@$!@$!@$!",const_expr_131986752163225000⟩)
2323
----
2424

2525
=============================================================================
2626
\* Modification History
27-
\* Created Fri Oct 28 22:52:01 PDT 2011 by lamport
27+
\* Created Fri Oct 28 22:52:01 PDT 2011 by lamport

‎specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_2/CarTalkPuzzle.tla

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -42,8 +42,8 @@ CONSTANTS N, P
4242
(* such that P(v) is true, if such a value exists. *)
4343
(***************************************************************************)
4444
RECURSIVE Sum(_,_)
45-
Sum(f,S) == IF S = {} THEN 0
46-
ELSE LET x == CHOOSE x \in S : TRUE
45+
Sum(f,S) ≜ IF S = {} THEN 0
46+
ELSE LET x ≜ CHOOSE x ∈ S : TRUE
4747
IN f[x] + Sum(f, S \ {x})
4848

4949
(***************************************************************************)
@@ -62,8 +62,8 @@ Sum(f,S) == IF S = {} THEN 0
6262
(* In TLA+, [S -> T] is the set of all functions with domain S and range a *)
6363
(* subset of T. \A and \E are the universal and existential quantifiers. *)
6464
(***************************************************************************)
65-
Break == {B \in [1..P -> 1..N] : Sum(B, 1..P) = N
66-
/\ \A i \in 1..P : \A j \in (i+1)..P : B[i] =< B[j]}
65+
Break ≜ {B ∈ [1‥P → 1‥N] : Sum(B, 1‥P) = N
66+
∧ ∀ i ∈ 1‥P : ∀ j ∈ (i+1)‥P : B[i] ≤ B[j]}
6767

6868
(***************************************************************************)
6969
(* To weigh a quantity of corn, we can put some of the weights on the same *)
@@ -74,22 +74,22 @@ Break == {B \in [1..P -> 1..N] : Sum(B, 1..P) = N
7474
(* piece numbers (numbers in 1..P), so Sum(B, S) is the weight of the *)
7575
(* pieces in S. *)
7676
(***************************************************************************)
77-
IsRepresentation(w, B, S, T) == S \cap T = {}
78-
/\ w + Sum(B,S) = Sum(B,T)
77+
IsRepresentation(w, B, S, T) ≜ S ∩ T = {}
78+
∧ w + Sum(B,S) = Sum(B,T)
7979
(***************************************************************************)
8080
(* I now define IsSolution(B) to be true iff break B solves the problem, *)
8181
(* meaning that it can be used to balance any weight in 1..N. *)
8282
(* *)
8383
(* SUBSET S is the set of all subsets of S (the power set of S). *)
8484
(***************************************************************************)
85-
IsSolution(B) == \A w \in 1..N :
86-
\E S, T \in SUBSET (1..P) : IsRepresentation(w, B, S, T)
85+
IsSolution(B) ≜ ∀ w ∈ 1‥N :
86+
∃ S, T ∈ SUBSET (1‥P) : IsRepresentation(w, B, S, T)
8787

8888
(***************************************************************************)
8989
(* I define AllSolutions to be the set of all breaks B that solve the *)
9090
(* problem. *)
9191
(***************************************************************************)
92-
AllSolutions == { B \in Break : IsSolution(B) }
92+
AllSolutions ≜ { B ∈ Break : IsSolution(B) }
9393

9494
(***************************************************************************)
9595
(* We can now have TLC compute the solution to the problem as follows. We *)
@@ -146,13 +146,13 @@ AllSolutions == { B \in Break : IsSolution(B) }
146146
(* [w \in 1..N |-> F(w)] is the N tuple with F(i) as element i. *)
147147
(* *)
148148
(***************************************************************************)
149-
ExpandSolutions ==
150-
LET PiecesFor(w, B) == CHOOSE ST \in (SUBSET (1..P)) \X (SUBSET (1..P)) :
149+
ExpandSolutions ≜
150+
LET PiecesFor(w, B) ≜ CHOOSE ST ∈ (SUBSET (1‥P)) × (SUBSET (1‥P)) :
151151
IsRepresentation(w, B, ST[1], ST[2])
152-
Image(S, B) == {B[x] : x \in S}
153-
SolutionFor(w, B) == << w,
152+
Image(S, B) ≜ {B[x] : x ∈ S}
153+
SolutionFor(w, B) ≜ ⟨ w,
154154
Image(PiecesFor(w, B)[1], B),
155-
Image(PiecesFor(w, B)[2], B) >>
156-
IN { [w \in 1..N |-> SolutionFor(w, B)] : B \in AllSolutions }
155+
Image(PiecesFor(w, B)[2], B) ⟩
156+
IN { [w ∈ 1‥N ↦ SolutionFor(w, B)] : B ∈ AllSolutions }
157157
===============================================================================
158-
Created by Leslie Lamport on 26 October 2011
158+
Created by Leslie Lamport on 26 October 2011

‎specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_2/MC.tla

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2,24 +2,24 @@
22
EXTENDS CarTalkPuzzle, TLC
33

44
\* CONSTANT definitions @modelParameterConstants:0N
5-
const_131965207585635000 ==
5+
const_131965207585635000 ≜
66
15
77
----
88

99
\* CONSTANT definitions @modelParameterConstants:1P
10-
const_131965207587136000 ==
10+
const_131965207587136000 ≜
1111
4
1212
----
1313

1414
\* Constant expression definition @modelExpressionEval
15-
const_expr_131965207588737000 ==
15+
const_expr_131965207588737000 ≜
1616
AllSolutions
1717
----
1818

1919
\* Constant expression ASSUME statement @modelExpressionEval
20-
ASSUME PrintT(<<"$!@$!@$!@$!@$!",const_expr_131965207588737000>>)
20+
ASSUME PrintT(⟨"$!@$!@$!@$!@$!",const_expr_131965207588737000⟩)
2121
----
2222

2323
=============================================================================
2424
\* Modification History
25-
\* Created Wed Oct 26 11:01:15 PDT 2011 by lamport
25+
\* Created Wed Oct 26 11:01:15 PDT 2011 by lamport

‎specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_3/CarTalkPuzzle.tla

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -42,8 +42,8 @@ CONSTANTS N, P
4242
(* such that P(v) is true, if such a value exists. *)
4343
(***************************************************************************)
4444
RECURSIVE Sum(_,_)
45-
Sum(f,S) == IF S = {} THEN 0
46-
ELSE LET x == CHOOSE x \in S : TRUE
45+
Sum(f,S) ≜ IF S = {} THEN 0
46+
ELSE LET x ≜ CHOOSE x ∈ S : TRUE
4747
IN f[x] + Sum(f, S \ {x})
4848

4949
(***************************************************************************)
@@ -62,8 +62,8 @@ Sum(f,S) == IF S = {} THEN 0
6262
(* In TLA+, [S -> T] is the set of all functions with domain S and range a *)
6363
(* subset of T. \A and \E are the universal and existential quantifiers. *)
6464
(***************************************************************************)
65-
Break == {B \in [1..P -> 1..N] : Sum(B, 1..P) = N
66-
/\ \A i \in 1..P : \A j \in (i+1)..P : B[i] =< B[j]}
65+
Break ≜ {B ∈ [1‥P → 1‥N] : Sum(B, 1‥P) = N
66+
∧ ∀ i ∈ 1‥P : ∀ j ∈ (i+1)‥P : B[i] ≤ B[j]}
6767

6868
(***************************************************************************)
6969
(* To weigh a quantity of corn, we can put some of the weights on the same *)
@@ -74,22 +74,22 @@ Break == {B \in [1..P -> 1..N] : Sum(B, 1..P) = N
7474
(* piece numbers (numbers in 1..P), so Sum(B, S) is the weight of the *)
7575
(* pieces in S. *)
7676
(***************************************************************************)
77-
IsRepresentation(w, B, S, T) == S \cap T = {}
78-
/\ w + Sum(B,S) = Sum(B,T)
77+
IsRepresentation(w, B, S, T) ≜ S ∩ T = {}
78+
∧ w + Sum(B,S) = Sum(B,T)
7979
(***************************************************************************)
8080
(* I now define IsSolution(B) to be true iff break B solves the problem, *)
8181
(* meaning that it can be used to balance any weight in 1..N. *)
8282
(* *)
8383
(* SUBSET S is the set of all subsets of S (the power set of S). *)
8484
(***************************************************************************)
85-
IsSolution(B) == \A w \in 1..N :
86-
\E S, T \in SUBSET (1..P) : IsRepresentation(w, B, S, T)
85+
IsSolution(B) ≜ ∀ w ∈ 1‥N :
86+
∃ S, T ∈ SUBSET (1‥P) : IsRepresentation(w, B, S, T)
8787

8888
(***************************************************************************)
8989
(* I define AllSolutions to be the set of all breaks B that solve the *)
9090
(* problem. *)
9191
(***************************************************************************)
92-
AllSolutions == { B \in Break : IsSolution(B) }
92+
AllSolutions ≜ { B ∈ Break : IsSolution(B) }
9393
=========
9494
(***************************************************************************)
9595
(* We can now have TLC compute the solution to the problem as follows. We *)
@@ -155,4 +155,4 @@ ExpandSolutions ==
155155
Image(PiecesFor(w, B)[2], B) >>
156156
IN { [w \in 1..N |-> SolutionFor(w, B)] : B \in AllSolutions }
157157
===============================================================================
158-
Created by Leslie Lamport on 26 October 2011
158+
Created by Leslie Lamport on 26 October 2011

‎specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_3/MC.tla

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2,24 +2,24 @@
22
EXTENDS CarTalkPuzzle, TLC
33

44
\* CONSTANT definitions @modelParameterConstants:0N
5-
const_131986786702435000 ==
5+
const_131986786702435000 ≜
66
121
77
----
88

99
\* CONSTANT definitions @modelParameterConstants:1P
10-
const_131986786704036000 ==
10+
const_131986786704036000 ≜
1111
5
1212
----
1313

1414
\* Constant expression definition @modelExpressionEval
15-
const_expr_131986786705637000 ==
15+
const_expr_131986786705637000 ≜
1616
AllSolutions
1717
----
1818

1919
\* Constant expression ASSUME statement @modelExpressionEval
20-
ASSUME PrintT(<<"$!@$!@$!@$!@$!",const_expr_131986786705637000>>)
20+
ASSUME PrintT(⟨"$!@$!@$!@$!@$!",const_expr_131986786705637000⟩)
2121
----
2222

2323
=============================================================================
2424
\* Modification History
25-
\* Created Fri Oct 28 22:57:47 PDT 2011 by lamport
25+
\* Created Fri Oct 28 22:57:47 PDT 2011 by lamport

0 commit comments

Comments
 (0)