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