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

add first version of Sudoku example

parent cf676984
No related branches found
No related tags found
No related merge requests found
MACHINE SudokuEvent
/* A version of Sudoku where the solving happens inside an event
(c) Michael Leuschel
*/
DEFINITIONS
Sze == 3; Mx==(Sze*Sze);
DOM == 1..Mx; D1 == 1..(Mx-1); D2 == 2..Mx ;
RAN == (1..Mx);
SET_PREF_MAXINT == 3; SET_PREF_TIME_OUT == 45000;
SUBSQ == ran(%i.(i:1..Sze | ((i-1)*Sze+1)..i*Sze));
SUBSQE == { {1,2,3,4}, {5,6,7,8}, {9,10,11,12}, {13,14,15,16} };
ANIMATION_FUNCTION_DEFAULT == {r,c,i|r:1..Mx & c:1..Mx & i=16};
ANIMATION_FUNCTION == ( {r,c,i|r:DOM & c:DOM & i:RAN & i = Board(r)(c)} );
ANIMATION_IMG0 == "images/sm_0.gif";
ANIMATION_IMG1 == "images/sm_1.gif";
ANIMATION_IMG2 == "images/sm_2.gif";
ANIMATION_IMG3 == "images/sm_3.gif";
ANIMATION_IMG4 == "images/sm_4.gif";
ANIMATION_IMG5 == "images/sm_5.gif";
ANIMATION_IMG6 == "images/sm_6.gif";
ANIMATION_IMG7 == "images/sm_7.gif";
ANIMATION_IMG8 == "images/sm_8.gif";
ANIMATION_IMG9 == "images/sm_9.gif";
ANIMATION_IMG16 == "images/sm_empty_box.gif";
SET_PREF_MAX_OPERATIONS == 82;
/* PUZZLE CONSTRAINTS : */
PUZZLE == (
Board(1)(1)=7 & Board(1)(2)=8 & Board(1)(3)=1 & Board(1)(4)=6 & Board(1)(6)=2
& Board(1)(7)=9 & Board(1)(9) = 5 &
Board(2)(1)=9 & Board(2)(3)=2 & Board(2)(4)=7 & Board(2)(5)=1 &
Board(3)(3)=6 & Board(3)(4)=8 & Board(3)(8)=1 & Board(3)(9)=2 &
Board(4)(1)=2 & Board(4)(4)=3 & Board(4)(7)=8 & Board(4)(8)=5 & Board(4)(9)=1 &
Board(5)(2)=7 & Board(5)(3)=3 & Board(5)(4)=5 & Board(5)(9)=4 &
Board(6)(3)=8 & Board(6)(6)=9 & Board(6)(7)=3 & Board(6)(8)=6 &
Board(7)(1)=1 & Board(7)(2)=9 & Board(7)(6)=7 & Board(7)(8)=8 &
Board(8)(1)=8 & Board(8)(2)=6 & Board(8)(3)=7 & Board(8)(6)=3 & Board(8)(7)=4 & Board(8)(9)=9 &
Board(9)(3)=5 & Board(9)(7)=1
);
UnassignedPosition(x,y) == x:DOM & y:DOM & not(y:dom(Board(x)))
VARIABLES
Board,
curx, cury
INVARIANT
Board : DOM --> (DOM +-> RAN) &
curx : DOM &
cury : DOM
INITIALISATION
Board : (Board : DOM --> (DOM +-> RAN) & PUZZLE) ||
curx, cury := 1,1
OPERATIONS
SetEmpty = BEGIN Board := %i.(i:DOM|{}) END;
SetPuzzle = BEGIN Board : (Board : DOM --> (DOM +-> RAN) & PUZZLE) END;
//val <-- GetBoard(x,y) = PRE x:DOM & y:dom(Board(x)) THEN val := Board(x)(y) END;
SetCurPos(x,y) = PRE x:DOM & y:DOM THEN
curx, cury := x,y
END;
SetBoard(val) = PRE val:RAN THEN
Board(curx)(cury) := val // Set the Value at a given board position
END;
solve(SBoard) = PRE
SBoard : DOM --> (DOM --> RAN) /*@desc "The solution must be complete" */ &
!(x,y).(y:dom(Board(x))
=> SBoard(x)(y) = Board(x)(y)) /*@desc "Copy partial solution (Board variable)" */ &
!y.(y:DOM =>
LET By BE By = SBoard(y) IN
!(x1).(x1:D1
=> !x2.(x1<x2 & x2:D2
=> (SBoard(x1)(y) /= SBoard(x2)(y) &
By(x1) /= By(x2)))
)
END
) /*@desc "Values are distinct on all columns and rows" */
&
!(s1,s2).(s1:SUBSQ & s2:SUBSQ => !x1.(x1:s1 =>
!(y1,x2,y2).( (x1:s1 & x2:s1 & x1>=x2 & y1:s2 & y2:s2 & (x1=x2 => y1>y2)
& (x1,y1) /= (x2,y2) )
=>
SBoard(x1)(y1) /= SBoard(x2)(y2)
)
) ) /*@desc "Values are all distinct within each Sub-Square" */
THEN
Board := SBoard
END
END
\ No newline at end of file
This diff is collapsed.
{
"svg":"SudokuFeld.svg",
"definitions":
[
{ "name":"BOARD",
"value" : "%x.(x:DOM|%y.(y:DOM|0) <+ Board(x))"
}
],
"items": [
{
"for": {"from":1, "to":9},
"repeat": [1,2,3,4,5,6,7,8,9],
"id": "txt_%0_%1",
"attr": "text",
"value" : "BOARD(%0)(%1)"
},
{
"for": {"from":1, "to":9},
"repeat": [1,2,3,4,5,6,7,8,9],
"id": "board_%0_%1",
"attr": "class",
"value" : "IF curx=%0 & cury=%1 THEN \"selected\" ELSIF %1:dom(Board(%0)) & (curx=%0 or cury=%1) & BOARD(%0)(%1)=BOARD(curx)(cury) THEN \"wrong\" ELSE \"normal\" END"
},
{
"for": {"from":1, "to":9},
"repeat": [1,2,3,4,5,6,7,8,9],
"id": "txt_%0_%1",
"attr": "visibility",
"value" : "IF %1 : dom(Board(%0)) THEN \"visible\" ELSE \"hidden\" END"
}
],
"events": [
{
"for": {"from":1, "to":9},
"repeat": [1,2,3,4,5,6,7,8,9],
"id": "g_%0_%1",
"event": "SetCurPos",
"predicates" : ["x=%0","y=%1"],
"hovers": [{ "attr":"stroke-width", "enter":"1", "leave":"0.1"}
]
}
]
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment