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 (4)
...@@ -127,18 +127,6 @@ BlendSmokerHasWaterDrinkingNeighbor == ...@@ -127,18 +127,6 @@ BlendSmokerHasWaterDrinkingNeighbor ==
(* Solution *) (* Solution *)
(************) (************)
Init ==
/\ drinks \in { p \in DRINKS : p[3] = "mylk" }
/\ nationality \in { p \in NATIONALITIES : p[1] = "norwegian" }
/\ colors \in { p \in COLORS : p[2] = "blue" }
/\ pets \in PETS
/\ cigars \in CIGARS
Next ==
UNCHANGED <<nationality, colors, cigars, pets, drinks>>
Spec == Init /\ [][Next]_<<nationality, colors, cigars, pets, drinks>>
Solution == Solution ==
/\ BritLivesInTheRedHouse /\ BritLivesInTheRedHouse
/\ SwedeKeepsDogs /\ SwedeKeepsDogs
...@@ -158,4 +146,17 @@ Solution == ...@@ -158,4 +146,17 @@ Solution ==
FindSolution == ~Solution FindSolution == ~Solution
Init ==
/\ drinks \in { p \in DRINKS : p[3] = "mylk" }
/\ nationality \in { p \in NATIONALITIES : p[1] = "norwegian" }
/\ colors \in { p \in COLORS : p[2] = "blue" }
/\ pets \in PETS
/\ cigars \in CIGARS
Next ==
UNCHANGED <<nationality, colors, cigars, pets, drinks>>
Spec == Init /\ [][Next]_<<nationality, colors, cigars, pets, drinks>>
============================================================ ============================================================
------------------------------ MODULE DieHard ------------------------------- ------------------------------ MODULE DieHard -------------------------------
(* File from TLC distribution; minor change for ProB and VisB *) (* File from TLC distribution; minor changes for ProB and VisB *)
(***************************************************************************) (***************************************************************************)
(* In the movie Die Hard 3, the heros must obtain exactly 4 gallons of *) (* In the movie Die Hard 3, the heros must obtain exactly 4 gallons of *)
(* water using a 5 gallon jug, a 3 gallon jug, and a water faucet. Our *) (* water using a 5 gallon jug, a 3 gallon jug, and a water faucet. Our *)
......
...@@ -5,20 +5,33 @@ DEFINITIONS ...@@ -5,20 +5,33 @@ DEFINITIONS
SET_PREF_MININT == -1; SET_PREF_MININT == -1;
MINLIM == MAXINT-1; MINLIM == MAXINT-1;
GOAL == (cur=1 & numbers /= {}); GOAL == (cur=1 & numbers /= {});
VISB_SVG_FILE == ""; VISB_JSON_FILE == "";
VISB_SVG_BOX == rec(height:220, width:220, viewBox:"0 0 220 220"); VISB_SVG_BOX == rec(height:220, width:220, viewBox:"0 0 220 220");
vsz == 20; vsz == 20;
"LibrarySVG.def"; "CHOOSE.def";
VISB_SVG_CONTENTS == '''
<style>
.tl-dps {
stroke : red;
stroke-linecap: butt;
opacity : 0.8
}
</style>
''';
VISB_SVG_OBJECTS3 == rec(`id`:"line", svg_class:"line", class:MU({"tl-dps"}),
title : ```Track Line ```, visibility:MU({"visible"}),
`stroke-dasharray`:svg_set_dasharray({1,3,4,5,6,7,8,9,10,50,51}), //```0 0 3 10000```,
x1:0,y1:210, x2:220,y2:210);
VISB_SVG_OBJECTS2 == {x,y•x:0..9 & y:0..9 | rec(`id`:("nr",x,y), svg_class:"text", VISB_SVG_OBJECTS2 == {x,y•x:0..9 & y:0..9 | rec(`id`:("nr",x,y), svg_class:"text",
x:vsz+x*vsz, y:vsz+y*vsz, `font-size`:10, x:vsz+x*vsz, y:vsz+y*vsz, `font-size`:10,
text:x+y*10)}; text:x+y*10)};
VISB_SVG_OBJECTS1 == {x,y•x:0..9 & y:0..9 | rec(`id`:("rec",x,y), svg_class:"rect", VISB_SVG_OBJECTS1 == {x,y•x:0..9 & y:0..9 | rec(`id`:("rec",x,y), svg_class:"rect",
x:15+x*vsz, y:5+y*vsz, x:15+x*vsz, y:5+y*vsz,
stroke:"green", `stroke-width`:1.5,fill:"white", `stroke-width`:1.5,
width:vsz-1, height:vsz-1)}; width:vsz-1, height:vsz-1,
VISB_SVG_UPDATES2 == {x,y•x:0..9 & y:0..9 | rec(`id`:("rec",x,y),
stroke:IF x+y*10=cur THEN "red" stroke:IF x+y*10=cur THEN "red"
ELSIF x+y*10:numbers THEN "green" ELSE "gray" END, ELSIF x+y*10:numbers THEN "green" ELSE "gray" END,
fill: IF x+y*10:numbers THEN "white" ELSE "gray" END)}; fill: IF x+y*10:numbers THEN "white" ELSE "lightgray" END)};
VARIABLES numbers,cur, limit VARIABLES numbers,cur, limit
INVARIANT INVARIANT
numbers <: INTEGER & cur:NATURAL1 & limit:NATURAL1 numbers <: INTEGER & cur:NATURAL1 & limit:NATURAL1
......
...@@ -9,21 +9,21 @@ ...@@ -9,21 +9,21 @@
<style id="sudoku_styles"> <style id="sudoku_styles">
@keyframes hideshow { @keyframes hideshow {
0% {opacitiy: 1; fill: darkseagreen;} 0% {opacity: 1; fill: darkseagreen;}
15% {opacitiy: 0;} 15% {opacity: 0;}
20% {opacitiy: 1; fill: lightgrey;} 20% {opacity: 1; fill: lightgrey;}
25% {opacitiy: 0;} 25% {opacity: 0;}
30% {opacitiy: 1; fill: seagreen;} 30% {opacity: 1; fill: seagreen;}
85% {opacitiy: 0;} 85% {opacity: 0;}
100% {opacity: 0;} 100% {opacity: 0;}
} }
@keyframes hideshow2 { @keyframes hideshow2 {
20% {opacitiy: 1; fill: darkseagreen;} 20% {opacity: 1; fill: darkseagreen;}
35% {opacitiy: 0;} 35% {opacity: 0;}
40% {opacitiy: 1; fill: lightgrey;} 40% {opacity: 1; fill: lightgrey;}
65% {opacitiy: 0;} 65% {opacity: 0;}
70% {opacitiy: 1; fill: seagreen;} 70% {opacity: 1; fill: seagreen;}
99% {opacitiy: 0;} 99% {opacity: 0;}
100% {opacity: 0;} 100% {opacity: 0;}
} }
.normal { .normal {
......