spectacle
spectacle copied to clipboard
will62794
Interactive, web-based tool for exploring, visualizing, and sharing formal specifications in TLA+.
The trace expressions `RoTxRequestAction` and `RwTxRequestAction ` for https://github.com/lemmy/CCF/blob/mku-ConsistencyMonolith/tla/consistency/Consistency.tla are certainly not true in the shown trace.
For the use cases I envision, I was not planning to implement full blown semantics of modules and module imports e.g. `EXTENDS`, etc. For example, for now I'm just considering...
Opening the following trace link takes forever (spinning wheel next to "root spec") in Edge (Vivaldi) and Safari: https://will62794.github.io/tla-web/#!/home?specpath=https%3A%2F%2Fraw.githubusercontent.com%2Flemmy%2FCCF%2Fmku-ConsistencyMonolith%2Ftla%2Fconsistency%2FConsistency.tla&traceExprs%5B0%5D=AllCommittedObservedRoInv&trace=297cc69b%2Cd0b53816%2Cc64ffa94%2C28d6a04f%2C266f1e96%2C44617b58%2C551598da%2C150d05ea%2C14022610%2C74fe4aa9%2Cae2a49a2%2Cd54bbb48
The following spec works fine in TLC, but fails exploration with tla-web with: ```javascript Error: argument "tx_id" doesn't exist in function domain. at assert (eval.js:39:15) at FcnRcdValue.applyArg (eval.js:422:9) at evalExpr...
@lorin's linearizability spec at https://github.com/lorin/tla-linearizability is a great use-case for tla-web. Imagine exploring the scenarios interactively while studying the original lin paper.
1. This is amazingly cool, thank you for making this. 2. If possible, I think this would be a great addition to learntla. Is it something I can embed in...
Decide how to handle "model values" for instantiation of CONSTANT parameters. Currently, it is expected that string values are to be used in place of model values.
It is often helpful to view the state variables in a trace by process (e.g. nodes, servers, etc.). Adding the ability to explode/split the trace on an arbitrary constant set...
Handle https://github.com/tlaplus/azure-cosmos-tla/blob/master/simple-model/show521677.tla. :-)
When hovering over an action name in the next-state selection pane, it would be helpful if additional details of that action were shown e.g., the code for that action and/or...