Markus Alexander Kuppe
Markus Alexander Kuppe
> [@lemmy](https://github.com/lemmy), thanks; quick follow-up question: Is it correct to assume that `POSTCONDITION` represents the total/aggregated coverage? I.e., is there no need to configure it as `_PERIODIC` (Unless model checking...
There is nobody actively maintaining PlusPy, but we can probably review a PR. By the way, TLC has now also an executor mode. It can execute a [blocking queue](https://github.com/lemmy/BlockingQueue/commit/980e5a30fad6859662c343de34e20f34a7463c18) and...
Like PlusPy, you can map a (randomly generated) TLA+ (prefix of a) behavior to code. Can you share more about your use case? https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/tool/TLAPlusExecutor.java https://github.com/lemmy/BlockingQueue/blob/980e5a30fad6859662c343de34e20f34a7463c18/impl/src/org/kuppe/App.java
1) * Make sure to exploit [symmetry reduction](https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/model-values.html#symmetry) * TLC doesn't support DFS but depth-first search iterative deepening; this mode is still exhaustive, i.e., explores *all* successor states * TLC's...
To make it easier for TLA+ beginners, I recommend hiding the proof step view (and the commands) until TLAPS is activated.
Alternatively, the wording could be adjusted so that beginners understand they likely don't need TLAPS at this stage and can simply ignore the view. The message could also include instructions...
### small ```shell 2025-09-17T20:10:21.530Z globals install 2025-09-17T20:10:21.535Z genaiscript:cli opts: { colors: true } 2025-09-17T20:10:21.535Z genaiscript:host:node installing undefined 2025-09-17T20:10:21.535Z genaiscript:host:node initializing NodeHost with dotEnvPaths: undefined 2025-09-17T20:10:21.535Z genaiscript:host set runtime host 2025-09-17T20:10:21.535Z...
> It looks like it wrote output.txt, you're not seeing it locally in your fs? No, there's no `output.txt`.
@pelikhan I will take a look if you point me in the right direction.