Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- one sig Board {
- cols : seq Columns
- } {
- #cols = 9
- not hasDups[cols]
- }
- sig Columns {
- cells : seq Values
- } {
- #cells = 9
- elems[cells] = Values
- }
- abstract sig Values {}
- one sig V1, V2, V3, V4, V5, V6, V7, V8, V9 extends Values {}
- fun row [ i : Int ] : Values {
- { elems[Board.cols].cells[i] }
- }
- fun subsquare [ startRow : Int, startCol : Int ] : Values {
- {
- Board.cols[startCol].cells[startRow] +
- Board.cols[startCol].cells[startRow + 1] +
- Board.cols[startCol].cells[startRow + 2] +
- Board.cols[startCol + 1].cells[startRow] +
- Board.cols[startCol + 1].cells[startRow + 1] +
- Board.cols[startCol + 1].cells[startRow + 2] +
- Board.cols[startCol + 2].cells[startRow] +
- Board.cols[startCol + 2].cells[startRow + 1] +
- Board.cols[startCol + 2].cells[startRow + 2]
- }
- }
- fact EveryRowHasEveryNumber {
- all v : Values | v in row[0]
- all v : Values | v in row[1]
- all v : Values | v in row[2]
- all v : Values | v in row[3]
- all v : Values | v in row[4]
- all v : Values | v in row[5]
- all v : Values | v in row[6]
- all v : Values | v in row[7]
- all v : Values | v in row[8]
- }
- fact EveryColumnHasEveryNumber {
- all c : elems[Board.cols] | !c.cells.hasDups
- }
- fact EverySubsquareHasEveryNumber {
- all v : Values | v in subsquare[0,0]
- all v : Values | v in subsquare[0,3]
- all v : Values | v in subsquare[0,6]
- all v : Values | v in subsquare[3,0]
- all v : Values | v in subsquare[3,3]
- all v : Values | v in subsquare[3,6]
- all v : Values | v in subsquare[6,0]
- all v : Values | v in subsquare[6,3]
- all v : Values | v in subsquare[6,6]
- }
- pred Show[i : Int] {
- //seq[i][j] = Int[7]
- i in inds[Board.cols]
- row[i] = Values
- }
- run Show for 5 int, 9 seq, 9 Columns
Add Comment
Please, Sign In to add comment