Sunday, November 20, 2022

steps I took to add a picture to the website frontpage

The current iteration of uses data from a JSON file to dynamically generate page content. 

On the front page of there's currently an SVG. I wanted to place a PNG next to the SVG. Before placing the PNG, I wanted to make the SVG narrower. Looking at the source code for the page index.html, I see

<svg id='viz'></svg>

Inspecting the source code of the rendered page, I see

var width = 600;

which comes from

To test out a change to a narrower width, I start "Docker desktop" on my Mac and, in the directory allofphysicsgraph/proofofconcept/v7_pickle_web_interface, run the command

docker-compose up --build --remove-orphans

In a web browser I was then able to access http://localhost:80 and got a warning from Chrome that the certs were invalid. Incognito mode seemed to be working better.

Wednesday, October 26, 2022

Levels of reproducibility and repeatability and replication

Knowledge progresses when one person can leverage the insights of another person. There are levels of reproducibility that require different levels investment on the part of the person looking to build on the initial knowledge. 

The levels described below are ranked from "requires lots of work to build upon" to "very easy to leverage."

Level 0: discoverable claim

Undocumented claims that no one else is aware of are irrelevant to the advancement of science. 

Level 1: claim without evidence

example: "My design for this car tire supports operational speeds of 50 miles per hour and will be usable for 50,000 miles."
No software or analytical calculations are provided. No explanation of how claim was arrived at.

Level 2: verbal hints of process used

software-based example: My design for the car tire is based on calculations from code written in Python.
analytical example: In my calculation of operational speed I used the Fourier transform.

What distinguishes 2 from 1: Advertising that code was written, or math was done. 
Most peer-reviewed scientific papers are written at this level or, if you're lucky, level 2. 
Most presentations of experiments (e.g., at conferences and lectures) also are made at this level or level 2.

Level 3: software without documentation or dependencies; or, for analytical, a few of the key equations

software-based example: Python script provided by the author to back up claim. No configuration file or random seed value. Library dependencies and versions need to be determined through trial and error (aka digital archeology).
analytical example: a few key equations (from a much more complex derivation) are mentioned, as are a few (not all) of the assumptions.

consequence: If you're smart and diligent, you may be able to recover statistically similar (though not exact) behavior for stochastic models, assuming neither you nor the original author had any bugs in the implementation.

Level 4:

software-based example: Python script with random seed value specified and configuration parameters documented. Documentation not included, nor are dependencies made explicit. 
analytical example: complete derivation provided, with explanation of assumptions

Level 5: repeatable

software-based example: Python script containerized, software versions pinned. Build process is executable. No digital archeology needed.
analytical example: portions of the complete derivation are checked by a computer algebra system (CAS) for correctness.

Level 6:

software-based example: Python script containerized with documentation of assumptions and examples of how to use. Configuration file with parameters and random seed values provided.
analytical example: complete derivation checked by a computer algebra system (CAS) for correctness. Proofs provided.  Citations where appropriate.

Caveat: the levels described above are not actually linear. There are a few meandering paths that get from 0 to 6. 


"Reproducibility vs. Replicability: A Brief History of a Confused Terminology"

Sunday, October 9, 2022

TLA+ comparison with other formal verification software

The scope of this post is limited to formal verification of algorithms and protocols. 

To save docker images to my repo,

docker pull official/imagename
docker image tag official/imagename:latest myusername/imagename:latest
docker push myusername/imagename:latest


Check the correctness of a specification. 
Not tied to a specific implementation or tests of an implementation.


"Jepsen is a Clojure library. A test is a Clojure program which uses the Jepsen library to set up a distributed system, run a bunch of operations against that system, and verify that the history of those operations makes sense."

For distributed systems, introduce {partitions, added resources, removed resources, delays, clock skew} and other noises, run operations, and then compare against expected results. 


"Stateright is a Rust actor library that aims to solve this problem by providing an embedded model checker, a UI for exploring system behavior (demo), and a lightweight actor runtime. It also features a linearizability tester that can be run within the model checker for more exhaustive test coverage than similar solutions such as Jepsen."


Can generate C, as well as parser/generators. 

Not explicitly temporal (whereas TLA+ is explicitly about temporal actions), but F* could be used for temporal models.



written by the same developer as SMV after the developer moved to Microsoft


constructive dependent type theory


"Simple formally verified compiler in Lean" by Ericson (2021)


CMU's SMV --> Cadence SMV --> nuSMV


simple type theory



Spin and Promela


