Re: [tlaplus] Sweeping a parameter range with TLC

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

My workaround is to fork a nested TLC for each configuration value from an outer “config spec".  What I like about this approach is that it allows me to define the configuration matrix directly in TLA+.  

https://github.com/lemmy/BlockingQueue/blob/main/BlockingQueuePoisonApple_statsSC.tla
https://github.com/tlaplus/Examples/blob/master/specifications/ewd998/EWD998_optsSC.tla
https://github.com/tlaplus/tlaplus/blob/master/general/performance/measure.tla
https://github.com/microsoft/CCF/blob/81943ea889e7087dee2379d5cdf4ab03552f999e/tla/consensus/MCccfraft.tla#L7-L18

A small improvement would be to introduce a dedicated operator for forking TLC, rather than relying on the current IOUtils!IOEnvExec method.  This part overlaps with the proposed REPL extension [1].

M.

[1] https://github.com/tlaplus/tlaplus/pull/1000#issuecomment-2303244077

> On Oct 3, 2024, at 8:17 PM, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:
> 
> Often I will have specs that take a constant representing input to the system. It is good to write specs this way because then you can write proofs over the unfixed value of that input constant. However, it is usually nice to model-check theorems before trying to prove them. It is also nice to model-check a set of possible values, rather than a single value chosen as input in the model. To this end I usually end up turning the input constant into a variable that is nondeterministically assigned some value from a set in the initial state and then never subsequently modified. However, this interferes with statement and proof of theorems. This must be a common issue, so does anybody have a good way around this? It seems like I would want to iteratively execute TLC across a range of values for a given constant.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5DABDDE6-944E-4796-83E6-73D662E2882A%40lemmster.de.