Hillel Wayne

https://blog.acolyer.org/ Several hundred papers along with extensive analysis. Across the entire spectrum of CS, so most are not cold showers. Papers found should link to the actual paper in the...

http://neverworkintheory.org/ ~150 papers, most have limited scope and don't cover hype topics, but there might be some diamonds in there.

Parser doesn't recognize `id \in` at the beginning of an action property

1

The following parse successfully: ``` Prop == [][x = {1, 2}]_x Prop == [][1 \in {1, 2}]_x Prop == [][LET S == {1, 2} IN x \in S]_x Prop ==...

Changing the type of a declare constant is unreadable in toolbox dark mode themes

1

This is seen on both Windows and Mac OSX toolbox. Constant is originally one type of value:  On changing to another type of value, the textbox turns white background...

TLC incorrectly allows higher-order recursive operators

8

Setup: ```tla EXTENDS Integers RECURSIVE SetReduce(_, _, _) SetReduce(Op(_, _), set, value) == IF set = {} THEN value ELSE LET s == CHOOSE x \in set: TRUE IN SetReduce(Op,...

Define process-local variables above PlusCal define block

2

Currently PlusCal compilation produces something like this: ```tla VARIABLES global_variables \* Anything in a define block goes here VARIABLES local_variables ``` This means that define block operators can't reference any...

Highlight lassos steps in error traces

1

Liveness violations are either a set of steps followed by "stuttering" or a "lasso", or list with a cycle. Lasso error traces look like this: ``` 1 2 3 4...

PlusCal single processes can't use `self`

1

Given ``` (* --algorithm demo variables x = 1; macro set_x() begin x := self; end macro; process good \in {1} begin G: set_x(); end process; process bad = 2...

Toolbox freezes when using "translate pluscal automatically"

1

Steps to reproduce: 1. Create a PlusCal spec, and translate it. Create a model for the spec. 2. Enable "translate pluscal automatically". 3. Make a modification to the PlusCal, but...

Reviewing the Entry-level Model Checker Tutorial

4

I was asked by Igor to do a review of the [binary search tutorial](https://github.com/informalsystems/apalache/blob/b627481fca3677b15457c704fdd6f8aab66b6d84/docs/src/tutorials/entry-tutorial.md?plain=1#) and provide feedback. First some general thoughts, then specific notes: First, **I do not think the...