Alexander-N

## Solve Every Sudoku Puzzle


## See http://norvig.com/sudoku.html

## Throughout this program we have:
##   r is a row,    e.g. 'A'
##   c is a column, e.g. '3'
##   s is a square, e.g. 'A3'
##   d is a digit,  e.g. '9'

Alexander-N

# Solve Every Sudoku Puzzle

## Reimplementaion of Peter Norvig's Python version
## See http://norvig.com/sudoku.html

## Throughout this program we have:
##   r is a row,    e.g. 'A'
##   c is a column, e.g. '3'
##   s is a square, e.g. "A3"
##   d is a digit,  e.g. '9'

Alexander-N

{
  "conceal.substitutions": [
    {
      "language": [
        "tla+",
        {
          "pattern": "**/*.tla"
        }
      ],
      "substitutions": [

Alexander-N

.* Event = "(?<event>.*)"(.|\n)*?Host = (?<host>.*)(.|\n)*?VectorClock = "(?<clock>.*)"(.|\n)*?value = \((?<values>.*)\)

@!@!@ENDMSG 2264 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
1: <Initial predicate>
/\ localVectorClock = ( Database :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) @@
  Cache :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) )
/\ receivedMessage_ = (ClientA :> Null @@ ClientB :> Null)
/\ pc = ( ClientA :> "SendDatabase" @@
  ClientB :> "SendDatabase" @@

Alexander-N

.* Event = "(?<event>.*)"(.|\n)*?Host = (?<host>.*)(.|\n)*?VectorClock = "(?<clock>.*)"(.|\n)*?value = (?<values>.*)

@!@!@ENDMSG 2264 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
1: <Initial predicate>
/\ localVectorClock = ( Database :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) @@
  Cache :> (ClientA :> 0 @@ ClientB :> 0 @@ Database :> 0 @@ Cache :> 0) )
/\ receivedMessage_ = (ClientA :> Null @@ ClientB :> Null)
/\ pc = ( ClientA :> "SendDatabase" @@
  ClientB :> "SendDatabase" @@

Alexander-N

@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.15 of Day Month 20?? (rev: d977051)
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 12 and seed 5016491069357648850 with 1 worker on 8 cores with 3524MB heap and 64MB offheap memory [pid: 7495] (Linux 5.4.0-72-generic amd64, Ubuntu 11.0.11 x86_64, MSBDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file /home/a/projects/tla-specs/asyncio-lock/step2.tla

Alexander-N

---- MODULE refueling ----
EXTENDS TLC, Integers, Naturals, FiniteSets
VARIABLES position, fuel, numberOfStops, stations

vars == <<position, fuel, numberOfStops, stations>>

Range(f) == {f[x]: x \in DOMAIN f}
Max(S) == CHOOSE i \in S : \A j \in S : i >= j
Min(S) == CHOOSE i \in S : \A j \in S : i <= j
Abs(x) == Max({x, -x})