Merge pull request #1579 from informalsystems/th/doc-fix-tune-here

Rename `--tuning-options` to `--tune-here`

UNRELEASED.md

@@ -10,3 +10,10 @@
          * Some bug fix, see #124
 
      DO NOT LEAVE A BLANK LINE BELOW THIS PREAMBLE -->
+### Breaking changes
+
+ * Rename `--tuning` to `--tuning-options-file`, see #1579
+
+### Bug fixes
+
+ * Fix references to `--tune-here` (actually `--tuning-options`), see #1579

docs/src/apalache/running.md

@@ -12,7 +12,7 @@ The model checker can be run as follows:
 $ apalache-mc check [--config=filename] [--init=Init] [--cinit=ConstInit] \
     [--next=Next] [--inv=Inv] [--length=10] [--algo=(incremental|offline)] \
     [--discard-disabled] [--no-deadlock] \
-    [--tuning=filename] [--tune-here=options] \
+    [--tuning-options-file=filename] [--tuning-options=key1=val1:...:keyn=valn] \
     [--smt-encoding=(oopsla19|arrays)] \
     [--out-dir=./path/to/dir] \
     [--write-intermediate=(true|false)] \
@@ -45,8 +45,10 @@ The arguments are as follows:
     - `--view <name>` sets the state view to `<name>`, see [Enumeration of counterexamples][].
     - `--no-deadlock` disables deadlock-checking, when `--discard-disabled=false` is on. When `--discard-disabled=true`,
       deadlocks are found in any case.
-    - `--tuning` specifies the properties file that stores the options for
+    - `--tuning-options-file` specifies a properties file that stores options for
       [fine tuning](tuning.md)
+    - `--tuning-options` can pass and/or override these [fine tuning](tuning.md)
+      options on the command line
     - `--out-dir` set location for outputting any generated logs or artifacts,
       *`./_apalache-out` by default*
     - `--write-intermediate` if `true`, then additional output is generated. See
@@ -60,9 +62,7 @@ The arguments are as follows:
       is set to `True`.  Setting `profiling` to `False` is incompatible with the
       `--smtprof` flag. The default is `False`.
 
-
-      The options that are passed with the option `--tuning-options`
-      have priority over the options that are passed with the option `--tuning`.
+Options passed with `--tuning-options` have priority over options passed with `--tuning-options-file`.
 
 If an initialization predicate, transition predicate, or invariant is specified both in the configuration file, and on
 the command line, the command line parameters take precedence over those in the configuration file.

docs/src/apalache/tuning.md

@@ -2,19 +2,21 @@ Parameters for fine tuning
 ==========================
 
 The parameters for fine tuning can be passed to the checker in a properties
-file.  Its name is given with the command-line option `--tuning=my.properties.`
+file.  Its name is given with the command-line option `--tuning-options-file=my.properties`.
 This file supports variable substitution, e.g., `${x}` is replaced with the
 value of `x`, if it was previously declared.
 
 Alternatively, you can pass the tuning options right in the command-line by
-passing the option `--tune-here` that has the following format:
+passing the option `--tuning-options` that has the following format:
 
     ```
-    --tune-here=key1=val1
-    --tune-here=key1=val1:key2=val2
+    --tuning-options=key1=val1
+    --tuning-options=key1=val1:key2=val2
     ...
     ```
 
+The following options are supported:
+
 1. __Randomization__: `smt.randomSeed=<int>` passes the random seed to `z3` (via
    `z3`'s parameters `sat.random_seed` and `smt.random_seed`).
 

mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala

@@ -221,7 +221,7 @@ object Tool extends LazyLogging {
     setCoreOptions(executor, check)
 
     var tuning =
-      if (check.tuning != "") loadProperties(check.tuning) else Map[String, String]()
+      if (check.tuningOptionsFile != "") loadProperties(check.tuningOptionsFile) else Map[String, String]()
     tuning = overrideProperties(tuning, check.tuningOptions)
     logger.info("Tuning: " + tuning.toList.map { case (k, v) => s"$k=$v" }.mkString(":"))
 
@@ -367,7 +367,7 @@ object Tool extends LazyLogging {
     def parseKeyValue(text: String): (String, String) = {
       val parts = text.split('=')
       if (parts.length != 2 || parts.head.trim == "" || parts(1) == "") {
-        throw new PassOptionException(s"Expected key=value in --tune-here=$propsAsString")
+        throw new PassOptionException(s"Expected key=value in --tuning-options=$propsAsString")
       } else {
         // trim to remove surrounding whitespace from the key, but allow the value to have white spaces
         (parts.head.trim, parts(1))

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala

@@ -28,12 +28,13 @@ class CheckCmd extends AbstractCheckerCmd(name = "check", description = "Check a
   var smtEncoding: SMTEncoding = opt[SMTEncoding](name = "smt-encoding", useEnv = true, default = oopsla19Encoding,
       description =
         "the SMT encoding: oopsla19, arrays (experimental), default: oopsla19 (overrides envvar SMT_ENCODING)")
-  var tuning: String =
-    opt[String](name = "tuning", default = "", description = "filename of the tuning options, see docs/tuning.md")
+  var tuningOptionsFile: String =
+    opt[String](name = "tuning-options-file", default = "",
+        description = "filename of the tuning options, see docs/tuning.md")
   var tuningOptions: String =
     opt[String](name = "tuning-options", default = "",
         description =
-          "tuning options as arguments in the format key1=val1:key2=val2:key3=val3 (priority over --tuning)")
+          "tuning options as arguments in the format key1=val1:key2=val2:key3=val3 (priority over --tuning-options-file)")
   var discardDisabled: Boolean = opt[Boolean](name = "discard-disabled", default = true,
       description =
         "pre-check, whether a transition is disabled, and discard it, to make SMT queries smaller, default: true")

test/tla/cli-integration-tests.md

@@ -1119,7 +1119,7 @@ EXITCODE: OK
 ### check reorderTest.tla MayFail succeeds: fixed SMT fails under SMT-based assignment finding
 
 ```sh
-$ apalache-mc check --next=MayFail --tuning=reorderTest.properties reorderTest.tla | sed 's/I@.*//'
+$ apalache-mc check --next=MayFail --tuning-options-file=reorderTest.properties reorderTest.tla | sed 's/I@.*//'
 ...
 The outcome is: NoError
 ...