Event B

"a modelling method for formalising and developing systems whose components can be modelled as discrete transition systems. An evolution of the (classical) B-method, Event-B is now centred around the general notion of events, which are also found in other formal methods such as Action Systems, TLA and UNITY."

An Introduction to the Event-B Modelling Method

Translating B to TLA+ for Validation with TLC

classical B for software development

Relevance of TLA+ to the Physics Derivation Graph

The Physics Derivation Graph is just a CRUD application, so I didn't expect TLA+ would be relevant. My initial view was that there isn't an algorithm or a protocol in the PDG. The PDG is just a webpage, some middleware (e.g., bash or Python) and a back-end database (CSV, SQL, JSON, Neo4j, etc). Standard MVC applies. 

After spending 1 day reviewing TLA+ materials, I realized the PDG has a workflow specification that I hadn't previously considered in detail. 

  1. User has a derivation in mind and they want to integrate it with existing PDG content. User knows their derivation's expressions, steps, symbols (variables and constants), and operators.
  2. User writes their derivation into the PDG referencing existing symbols, existing expressions, and existing inference rules. 
    • If the relevant symbol isn't available, add it.
    • If an existing symbol needs to be corrected/revised/merged, modify it.
    • If the relevant inference rule isn't available, add it.
    • If an existing inference rule needs to be corrected/revised/merged, modify it.
  3. Integrated derivation steps are checked for correctness using a Computer Algebra System (e.g., SymPy, Mathematica, etc)
That user story sounds reasonable until you consider two concurrent users editing the same steps or expressions or symbols or inference rules or operators. If each of the above steps are considered atomic, there are potential conflicts. 
  • One user could be attempting to create a new derivation step while another modifies existing symbols or inference rules. 
  • Two users could concurrently attempt to modify/merge/edit existing symbols or inference rules. When they commit their change, the thing they are changing may have disappeared or been altered.
One way to avoid the above potential for conflict would be to lock the database while edits are made (no concurrent users).
Another avoidance mechanism would be to queue changes and check consistency of every change sequentially (serialize concurrency). 

Saturday, October 8, 2022

glossary for TLA+ and PlusCal jargon


See also TLA+ language summary and this summary. Here's another summary of operators.

jargon definition
Apalache "symbolic model checker for TLA+." "Translates TLA+ into the logic supported by SMT solvers such as Microsoft Z3."
Source: apalache github

aka execution
sequence of states
Source: Lecture 1 video


Source: Specifying Systems page i25

execution see behavior.
Source: Lecture 1 video

execution stopped when it wasn't supposed to
Source: Lecture 3 video

See also termination
Source: Lecture 2 video
Source: Lecture 2 video
Source: Lecture 2 video
Source: Lecture 2 video
liveness property

"you have to look at the entire execution, which may be infinite, to determine that it is not satisfied."
Source: session 9

See also safety property

Source: Lecture 2 video
PlusCal User's manual
safety property

"if is not satisfied by an execution, then you can tell that it's not satisfied by looking at a finite portion of the execution—even if the execution is infinite."
Source: session 9

See also liveness property

state assignment of values to variables
Source: Lecture 1 video and
Source: TLA+ chapter in "Software Specification Methods"
state machine, specification of
  • all possible initial states
    • variables
    • initial value of each variable
  • what state follows a given state
    • relations values of variables in current state and possible values in the next state.
Source: Lecture 1 video
state predicate

"A formula that is true or false of a state. A state predicate is just an ordinary Boolean-valued formula that can contain variables but no primed variables and no temporal operators like <>."
Source: session 9

step change from one state to the next state.
Source: Lecture 1 video
strong fairness "A step of a process is strongly fair in a behavior iff there is no point in the behavior after which the step is enabled in infinitely many states but no such step occurs in the behavior."
Source: session 9

See also weak fairness
strongly fair see strong fairness

execution stopped when it was supposed to
Source: Lecture 3 video

See also deadlock

Temporal Logic of Actions
a temporal logic developed for describing and reasoning about concurrent and distributed systems
Source: Specifying and Verifying Systems With TLA+

TLAPS TLA+ proof system.
Source: Lecture 1 video and
Source: TLA+ Proof System (TLAPS)

language for high-level modeling digital systems. Here "high-level" refers to the design aspects, above the code. Examples of digital systems: algorithms, programs, and computer systems.
Source: Lecture 1 video

"a formal specification language based on (untyped) ZF set theory, first-order logic, and TLA (the Temporal Logic of Actions)"
Source: Specifying and Verifying Systems With TLA+

