Markus Alexander Kuppe
Markus Alexander Kuppe
Related: https://github.com/tlaplus/tlapm/issues/206
@younes-io The screenshots suggest that the module provider doesn't take EXTENDS into account and thinks that e.g. `Len`, ... is defined in `Json`. It is possible that this information is...
> This proof works: > > ``` > THEOREM DeadlockFreedom == Spec => []Invariant > 1. Init => IInv BY SMT DEF IInv > 2. TypeInv /\ IInv /\ [Next]_vars...
> However, it makes sense to spin out the TLAPM parser into its own repo (it's still quite a good parser and worth keeping for its own sake!) so you...
Understood - there’s no issue with refactoring the parse tree format, but it will require refactoring some of the transformations. To minimize the risk of regressions, such refactoring should be...
> There's an even more complicated analysis that needs to be done for higher-order operators Nit: TLA+ is a first-order logic. It is not higher-order, where operators can be treated...
> @lemmy good point. What do you think is a good term for the parameter of these not-higher-order-ops? I've seen "operator parameter parameter" a few times in the codebase which...
> > _Aside: This could be an interesting to model in TLA+ using a separate high-level specification such as https://github.com/Azure/azure-cosmos-tla/blob/master/general-model/cosmos_client.tla_ The latest versions of the Cosmos specs are hosted at...
Please consider adding tests to https://github.com/tlaplus/CommunityModules/blob/master/tests/GraphsTests.tla
> Arrgh, GitHub pretty-printing ... the above should read ` \in SimplePath(G)` holds for every n. Just put it in single backticks the next time.