[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Demo of sweeping parameter ranges with script



>It can't share state between TLC runs

This is something I've been thinking about. If we were to build sweep functionality in to TLC somehow, would it be valid to run it all in a single execution? Naively you'd just convert all the swept constants to variables assigned some value in the initial state and then subsequently unchanged. This clearly changes their level so in some sense is invalid, but would it preserve all the safety/liveness/symmetry etc. properties that we care about? Seems like an interesting proof could be written.

Andrew Helwer

On Monday, October 7, 2024 at 5:01:14 PM UTC-4 hwa...@xxxxxxxxx wrote:
Last week Andrew asked about "sweeping" a parameter in TLC: model checking with CONSTANT X = 1, then with X = 2, etc. You can't do this "in-band" with TLC alone but you can do it by using a separate script to generate a sequence of CFGs.

We'll demonstrate this with a slight modification of blocking queue: spec and script can both be found at this gist. I used Powershell but it shouldn't be any harder in bash:

function template($t) {
@"
SPECIFICATION Spec
CONSTANTS
    BuffLen = 2
    NumThreads = $t
CHECK_DEADLOCK TRUE
"@
}

foreach ($i in 2..6) {
    Write-Output "Testing with NumThreads = $i"
    (template $i) > "MCSweepingExample.cfg"
    java -jar /path/to/tla2tools.jar -noGenerateSpecTE SweepingExample.tla -config MCSweepingExample.cfg > out
    if($LASTEXITCODE) {
        Write-Output "Error, see `out` for deets"
        exit
    }
}

This will try `NumThreads = 2..6` and eventually find an error on Threads = 5.

This is just a proof of concept and has a couple of drawbacks:

- It can't share states between TLC runs. Doesn't matter here but it would if we also swept on `BuffLen`.
- Handling model values isn't a problem, but for symmetric model values you'd need to generate an `MCSweepingExample.tla` too.

One idea this opens up is sweeping params until you get an error, and then rerunning with some changes, like an optimization or a new ALIAS or something. Gonna sleep on that!

This does make me think TLC would benefit from a `-quiet` flag.

H

--
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/927f0624-ba8e-4abe-909f-c4409e5dd34cn%40googlegroups.com.