[tlaplus] Demo of sweeping parameter ranges with script

["hwa...@xxxxxxxxx" <hwayne@xxxxxxxxx>]

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/ebdba326-51bd-4098-9dd8-b2a9bc16a3efn%40googlegroups.com.