Skip to content
Snippets Groups Projects
Commit 0acf8cdd authored by Michael Leuschel's avatar Michael Leuschel
Browse files

improve DieHard visualisation 


Signed-off-by: default avatarMichael Leuschel <leuschel@uni-duesseldorf.de>
parent ec48f3d9
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Jars/DieHard.tla
+ 8
− 0
View file @ 0acf8cdd
...@@ -69,15 +69,19 @@ Init == /\ big = 0 ...@@ -69,15 +69,19 @@ Init == /\ big = 0
(***************************************************************************) (***************************************************************************)
FillSmallJug == /\ small' = 3 FillSmallJug == /\ small' = 3
/\ big' = big /\ big' = big
/\ small < 3 \* added for VisB
FillBigJug == /\ big' = 5 FillBigJug == /\ big' = 5
/\ small' = small /\ small' = small
/\ big < 5 \* added for VisB
EmptySmallJug == /\ small' = 0 EmptySmallJug == /\ small' = 0
/\ big' = big /\ big' = big
/\ small > 0 \* added for VisB
EmptyBigJug == /\ big' = 0 EmptyBigJug == /\ big' = 0
/\ small' = small /\ small' = small
/\ big > 0 \* added for VisB
(***************************************************************************) (***************************************************************************)
(* We now consider pouring water from one jug into another. Again, since *) (* We now consider pouring water from one jug into another. Again, since *)
...@@ -98,9 +102,13 @@ Min(m,n) == IF m < n THEN m ELSE n ...@@ -98,9 +102,13 @@ Min(m,n) == IF m < n THEN m ELSE n
(***************************************************************************) (***************************************************************************)
SmallToBig == /\ big' = Min(big + small, 5) SmallToBig == /\ big' = Min(big + small, 5)
/\ small' = small - (big' - big) /\ small' = small - (big' - big)
/\ small > 0 \* added for VisB
/\ big < 5 \* added for VisB
BigToSmall == /\ small' = Min(big + small, 3) BigToSmall == /\ small' = Min(big + small, 3)
/\ big' = big - (small' - small) /\ big' = big - (small' - small)
/\ big > 0 \* added for VisB
/\ small < 3 \* added for VisB
(***************************************************************************) (***************************************************************************)
(* We define the next-state relation, which I like to call Next. A Next *) (* We define the next-state relation, which I like to call Next. A Next *)
......
Jars/DieHard_tla.json
+ 20
− 4
View file @ 0acf8cdd
...@@ -97,6 +97,22 @@ ...@@ -97,6 +97,22 @@
"id": "goal", "id": "goal",
"attr": "x2", "attr": "x2",
"value": "IF maxf(3) > maxf(5) THEN 48 ELSE 153 END" "value": "IF maxf(3) > maxf(5) THEN 48 ELSE 153 END"
},
{
"id": "fill_%0",
"attr": "stroke",
"value": "IF level(%0) = %0 THEN \"white\" ELSE \"black\" END",
"repeat": [
["3"], ["5"]
]
},
{
"id": "empty_%0",
"attr": "stroke",
"value": "IF level(%0) = 0 THEN \"white\" ELSE \"black\" END",
"repeat": [
["3"], ["5"]
]
} }
], ],
...@@ -104,13 +120,13 @@ ...@@ -104,13 +120,13 @@
{ {
"id": "fill_3", "id": "fill_3",
"event": "FillSmallJug", "event": "FillSmallJug",
"hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"}, "hovers": [{ "attr":"stroke-width", "enter":"2", "leave":"1"},
{ "attr":"opacity", "enter":"0.8", "leave":"1.0"}] { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
}, },
{ {
"id": "fill_5", "id": "fill_5",
"event": "FillBigJug", "event": "FillBigJug",
"hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"}, "hovers": [{ "attr":"stroke-width", "enter":"2", "leave":"1"},
{ "attr":"opacity", "enter":"0.8", "leave":"1.0"}] { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
}, },
{ {
...@@ -124,13 +140,13 @@ ...@@ -124,13 +140,13 @@
{ {
"id": "empty_3", "id": "empty_3",
"event": "EmptySmallJug", "event": "EmptySmallJug",
"hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"}, "hovers": [{ "attr":"stroke-width", "enter":"2", "leave":"1"},
{ "attr":"opacity", "enter":"0.8", "leave":"1.0"}] { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
}, },
{ {
"id": "empty_5", "id": "empty_5",
"event": "EmptyBigJug", "event": "EmptyBigJug",
"hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"}, "hovers": [{ "attr":"stroke-width", "enter":"2", "leave":"1"},
{ "attr":"opacity", "enter":"0.8", "leave":"1.0"}] { "attr":"opacity", "enter":"0.8", "leave":"1.0"}]
}, },
{ {
......
Jars/Jars.svg
+ 4
− 4
View file @ 0acf8cdd
...@@ -27,13 +27,13 @@ ...@@ -27,13 +27,13 @@
<text id="jar_5_text" opacity="1" x="125" y="95">0</text> <text id="jar_5_text" opacity="1" x="125" y="95">0</text>
<line id="goal" x1="107" y1="120" x2="153" y2="120" stroke-width="2" stroke="#FF7777"/> <line id="goal" x1="107" y1="120" x2="153" y2="120" stroke-width="2" stroke="#FF7777"/>
<circle id="fill_3" cx="25" cy="25" r="15" fill="#BBBBBB"/> <circle id="fill_3" cx="25" cy="25" r="15" fill="#BBBBBB" stroke="black" stroke-width="1.0"/>
<rect id="fill_3_sym" x="20" y="20" width="10" height="12" style="fill:#267CEB"/> <rect id="fill_3_sym" x="20" y="20" width="10" height="12" style="fill:#267CEB"/>
<circle id="fill_5" cx="130" cy="25" r="15" fill="#BBBBBB"/> <circle id="fill_5" cx="130" cy="25" r="15" fill="#BBBBBB" stroke="black" stroke-width="1.0"/>
<rect id="fill_5_sym" x="125" y="20" width="10" height="12" style="fill:#267CEB"/> <rect id="fill_5_sym" x="125" y="20" width="10" height="12" style="fill:#267CEB"/>
<circle id="empty_3" cx="25" cy="65" r="15" fill="#BBBBBB"/> <circle id="empty_3" cx="25" cy="65" r="15" fill="#BBBBBB" stroke="black" stroke-width="1.0"/>
<rect id="empty_3_sym" x="20" y="60" width="10" height="12" style="fill:#DDEEFF"/> <rect id="empty_3_sym" x="20" y="60" width="10" height="12" style="fill:#DDEEFF"/>
<circle id="empty_5" cx="130" cy="65" r="15" fill="#BBBBBB"/> <circle id="empty_5" cx="130" cy="65" r="15" fill="#BBBBBB" stroke="black" stroke-width="1.0"/>
<rect id="empty_5_sym" x="125" y="60" width="10" height="12" style="fill:#DDEEFF"/> <rect id="empty_5_sym" x="125" y="60" width="10" height="12" style="fill:#DDEEFF"/>
<circle id="transfer" cx="77.5" cy="45" r="15" fill="#BBBBBB"/> <circle id="transfer" cx="77.5" cy="45" r="15" fill="#BBBBBB"/>
<polyline id="transfer_left" points="70,45 76,41 76,49" fill="#00000"/> <polyline id="transfer_left" points="70,45 76,41 76,49" fill="#00000"/>
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment