hwayne

Steps to Run

1. Download the VSCode Extension (https://marketplace.visualstudio.com/items?itemName=tlaplus.vscode-ide)
2. Put WireAsync.tla and WireAsync.cfg in the same file
3. Run VSCode command TLA+ > Check Model With TLC

hwayne

from z3 import *  # type: ignore
s1, s2 = Solver(), Solver()

a0, a, b, c, d, e, f = Consts('a0 a b c d e f', IntSort())
x, y, z = Ints('x y z')
t = "a*x+b*y+c*z+d*x*y+e*x*z+f*y*z+a0"

lambdamax = lambda x, y, z: eval(t)

z3max = Function('z3max', IntSort(), IntSort(), IntSort(),  IntSort())

hwayne

# Associated newsletter: https://buttondown.com/hillelwayne/archive/solving-linkedin-queens-with-smt/
# See also: https://ryanberger.me/posts/queens/
# And: https://github.com/ryan-berger/queens/blob/master/main.py

from z3 import * # type: ignore
from itertools import combinations, chain, product
solver = Solver()
size = 9

# queens[n] = col of queen on row n

hwayne

SPECIFICATION Spec
PROPERTY Liveness
CHECK_DEADLOCK FALSE

hwayne

-- Drop this in /after or /after/plugin/
-- explanation at commands (at end of file)

vim.g.exo = "where you store your data files"
local filelinks_file = vim.g.exo .. 'filelinks.json'

local function get_filelinks()
  return vim.fn.json_decode(vim.fn.readfile(filelinks_file))
end

hwayne

local function moduleline() -- can't be a global as line can move
  local lines = vim.api.nvim_buf_get_lines(0, 0, -1, false)
  for idx, line in ipairs(lines) do
    if string.match(line, "%-+ MODULE [%w_]+ %-") then
      return idx, line
    end
  end
end

local function fix_module_string()

hwayne

Bsky spinner

Spins your avatar like a clock

https://bsky.app/settings/app-passwords

Disclaimer: I set this up locally half a year ago and forgot all the steps, so the steps below may be wrong.

To run locally

hwayne

function template($t) {
    @"
SPECIFICATION Spec

CONSTANTS
    BuffLen = 2
    NumThreads = $t

CHECK_DEADLOCK TRUE
"@

hwayne

SPECIFICATION Spec
\* Add statements after this line.
CONSTANTS 
    Threads = {t1}
    NULL = NULL
    Keys = {k1}
    MaxId = 1
    BUGMODE = TRUE

PROPERTY LockProp

hwayne

For the newsletter at: FILL IN

Run with Dafny 4.6.0, with the flag --standard-libraries.