Shon Feder
Shon Feder
Yep. I’ll take this on. Thanks.
re: simplifying selection of action, perhaps something like this? ```tla ---- MODULE Ex ---- EXTENDS Apalache, Integers VARIABLES \* @typeAlias: COIN = {denom: Str, amount: Int}; \* @typeAlias: ACTION =...
Right, sorry, that was orthoginal to the big ints thing. I was only addressing > Besides that, what I want to achieve, is to express a non-deterministic choice of action....
For returning the logging data, Igor suggested we just a log-appender, that we can register with our current logging system. Then we just need to get the counter-example (and maybe...
After reviewing the log configuration code, and thinking things over a bit, it doesn't look like we can simply add a log appender with the current architecture -- at least...
Hi, Andrey! We should definitely make time to discuss MBT needs. I'll get an invite out. In the proper order of things the final version of the RPC data returned...
> async communication saves lots of time, but can also misleading in some cases, as the complete context is missing True! Tho I can and should also improve my ticket...
Did some exploratory testing. The minimal example I've turned up that triggers this behavior is ```tla EXTENDS Naturals Next == TRUE Init == TRUE Inv == [ x \in Nat...
Related to #2073
Related to #2261