Hillel Wayne hwayne

For the newsletter at: FILL IN

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

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

	function template($t) {
	@"
	SPECIFICATION Spec

	CONSTANTS
	BuffLen = 2
	NumThreads = $t

	CHECK_DEADLOCK TRUE
	"@

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

	PROPERTY LockProp

	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)]

	// dreidel model I wrote in 2023.
	// see https://buttondown.com/hillelwayne/archive/i-formally-modeled-dreidel-for-no-good-reason/
	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);

	// 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;

	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

	import planner.

	main =>
	S0 = {22, 0, [6, 6, 9, 5, 9, 1, 10, 9, 9, 3]},
	plan(S0, Plan),
	nl,
	writeln(Plan),
	nl.

	final({Target, Current, _}) =>