Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found
Select Git revision
  • master
1 result

Target

Select target project
  • general/stups/visb-visualisation-examples
1 result
Select Git revision
  • master
1 result
Show changes
Commits on Source (2)
......@@ -4,3 +4,4 @@
*.fuzz
*.log
*_tla.txt
*.dot
......@@ -69,15 +69,19 @@ Init == /\ big = 0
(***************************************************************************)
FillSmallJug == /\ small' = 3
/\ big' = big
/\ small < 3 \* added for VisB
FillBigJug == /\ big' = 5
/\ small' = small
/\ big < 5 \* added for VisB
EmptySmallJug == /\ small' = 0
/\ big' = big
/\ small > 0 \* added for VisB
EmptyBigJug == /\ big' = 0
/\ small' = small
/\ big > 0 \* added for VisB
(***************************************************************************)
(* 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
(***************************************************************************)
SmallToBig == /\ big' = Min(big + small, 5)
/\ small' = small - (big' - big)
/\ small > 0 \* added for VisB
/\ big < 5 \* added for VisB
BigToSmall == /\ small' = Min(big + small, 3)
/\ 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 *)
......
......@@ -97,6 +97,22 @@
"id": "goal",
"attr": "x2",
"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 @@
{
"id": "fill_3",
"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"}]
},
{
"id": "fill_5",
"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"}]
},
{
......@@ -124,13 +140,13 @@
{
"id": "empty_3",
"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"}]
},
{
"id": "empty_5",
"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"}]
},
{
......
......@@ -27,13 +27,13 @@
<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"/>
<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"/>
<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"/>
<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"/>
<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"/>
<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"/>
......