Markus Alexander Kuppe
Markus Alexander Kuppe
### Quantify current coverage with five nodes Main observation: The `RcvProposeVoteRequest` action rarely, if ever, occurs, likely because the upper limit set for the length of the generated traces (`-depth`)...
I've been running simulations of the specification for a few hours, and so far, neither `LogMatchingProp` nor `LeaderProp` have been violated. However, the overall coverage is limited (see below) because...
> [@lemmy](https://github.com/lemmy) perhaps I missing something here, but this does not seem like an improvement? It looks like there are fewer distinct states in proportion than before, the frequency of...
Related: https://github.com/tlaplus/tlaplus/issues/1065
@melhindi To enable TLC to periodically and at the end of model checking write the `TLCGet("stats")` to the `SIMccfraft.ndjson` file, simply add a definition like `PrintStats` to your specification. Then,...
It could also be interesting to see how well e.g. Github Copilot is able to predict those defs.
Unfortunately, there are no resources to change/fix the Toolbox.
> I've updated my branch with the tip from Damien which restores the compatibility of two-argument options. Does this make https://github.com/tlaplus/tlaplus/pull/1085 obsolete?
> I tried to do, but I can't seem to write to your fork You and the others should have collaborator permissions in my fork:
Using the verb concatenated with the camel-cased path appears to be a common default. For example, the verb `delete` combined with the path `app/log/private/all` becomes the operationId `DeleteAppLogPrivateAll`. Does the...