using Apache commons-configuration2, which allows variable substitution

docs/tuning.md

@@ -2,8 +2,17 @@ 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.`` 
+Its name is given with the command-line option ``--tuning=my.properties.`` This file
+supports variable substitution, e.g., ``${x}`` is replaced with the value of ``x``, if it was
+previously declared.
+
 
+  1. __Timeouts__: ``search.transition.timeout=<seconds>`` and ``search.invariant.timeout=<seconds>`` set timeouts
+  in seconds for checking whether a transition is enabled and whether the invariant holds, respectively.
+  When a timeout occurs, while transition is checked, the transition is considered disabled
+  and the search continues. When a timeout occurs, while the invariant is checked, the invariant
+  is considered satisfied. Obviously, one can miss a bug by setting small timeouts.
+
   1. __Guided search__: ``search.transitionFilter=<sequence>``. Restrict the choice of symbolic
   transitions at every step with a regular expression. For instance, ``search.filter=0,5,2|3``
   requres to start with the 0th transition, continue with the 5th transition,

mod-tool/pom.xml

@@ -119,6 +119,18 @@
             <artifactId>clist-macros_2.12</artifactId>
             <version>3.2.2</version>
         </dependency>
+        <dependency>
+            <!-- configurations in property files -->
+            <groupId>org.apache.commons</groupId>
+            <artifactId>commons-configuration2</artifactId>
+            <version>2.4</version>
+        </dependency>
+        <dependency>
+            <!-- commons-configuration2 uses commons-beanutiles (without declaring it in dependencies?) -->
+            <groupId>commons-beanutils</groupId>
+            <artifactId>commons-beanutils</artifactId>
+            <version>1.9.3</version>
+        </dependency>
         <dependency>
             <groupId>ch.qos.logback</groupId>
             <artifactId>logback-classic</artifactId>

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

@@ -1,12 +1,11 @@
 package at.forsyte.apalache.tla
 
-import java.io.{FileNotFoundException, FileReader, IOException}
+import java.io.{File, FileNotFoundException, FileReader, IOException}
 import java.time.LocalDateTime
 import java.time.temporal.ChronoUnit
 import java.util.Properties
 
 import scala.collection.JavaConverters._
-
 import at.forsyte.apalache.infra.PassOptionException
 import at.forsyte.apalache.infra.log.LogbackConfigurator
 import at.forsyte.apalache.infra.passes.{PassChainExecutor, TlaModuleMixin}
@@ -17,6 +16,9 @@ import at.forsyte.apalache.tla.tooling.Version
 import at.forsyte.apalache.tla.tooling.opt.{CheckCmd, ParseCmd}
 import com.google.inject.Guice
 import com.typesafe.scalalogging.LazyLogging
+import org.apache.commons.configuration2.Configuration
+import org.apache.commons.configuration2.builder.fluent.Configurations
+import org.apache.commons.configuration2.ex.ConfigurationException
 import org.backuity.clist.Cli
 
 /**
@@ -120,22 +122,21 @@ object Tool extends App with LazyLogging {
   }
 
   private def loadProperties(filename: String): Map[String, String] = {
-    val props = new Properties()
+    // use an apache-commons library, as it supports variable substitution
     try {
-      val reader = new FileReader(filename)
-      props.load(reader)
-      reader.close()
+      val config = new Configurations().properties(new File(filename))
+      // access configuration properties
       var map = Map[String, String]()
-      for (name: String <- props.stringPropertyNames().asScala) {
-        map += (name -> props.getProperty(name)) // this seems to be the easiest way to convert Properties
+      for (name: String <- config.getKeys.asScala) {
+        map += (name -> config.getString(name))
       }
       map
     } catch {
       case _: FileNotFoundException =>
         throw new PassOptionException(s"The properties file $filename not found")
 
-      case e: IOException =>
-        throw new PassOptionException(s"IO error while reading properties from $filename: ${e.getMessage}")
+      case e: ConfigurationException =>
+        throw new PassOptionException(s"Error in the properties file $filename: ${e.getMessage}")
     }
   }