towards #76: a parser for TLC config files (not integrated yet), 8 hours

pom.xml

@@ -103,6 +103,12 @@
                 <version>3.5.0</version>
             </dependency>
 
+            <dependency>
+                <groupId>org.scala-lang.modules</groupId>
+                <artifactId>scala-parser-combinators</artifactId>
+                <version>1.1.2</version>
+            </dependency>
+
             <dependency>
                 <groupId>junit</groupId>
                 <artifactId>junit</artifactId>

tla-import/src/main/scala/at/forsyte/apalache/io/tlc/TlcConfigParser.scala

@@ -1,10 +1,160 @@
 package at.forsyte.apalache.io.tlc
 
+import java.io.{Reader, StringReader}
+
+import at.forsyte.apalache.io.tlc.config._
+
+import scala.util.parsing.combinator.Parsers
+import scala.util.parsing.input.NoPosition
+
+
 /**
-  * A parser for the TLC configuration files.
+  * <p>A parser for the TLC configuration files. For the syntax,
+  * see [<a href="http://research.microsoft.com/users/lamport/tla/book.html">Specifying Systems</a>, Ch. 14]
+  * by Leslie Lamport. TLC configuration files have a rich assignment syntax, e.g., one can write a parameter assignment
+  * `S = {{1, 2, 3}, "a"}`. We ignore this syntax, as TLA Toolbox produces configuration files using the replacement
+  * syntax `S <- const...`. The only exception is when one uses model values, e.g., `S = S`, which we also support.</p>
+  *
+  * <p>This parser is built using
+  * <a href="https://github.com/scala/scala-parser-combinators">Scala parser combinators</a>.</p>
   *
   * @author Igor Konnov
   */