TLA+ version 2 user guide (2018)

TLA+ hyperbook

TLA+ toolbox IDE for TLA+.
Source: Lecture 1 video.

Toolbox website
TLC on-the-fly model checker for debugging TLA+ specifications
Source: Specifying and Verifying Systems With TLA+
Source: Lecture 2 video
Source: Lecture 2 video
weak fairness

the process must keep taking steps if it can
Source: session 9

See also strong fairness

weakly fair see weak fairness
/\ and
\/ or
Source: Lecture 2 video

aka eventually
For any state predicate P, the formula <>P is true of a behavior iff P is true of at least one state of the behavior.
Source: session 9


aka always
For any state predicate P, the formula <>P is true of a behavior iff P is true of at least one state of the behavior.
Source: session 9


aka leads to
Source: session 9

' aka prime
next value

In module Sequences

See TLA+ summary page 8 of 9, and this summary.
jargon definition
Append(seq,e) the sequence obtained by appending the value e as the new last element of the sequence seq. For example,
Append(<<1, 2>>, 42) equals <<1, 2, 42>>.
Source: intermezzo 1
Head(seq) the first element of a non-empty sequence seq. For example, Head(<<"a", "c", "b">>) equals "a".
Source: intermezzo 1
\o aka concatenation
"seq1 \o seq2 is the sequence obtained by concatinating the sequences seq1 and seq2 in the obvious way. For example, seq \o <<e>> equals Append(seq,e) for any sequence seq and value e."
Source: intermezzo 1

websites for learning TLA+


Lamport's homepage

video tutorial series:

TLA+ Github - includes DieHard4, DiningPhilosophers, Paxos, - Hillel Wayne -- announcement about revision to book; points to

Hillel Wayne - Designing Distributed Systems with TLA+

Tackling Concurrency Bugs with TLA+ by Hillel Wayne

  • toy example of money transfer in TLA+
  • three real-world cases from Hillel's employer of using TLA+ to check design before implementation

@pressron - Ron Pressler
Ron Pressler - The Practice and Theory of TLA+

TLA+ in Docker in VSCode

A gentle intro to TLA+
Demos a three-state system using VSCode

VSCode plug-in using Docker for TLA+:

My video on how to install TLA+ inside Docker as a plug-in for VSCode:

Questions and Answers

Blog posts
Deep dive into practical use of TLA+ for real software. Links to github repo with Dockerfile

Using TLA+ for fun and profit in the development of Elasticsearch - Yannick Welsch

TLA+ Toolbox for Beginners

Modeling Virtual Machines and Interrupts in TLA+ & PlusCal - Valentin Schneider
use of TLA+ at ARM

TLA+ Tutorial 2021 at DISC 2021

Debugging software designs using testable pseudo-code (Jay Parlar)
Alice and Bob money transfer model (from
utility: first motivating example for why TLA+ provides value to design process

A Beginner's Guide to TLA+ Exploring State Machines & Proving Correctness

SREcon20 Americas - Weeks of Debugging Can Save You Hours of TLA+
Uses an example written in C that has a rare deadlock. 

Saturday, May 28, 2022

Next steps once math expressions are tokenized

In my previous post I outlined a sequence of steps with a negative framing about how difficult each step would be. A positive framing of the sequence is

  1. Analyze .tex from arxiv and account for issues like encoding and misspelling and mal-formed latex and expansion of macros.
  2. Once the math (e.g. $x$) and expressions are separated from the text, tokenize variables within expressions.
  3. Once variables are tokenized within expressions, identifying the concept (e.g., name of constants) based on the text in the paper.
  4. Reconcile variables across different .tex files in arxiv
  5. Create an interface providing semantically-enriched arxiv content that is indexed for search queries to users.

Suppose we are at step 2 and everything in a document is correctly tokenized (or even if just a fraction  of the content is tokenized). The follow-on step (3) would be to detect the definition of the tokens from the text. For example, if the variable "a" shows up in an expression, and $a$ shows up in the text, and the text is something like

"where $a$ is the number of cats in the house"
Then we can deduce that "a" is defined as "number of cats in the house".

Step 4 would be to figure out if "a" is used similarly in other papers. That would indicate a relation of the papers based on the topic of the content. See for example

Another use case for tokenized text (in step 2) with some semantic meaning (step 3) would be to validate the expressions. If the expression is "a = b" and the two variables have different units, that means the expression is wrong.