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
Loading items

Target

Select target project
  • general/stups/visb-visualisation-examples
1 result
Select Git revision
Loading items
Show changes

Commits on Source 2

MACHINE Sieve_VisB
// A version of the Sieve model with a simple VisB visualisation
DEFINITIONS
SET_PREF_MAXINT == 99;
SET_PREF_MININT == -1;
MINLIM == MAXINT-1;
GOAL == (cur=1 & numbers /= {});
VISB_SVG_FILE == "";
VISB_SVG_BOX == rec(height:220, width:220, viewBox:"0 0 220 220");
vsz == 20;
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,
text:x+y*10)};
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,
stroke:"green", `stroke-width`:1.5,fill:"white",
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"
ELSIF x+y*10:numbers THEN "green" ELSE "gray" END,
fill: IF x+y*10:numbers THEN "white" ELSE "gray" END)};
VARIABLES numbers,cur, limit
INVARIANT
numbers <: INTEGER & cur:NATURAL1 & limit:NATURAL1
INITIALISATION numbers := {} || cur := 1 || limit := 1
OPERATIONS
StartSieve(lim) = PRE cur=1 & lim>MINLIM & lim <= MAXINT THEN
numbers := 2..lim ||
cur := 2 ||
limit := lim
END;
prime <-- TreatNumber(cc) = PRE cc=cur & cur>1 & cur*cur<= limit THEN
IF cc:numbers THEN
numbers := numbers - ran(%n.(n:cur..limit/cur|cur*n))
/* numbers := numbers - ran(%n.(n:2..limit/cur|cur*n)) */
|| prime := TRUE
ELSE
prime := FALSE
END ||
cur := cur+1
END;
r <-- Finish = PRE cur*cur>limit THEN
cur := 1 || r := card(numbers)
END
END
...@@ -5,7 +5,7 @@ MACHINE SudokuEventUnicode ...@@ -5,7 +5,7 @@ MACHINE SudokuEventUnicode
*/ */
DEFINITIONS DEFINITIONS
Sze == 3; Mx==(Sze*Sze); Sze == 3; Mx==(Sze*Sze);
DOM == 1..Mx; D1 == 1..(Mx-1); D2 == 2..Mx ; DOM == 1..Mx;
RAN == (1..Mx); RAN == (1..Mx);
SUBSQS == λi.(i∈1..Sze | ((i-1)*Sze+1)..i*Sze); SUBSQS == λi.(i∈1..Sze | ((i-1)*Sze+1)..i*Sze);
SUBSQ == ran(SUBSQS); SUBSQ == ran(SUBSQS);
...@@ -45,7 +45,7 @@ DEFINITIONS ...@@ -45,7 +45,7 @@ DEFINITIONS
PossibleVals(cx,cy) == // locally possible values by examining all direct neighbouring conflict positions PossibleVals(cx,cy) == // locally possible values by examining all direct neighbouring conflict positions
DOM \ ran({x,y,r| x↦y ∈ conflict_pos(cx,cy) ∧ y∈dom(Board(x)) ∧ r=Board(x)(y)}) DOM \ ran({x,y,r| x↦y ∈ conflict_pos(cx,cy) ∧ y∈dom(Board(x)) ∧ r=Board(x)(y)})
CONSTANTS CONSTANTS
get_square /*@desc "Subsquare (1,2,3) for a coordinate 1..9" */, get_square /*@desc "Subsquare 1..3 for a coordinate 1..9" */,
conflict_pos /*@desc "set of positions that are in conflict with a given position" */, conflict_pos /*@desc "set of positions that are in conflict with a given position" */,
conflict_pos_sym /*@desc "symmetry-reduced version of conflict_pos" */, conflict_pos_sym /*@desc "symmetry-reduced version of conflict_pos" */,
PuzzleBoard /*@desc "Stored Puzzle" */ PuzzleBoard /*@desc "Stored Puzzle" */
...@@ -71,8 +71,8 @@ PROPERTIES ...@@ -71,8 +71,8 @@ PROPERTIES
ASSERTIONS ASSERTIONS
get_square ∈ DOM → 1..Sze; get_square ∈ DOM → 1..Sze;
get_square(1) = 1; get_square(3)=1; get_square(4)=2; get_square(9)=3; get_square(1) = 1; get_square(3)=1; get_square(4)=2; get_square(9)=3;
{1}× D2 ⊆ conflict_pos(1,1); {1}× (2..Mx) ⊆ conflict_pos(1,1);
D2×{1} ⊆ conflict_pos(1,1); (2..Mx)×{1} ⊆ conflict_pos(1,1);
(1..Sze)×(1..Sze) ⊆ {(1,1)} ∪ conflict_pos(1,1) (1..Sze)×(1..Sze) ⊆ {(1,1)} ∪ conflict_pos(1,1)
VARIABLES VARIABLES
Board, Board,
...@@ -86,11 +86,14 @@ INITIALISATION ...@@ -86,11 +86,14 @@ INITIALISATION
curx, cury := 1,1 curx, cury := 1,1
OPERATIONS OPERATIONS
SetEmpty = BEGIN Board := λi.(i∈DOM|∅) END; SetEmpty = BEGIN Board := λi.(i∈DOM|∅) END;
SetPuzzle = BEGIN Board := PuzzleBoard END; SetPuzzle = BEGIN Board := PuzzleBoard END;
SetCurPos(x,y) = // Change the current (cursor) position SetCurPos(x,y) = // Change the current (cursor) position
SELECT x∈DOM ∧ y∈DOM THEN SELECT x∈DOM ∧ y∈DOM THEN
curx, cury := x,y curx, cury := x,y
END; END;
SetCurPosToDetPosition(dx,dy) = // Hint action∈ set the cursor to deterministic position SetCurPosToDetPosition(dx,dy) = // Hint action∈ set the cursor to deterministic position
SELECT dx∈DOM ∧ dy∈DOM ∧ SELECT dx∈DOM ∧ dy∈DOM ∧
¬(dy∈dom(Board(dx))) ∧ ¬(dy∈dom(Board(dx))) ∧
...@@ -98,18 +101,22 @@ OPERATIONS ...@@ -98,18 +101,22 @@ OPERATIONS
THEN THEN
curx, cury := dx,dy // Change current position curx, cury := dx,dy // Change current position
END; END;
SetBoard(val) = // Set the value of the board at the current position SetBoard(val) = // Set the value of the board at the current position
SELECT val∈RAN ∧ cury ∉ dom(PuzzleBoard(curx)) THEN SELECT val∈RAN ∧ cury ∉ dom(PuzzleBoard(curx)) THEN
Board(curx)(cury) := val Board(curx)(cury) := val
END; END;
ClearCurPos = // Clear the value at the current position ClearCurPos = // Clear the value at the current position
SELECT cury ∉ dom(PuzzleBoard(curx)) THEN SELECT cury ∉ dom(PuzzleBoard(curx)) THEN
Board(curx) := {cury} ⩤ Board(curx) Board(curx) := {cury} ⩤ Board(curx)
END; END;
res <-- GetPossibleVals = // get possible values for the current position res <-- GetPossibleVals = // get possible values for the current position
BEGIN BEGIN
res := PossibleVals(curx,cury) res := PossibleVals(curx,cury)
END; END;
Solve(SBoard) = // Solve the board Solve(SBoard) = // Solve the board
SELECT SELECT
SBoard ∈ DOM → (DOM → RAN) /*@desc "The solution SBoard must be complete" */ ∧ SBoard ∈ DOM → (DOM → RAN) /*@desc "The solution SBoard must be complete" */ ∧
......