Add simulation mode to model validation

Signed-off-by: Joshua Zhang <joshuazh@microsoft.com>

Author: joshuazh-x

tla/README.md

@@ -72,6 +72,11 @@ The TLA+ spec defines the desired behaviors of the model. To validate the correc
 ./validate-model.sh -s ./MCetcdraft.tla -c ./MCetcdraft.cfg 
 ```
 
+You can also add `-m` option to run model checking in simulation mode, which will randomly walk in the state machine and is helpful for finding issues quickly.
+
+```console
+./validate-model.sh -m -s ./MCetcdraft.tla -c ./MCetcdraft.cfg 
+```
 
 ## Validate Collected Traces
 With above example trace logger, validate.sh can be used to validate traces parallelly.

tla/validate-model.sh

@@ -1,13 +1,13 @@
 #!/usr/bin/env bash
 
-WORKDIR="$(mktemp -d)"
+WORKDIR="${WORKDIR:-$(mktemp -d)}"
 TOOLDIR="${WORKDIR}/tool"
 STATEDIR="${WORKDIR}/state"
-FAILFAST=false
 PARALLEL=$(nproc)
+SIMULATE=false
 
 function show_usage {
-    echo "usage: validate-model.sh -s <spec> -c <config>">&2
+    echo "usage: validate-model.sh [-m] -s <spec> -c <config>">&2
 }
 
 function install_tlaplus {
@@ -22,16 +22,23 @@ function validate {
     local config=${2}
     local tooldir=${3}
     local statedir=${4}
+    local sim=${5:-false}
 
     set -o pipefail
-    java -XX:+UseParallelGC -cp ${tooldir}/tla2tools.jar:${tooldir}/CommunityModules-deps.jar tlc2.TLC -config "${config}" "${spec}" -lncheck final -metadir "${statedir}" -fpmem 0.9
+    if [ "$sim" = true ]; then
+        java -XX:+UseParallelGC -cp ${tooldir}/tla2tools.jar:${tooldir}/CommunityModules-deps.jar tlc2.TLC -config "${config}" "${spec}" -lncheck final -metadir "${statedir}" -fpmem 0.9 -workers auto -simulate
+    else
+        java -XX:+UseParallelGC -cp ${tooldir}/tla2tools.jar:${tooldir}/CommunityModules-deps.jar tlc2.TLC -config "${config}" "${spec}" -lncheck final -metadir "${statedir}" -fpmem 0.9 -workers auto
+    fi
+    
 }
 
-while getopts :hs:c:p: flag
+while getopts :hms:c: flag
 do
     case "${flag}" in
         s) SPEC=${OPTARG};;
         c) CONFIG=${OPTARG};;
+        m) SIMULATE=true;;
         h|*) show_usage; exit 1;; 
     esac
 done
@@ -47,5 +54,5 @@ echo "config: ${CONFIG}"
 
 install_tlaplus
 
-validate $SPEC $CONFIG $TOOLDIR $STATEDIR
+validate $SPEC $CONFIG $TOOLDIR $STATEDIR $SIMULATE