Markus Alexander Kuppe
Markus Alexander Kuppe
It's the opposite of the direction in which we've been moving and I'm not saying it should be done, but moving each spec into its own Github repo in, perhaps,...
/cc @kape1395 for visibility
https://github.com/tlaplus/Examples/commit/4309acfaeee000924413075e605606d13d3d13c2
Is this related to/impacting the JSON logging that @achamayou added as part of trace validation?
Perhaps not an option for larger log files, but a [graphviz editor](https://edotor.net) serializes the input and appends it to the URL when sharing. For larger log files, Shiviz could load...
Without `StatusCommittedResponseAction`, I can also trigger "argument "tx" doesn't exist in function domain.".
> Also note that if you want the interface to properly display next possible actions, you should update the spec structure to have actions parameterized by any non-deterministic arguments (e.g....
```tla ---- MODULE Consistency ---- EXTENDS Naturals, Sequences ---------------------------------------------------------------------- \* tla-web doesn't have a builtin for the standard module's Sequences!SelectSeq. \* This is why its definition is included under a...
Now also at https://github.com/lemmy/CCF/blob/mku-ConsistencyMonolith/tla/consistency/Consistency.tla