People who take my TLA+ Class get a free specification review. Cory Myers asked for a review of his Reply.tla spec, reproduced from the PR below, and has graciously agreed to let me make it public. The review itself is here.
Note this is a "light" review: I'm looking for general TLA+ antipatterns and techniques that don't require me to deeply understand the problem domain. This represents about an hour of review.
For the newsletter at: FILL IN
Run with Dafny 4.6.0, with the flag --standard-libraries.
Going line by line:
b =: >: i. 9 9 9This generates a 9 by 9 by 9 array with all values from 1 to 729. We can choose what each axis represents: I decided that each table is all of the boolean variables for one number, and the rows and columns map to sudoku rows and columns. For example:
| import xml.etree.ElementTree as ET | |
| from xml.etree.ElementTree import Element | |
| from copy import deepcopy | |
| from argparse import ArgumentParser | |
| from dataclasses import dataclass | |
| from string import Template | |
| from pathlib import Path | |
| import typing as t | |
| #Common issue is that I need to have multiple slightly different versions of the same spec, this is a helper to do that. |
| function Ask { | |
| Param ( | |
| [PSDefaultValue(Help="*")] | |
| [switch]$Fast, | |
| [Parameter(Position=1)] | |
| [Alias("M")] | |
| [int]$Tokens=256, | |
| [Alias("n")] | |
| [int]$Results=1, | |
| [Parameter(Mandatory=$true, Position=0)] |
| // put in https://editor.p5js.org/ | |
| // generated (mostly) with GPT4 | |
| let cols, rows; | |
| let w = 2; | |
| let colors = []; | |
| let i = 0; | |
| let j = 0; | |
| let sorted = false; |
| dtmc | |
| const int M; //starting money | |
| formula Players = 4; //Players | |
| formula maxval = M*Players; | |
| formula done = (p1=0) | (p2=0) | (p3=0) | (p4=0); | |
| formula halfpot = ceil(pot/2); | |
| module dreidel | |
| p1 : [0..maxval] init M; |
Pleased to announce a new #NFT offering: #eNdFT! We are minting one cause of death NFT for every person on earth, which is 100% guaranteed to reflect the way you do, in fact, actually die.
Unless you trade it!
Unhappy with your "car crash" #eNdFT? Exchange it for an "old age"! Of course, you better be prepared to pay through the nose for "old age". Due to the nature of our product, eNdFTs cannot be bought or sold, only be traded 1-1 for another #eNdFT (plus an optional eth price to cover value differences). There is no escaping death.
Please note that our prediction software isn't perfect. While every #eNdFT is accurate, it may be imprecise. For example, you could receive the "Most likely drowned" NFT, or "either cancer or a stabbing". Don't worry, eNdFTs are still an exciting speculation opportunity! We're improving our prediction software all the time, and that "cancer or stabbing" #eNdFT could one day become a super valuable "cancer"! Join the #eNdFT network today!
(Disclaimers: while we will confirm
| -- Put this in after/plugins | |
| local api = vim.api | |
| local function chunk(text) | |
| local sections = {} | |
| for line in vim.gsplit(text, "@@@") do | |
| if line:find("^s") then | |
| table.insert(sections, {role = "system", content = line:sub(3)}) |
| import planner. | |
| lookup(Val, Arr1, Arr2) = Out => | |
| nth(I, Arr1, Val), | |
| nth(I, Arr2, Out). | |
| main => | |
| Machine = [{{load1, 1}, {proc1, 0}, {done1, 0}, {load2, 1}, {proc2, 0}, {done2, 0}, {lock, 1}}, | |
| [ {load1, | |
| {{load1, 1}, {lock, 1}}, % Maybe the inner ones should be lists, they're only iterated over |