-class TlcConfigParser {
+object TlcConfigParser extends Parsers {
+  override type Elem = TlcConfigToken
+
+  private abstract class ConstBinding
+  private case class ConstAssignment(name: String, assignment: String) extends ConstBinding
+  private case class ConstReplacement(name: String, replacement: String) extends ConstBinding
+
+  /**
+    * Parse a configuration file from a reader.
+    * @param reader a reader
+    * @return a config on success; throws TlcConfigParseError on failure
+    */
+  def apply(reader: Reader): TlcConfig = {
+    config(new TlcConfigTokenReader(TlcConfigLexer(reader))) match {
+      case Success(config: TlcConfig, _) => config
+      case Success(_, _) => throw new TlcConfigParseError("Unexpected parse result", NoPosition)
+      case Failure(msg, next) => throw new TlcConfigParseError(msg, next.pos)
+      case Error(msg, next) => throw new TlcConfigParseError(msg, next.pos)
+    }
+  }
+
+  /**
+    * Parse a configuration file from a string.
+    * @param text a string
+    * @return a config on success; throws TlcConfigParseError on failure
+    */
+  def apply(text: String): TlcConfig = {
+    apply(new StringReader(text))
+  }
+
+  // the access point
+  private def config: Parser[TlcConfig] = {
+    phrase(allConstLists ~ allConstraintLists ~ allActionConstraintLists ~
+        (initNextSection | specSection) ~ allInvariantLists ~ allPropertyLists) ^^ {
+      case consts ~ stateConstraints ~ actionConstraints ~ spec ~ invariants ~ properties =>
+        val assignments = consts.collect { case ConstAssignment(nm, asgn) => nm -> asgn }
+        val replacements = consts.collect { case ConstReplacement(nm, repl) => nm -> repl }
+        TlcConfig(
+          constAssignments = Map(assignments :_*),
+          constReplacements = Map(replacements :_*),
+          stateConstraints = stateConstraints,
+          actionConstraints = actionConstraints,
+          invariants = invariants,
+          temporalProps = properties,
+          spec)
+    }
+  }
+
+  private def allConstLists: Parser[List[ConstBinding]] = {
+    rep(constList | symmetryHint) ^^ {
+      lists => lists.flatten
+    }
+  }
+
+  private def constList: Parser[List[ConstBinding]] = {
+    CONST() ~ rep1(assignOrReplace) ^^ {
+      case _ ~ bindingList => bindingList
+    }
+  }
+
+  // Constants can come with SYMMETRY definitions. The parser just swallows them.
+  private def symmetryHint: Parser[List[ConstBinding]] = {
+    SYMMETRY() ~ ident ^^ {
+      case _ ~ _ => List() // ignore the SYMMETRY definitions
+    }
+  }
+
+  private def assignOrReplace: Parser[ConstBinding] = {
+    ident ~ (EQ() | LEFT_ARROW()) ~ ident ^^ {
+      case IDENT(lhs) ~ EQ() ~ IDENT(rhs) => ConstAssignment(lhs, rhs)
+      case IDENT(lhs) ~ LEFT_ARROW() ~ IDENT(rhs) => ConstReplacement(lhs, rhs)
+    }
+  }
+
+  private def allConstraintLists: Parser[List[String]] = {
+    rep(constraintList) ^^ {
+      lists => lists.flatten
+    }
+  }
+
+  private def constraintList: Parser[List[String]] = {
+    CONSTRAINT() ~ rep1(ident) ^^ {
+      case _ ~ list => list.collect { case IDENT(name) => name }
+    }
+  }
+
+  private def allActionConstraintLists: Parser[List[String]] = {
+    rep(actionConstraintList) ^^ {
+      lists => lists.flatten
+    }
+  }
+
+  private def actionConstraintList: Parser[List[String]] = {
+    ACTION_CONSTRAINT() ~ rep1(ident) ^^ {
+      case _ ~ list => list.collect { case IDENT(name) => name }
+    }
+  }
+
+  private def initNextSection: Parser[BehaviorSpec] = {
+    INIT() ~ ident ~ NEXT() ~ ident ^^ {
+      case _ ~ IDENT(initName) ~ _ ~ IDENT(nextName) => InitNextSpec(initName, nextName)
+    }
+  }
+
+  private def specSection: Parser[BehaviorSpec] = {
+    SPECIFICATION() ~ ident ^^ {
+      case _ ~ IDENT(specName) => TemporalSpec(specName)
+    }
+  }
+
+  private def allInvariantLists: Parser[List[String]] = {
+    rep(invariantList) ^^ {
+      lists => lists.flatten
+    }
+  }
+
+  private def invariantList: Parser[List[String]] = {
+    INVARIANT() ~ rep1(ident) ^^ {
+      case _ ~ list => list.collect { case IDENT(name) => name }
+    }
+  }
+
+  private def allPropertyLists: Parser[List[String]] = {
+    rep(propertyList) ^^ {
+      lists => lists.flatten
+    }
+  }
+
+  private def propertyList: Parser[List[String]] = {
+    PROPERTY() ~ rep1(ident) ^^ {
+      case _ ~ list => list.collect { case IDENT(name) => name }
+    }
+  }
 
+  private def ident: Parser[IDENT] = {
+    accept("identifier", { case id @ IDENT(_) => id })
+  }
 }

tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/TlcConfig.scala

@@ -0,0 +1,49 @@
+package at.forsyte.apalache.io.tlc.config
+
+/**
+  * A behavior spec is either Init-Next, or a temporal specification Init /\ [] [Next]_vars /\ Temporal.
+  */
+abstract sealed class BehaviorSpec
+
+/**
+  * The behavior is given by INIT and NEXT.
+  *
+  * @param init name of the Init predicate
+  * @param next name of the Next predicate
+  */
+case class InitNextSpec(init: String, next: String) extends BehaviorSpec
+
+/**
+  * The behavior is given by SPECIFICATION, that is, a definition of the form Init /\ [] [Next]_vars /\ Temporal.
+  *
+  * @param name the name of the specification definition
+  */
+case class TemporalSpec(name: String) extends BehaviorSpec
+
+/**
+  * A parsed TLC configuration file. The case class is used here to make copying easier.
+  *
+  * @param constAssignments  Assignments of the form MyParam = ModelValue, which makes TLC to replace MyParam with
+  *                          a model value. Although TLC supports other kinds of values, e.g., 1, "foo", { 1, 2, 3 },
+  *                          we do not like to write a complex parser.
+  *                          Use a replacement, if you have richer expressions.
+  * @param constReplacements Replacements of the form MyParam <- AnotherDef. In this case,
+  *                          AnotherDef has to be defined in the respective TLA+ module.
+  *
+  * @param stateConstraints state constraints
+  * @param actionConstraints action constraints
+  * @param invariants A list of invariants to check.
+  *
+  * @param temporalProps A list of temporal properties to check.
+  *
+  * @param behaviorSpec A behavior specification. A well-formed config should have one.
+  *
+  * @author Igor Konnov
+  */
+case class TlcConfig(constAssignments: Map[String, String],
+                     constReplacements: Map[String, String],
+                     stateConstraints: List[String],
+                     actionConstraints: List[String],
+                     invariants: List[String] = List(),
+                     temporalProps: List[String],
+                     behaviorSpec: BehaviorSpec)

tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/TlcConfigLexer.scala

@@ -0,0 +1,99 @@
+package at.forsyte.apalache.io.tlc.config
+
+import java.io.Reader
+
+import scala.util.matching.Regex
+import scala.util.parsing.combinator.RegexParsers
+
+/**
+  * <p>A lexer for the TLC configuration files.</p>
+  *
+  * <p>This code follows the
+  * <a href="http://nielssp.dk/2015/07/creating-a-scanner-using-parser-combinators-in-scala">tutorial on scanners</a>.</p>
+  *
+  * @author Igor Konnov
+ */
+object TlcConfigLexer extends RegexParsers {
+  override def skipWhitespace: Boolean = true
+  override val whiteSpace: Regex = "[ \t\r\f]+".r // process linefeed separately, in order to parse one-line comments
+
+  /**
+    * Parse the input stream and return the list of tokens. Although collecting the list of all tokens in memory is
+    * not optimal, TLC configurations files are tiny, so it should not be a big deal.
+    *
+    * @param reader a Java reader
+    * @return the list of parsed tokens
+    * @throws TlcConfigParseError when the lexer finds an error
+    */
+  def apply(reader: Reader): List[TlcConfigToken] = parseAll(program, reader) match {
+    case Success(result, _) => result
+    case NoSuccess(msg, next) => throw new TlcConfigParseError(msg, next.pos)
+  }
+
+  def program: Parser[List[TlcConfigToken]] = skip ~> rep(token <~ skip) <~ eof
+
+  def eof: Parser[String] = "\\z".r | failure("unexpected character")
+
+  def token: Parser[TlcConfigToken] =
+    positioned(
+      constant | init | next | specification | invariant | property | constraint | actionConstraint |
+        symmetry | leftArrow | eq | identifier
+    ) ///
+
+  // it is important that linefeed is not a whiteSpace, as otherwise singleComment consumes the whole input!
+  def skip: Parser[Unit] = rep(whiteSpace | singleComment | multiComment | linefeed) ^^^ Unit
+
+  def linefeed: Parser[Unit] = "\n" ^^^ Unit
+
+  def singleComment: Parser[Unit] = "\\*" ~ rep(not("\n") ~ ".".r) ^^^ Unit
+
+  def multiComment: Parser[Unit] = "(*" ~ rep(not("*)") ~ "(?s).".r) ~ "*)" ^^^ Unit
+
+  private def identifier: Parser[IDENT] = {
+    "[a-zA-Z_][a-zA-Z0-9_]*".r ^^ { name => IDENT(name) }
+  }
+
+  private def constant: Parser[CONST] = {
+    "CONSTANT(S|)".r  ^^ (_ => CONST())
+  }
+
+  private def init: Parser[INIT] = {
+    "INIT"  ^^ (_ => INIT())
+  }
+
+  private def next: Parser[NEXT] = {
+    "NEXT"  ^^ (_ => NEXT())
+  }
+
+  private def specification: Parser[SPECIFICATION] = {
+    "SPECIFICATION" ^^ (_ => SPECIFICATION())
+  }
+
+  private def invariant: Parser[INVARIANT] = {
+    "INVARIANT(S|)".r ^^ (_ => INVARIANT())
+  }
+
+  private def property: Parser[PROPERTY] = {
+    "PROPERT(Y|IES)".r ^^ (_ => PROPERTY())
+  }
+
+  private def constraint: Parser[CONSTRAINT] = {
+    "CONSTRAINT(S|)".r ^^ (_ => CONSTRAINT())
+  }
+
+  private def actionConstraint: Parser[ACTION_CONSTRAINT] = {
+    "ACTION_CONSTRAINT(S|)".r ^^ (_ => ACTION_CONSTRAINT())
+  }
+
+  private def symmetry: Parser[SYMMETRY] = {
+    "SYMMETRY".r ^^ (_ => SYMMETRY())
+  }
+
+  private def leftArrow: Parser[LEFT_ARROW] = {
+    "<-" ^^ (_ => LEFT_ARROW())
+  }
+
+  private def eq: Parser[EQ] = {
+    "=" ^^ (_ => EQ())
+  }
+}

tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/TlcConfigParseError.scala

@@ -0,0 +1,15 @@
+package at.forsyte.apalache.io.tlc.config
+
+import scala.util.parsing.input.Position
+
+/**
+  * The exception thrown by TlcConfigParser if any error occurs.
+ *
+  * @param msg the error message
+  * @param pos a position in the input
+  */
+class TlcConfigParseError(val msg: String, val pos: Position) extends Exception(msg) {
+  override def toString: String = {
+    "Config parse error at %s: %s".format(pos, msg)
+  }
+}