From 16ca13055dae8c87f624e3ef72f5e1eb7cb63527 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Sat, 7 Dec 2019 14:46:53 +0100 Subject: [PATCH] towards #76: a parser for TLC config files (not integrated yet), 8 hours --- pom.xml | 6 + .../apalache/io/tlc/TlcConfigLexer.scala | 54 ----- .../apalache/io/tlc/TlcConfigParser.scala | 154 +++++++++++- .../apalache/io/tlc/config/TlcConfig.scala | 49 ++++ .../io/tlc/config/TlcConfigLexer.scala | 99 ++++++++ .../io/tlc/config/TlcConfigParseError.scala | 15 ++ .../io/tlc/config/TlcConfigTokenReader.scala | 10 + .../apalache/io/tlc/config/tokens.scala | 93 ++++++++ .../apalache/io/tlc/TestTlcConfigParser.scala | 219 ++++++++++++++++++ 9 files changed, 643 insertions(+), 56 deletions(-) delete mode 100644 tla-import/src/main/scala/at/forsyte/apalache/io/tlc/TlcConfigLexer.scala create mode 100644 tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/TlcConfig.scala create mode 100644 tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/TlcConfigLexer.scala create mode 100644 tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/TlcConfigParseError.scala create mode 100644 tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/TlcConfigTokenReader.scala create mode 100644 tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/tokens.scala create mode 100644 tla-import/src/test/scala/at/forsyte/apalache/io/tlc/TestTlcConfigParser.scala diff --git a/pom.xml b/pom.xml index d5e3f98f20..63be040aa7 100644 --- a/pom.xml +++ b/pom.xml @@ -103,6 +103,12 @@ 3.5.0 + + org.scala-lang.modules + scala-parser-combinators + 1.1.2 + + junit junit diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/TlcConfigLexer.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/TlcConfigLexer.scala deleted file mode 100644 index 5761e003bc..0000000000 --- a/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/TlcConfigLexer.scala +++ /dev/null @@ -1,54 +0,0 @@ -package at.forsyte.apalache.io.tlc - -import at.forsyte.apalache.io.tlc.config._ - -import scala.util.parsing.combinator.RegexParsers - -/** - * A lexer for the TLC configuration files. - * - * @author Igor Konnov - */ -object TlcConfigLexer extends RegexParsers { - override def skipWhitespace: Boolean = true - - def identifier: Parser[Ident] = { - "[a-zA-Z_][a-zA-Z0-9_]*".r ^^ { name => Ident(name) } - } - - def constant: Parser[Constant] = { - "CONSTANT(S|)".r ^^ (_ => Constant()) - } - - def init: Parser[Init] = { - "INIT" ^^ (_ => Init()) - } - - def next: Parser[Next] = { - "NEXT" ^^ (_ => Next()) - } - - def specification: Parser[Specification] = { - "SPECIFICATION" ^^ (_ => Specification()) - } - - def invariant: Parser[Invariant] = { - "INVARIANT" ^^ (_ => Invariant()) - } - - def property: Parser[Property] = { - "PROPERT(Y|IES)" ^^ (_ => Property()) - } - - def constraint: Parser[Constraint] = { - "CONSTRAINT" ^^ (_ => Constraint()) - } - - def assign: Parser[Assign] = { - "<-" ^^ (_ => Assign()) - } - - def eq: Parser[Eq] = { - "=" ^^ (_ => Eq()) - } -} diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/TlcConfigParser.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/TlcConfigParser.scala index 3963e9da74..0347638565 100644 --- a/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/TlcConfigParser.scala +++ b/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. + *

A parser for the TLC configuration files. For the syntax, + * see [Specifying Systems, 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.

+ * + *

This parser is built using + * Scala parser combinators.

* * @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 }) + } } diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/TlcConfig.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/TlcConfig.scala new file mode 100644 index 0000000000..056042345f --- /dev/null +++ b/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) diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/TlcConfigLexer.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/TlcConfigLexer.scala new file mode 100644 index 0000000000..4875084147 --- /dev/null +++ b/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 + +/** + *

A lexer for the TLC configuration files.

+ * + *

This code follows the + * tutorial on scanners.

+ * + * @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()) + } +} diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/TlcConfigParseError.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/TlcConfigParseError.scala new file mode 100644 index 0000000000..1066ec6fbb --- /dev/null +++ b/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) + } +} diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/TlcConfigTokenReader.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/TlcConfigTokenReader.scala new file mode 100644 index 0000000000..c3b12821dd --- /dev/null +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/TlcConfigTokenReader.scala @@ -0,0 +1,10 @@ +package at.forsyte.apalache.io.tlc.config + +import scala.util.parsing.input.{NoPosition, Position, Reader} + +class TlcConfigTokenReader(tokens: Seq[TlcConfigToken]) extends Reader[TlcConfigToken] { + override def first: TlcConfigToken = tokens.head + override def atEnd: Boolean = tokens.isEmpty + override def pos: Position = if (tokens.isEmpty) NoPosition else tokens.head.pos + override def rest: Reader[TlcConfigToken] = new TlcConfigTokenReader(tokens.tail) +} diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/tokens.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/tokens.scala new file mode 100644 index 0000000000..c90aaf58db --- /dev/null +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/config/tokens.scala @@ -0,0 +1,93 @@ +package at.forsyte.apalache.io.tlc.config + +import scala.util.parsing.input.Positional + +/** + * A token. + */ +sealed trait TlcConfigToken extends Positional + +/** + * An identifier + * @param name the name associated with the identifier + */ +case class IDENT(name: String) extends TlcConfigToken { + override def toString: String = "identifier '%s'".format(name) +} + +/** + * The CONSTANT keyword. + */ +case class CONST() extends TlcConfigToken { + override def toString: String = "CONSTANT" +} + +/** + * The INIT keyword. + */ +case class INIT() extends TlcConfigToken { + override def toString: String = "INIT" +} + +/** + * The NEXT keyword. + */ +case class NEXT() extends TlcConfigToken { + override def toString: String = "NEXT" +} + +/** + * The SPECIFICATION keyword. + */ +case class SPECIFICATION() extends TlcConfigToken { + override def toString: String = "SPECIFICATION" +} + +/** + * The INVARIANT keyword. + */ +case class INVARIANT() extends TlcConfigToken { + override def toString: String = "INVARIANT" +} + +/** + * The PROPERTY keyword. + */ +case class PROPERTY() extends TlcConfigToken { + override def toString: String = "PROPERTY" +} + +/** + * The CONSTRAINT keyword (for state constraints). + */ +case class CONSTRAINT() extends TlcConfigToken { + override def toString: String = "CONSTRAINT" +} + +/** + * The ACTION_CONSTRAINT keyword (for action constraints). + */ +case class ACTION_CONSTRAINT() extends TlcConfigToken { + override def toString: String = "ACTION_CONSTRAINT" +} + +/** + * A hint about using symmetry. + */ +case class SYMMETRY() extends TlcConfigToken { + override def toString: String = "SYMMETRY" +} + +/** + * An assignment "<-". + */ +case class LEFT_ARROW() extends TlcConfigToken { + override def toString: String = "<-" +} + +/** + * An equality "=". + */ +case class EQ() extends TlcConfigToken { + override def toString: String = "=" +} \ No newline at end of file diff --git a/tla-import/src/test/scala/at/forsyte/apalache/io/tlc/TestTlcConfigParser.scala b/tla-import/src/test/scala/at/forsyte/apalache/io/tlc/TestTlcConfigParser.scala new file mode 100644 index 0000000000..afd8431d08 --- /dev/null +++ b/tla-import/src/test/scala/at/forsyte/apalache/io/tlc/TestTlcConfigParser.scala @@ -0,0 +1,219 @@ +package at.forsyte.apalache.io.tlc + +import at.forsyte.apalache.io.tlc.config.{InitNextSpec, TemporalSpec, TlcConfigParseError} +import org.junit.runner.RunWith +import org.scalatest.FunSuite +import org.scalatest.junit.JUnitRunner + +/** + * Tests for the TLC configuration parser. + * + * @author Igor Konnov + */ +@RunWith(classOf[JUnitRunner]) +class TestTlcConfigParser extends FunSuite { + + test("INIT-NEXT") { + val text = + """ + |INIT Init + |NEXT Next + """.stripMargin + + val config = TlcConfigParser(text) + assert(config.behaviorSpec == InitNextSpec("Init", "Next")) + } + + test("Malformed INIT-NEXT") { + val text = + """ + |INIT + |NEXT Next + """.stripMargin + + assertThrows[TlcConfigParseError](TlcConfigParser(text)) + } + + test("SPECIFICATION") { + val text = + """ + |SPECIFICATION Spec + """.stripMargin + + val config = TlcConfigParser(text) + assert(config.behaviorSpec == TemporalSpec("Spec")) + } + + test("CONSTANT assignments") { + val text = + """ + |CONSTANT + |N = M + |K = L + |INIT Init + |NEXT Next + """.stripMargin + + val config = TlcConfigParser(text) + assert(config.constAssignments == Map("N" -> "M", "K" -> "L")) + assert(config.constReplacements.isEmpty) + } + + test("CONSTANT assignments and SYMMETRY") { + val text = + """ + |CONSTANT + |N = M + |\* symmetry definitions are skipped by our parser + |SYMMETRY symmDef1 + |CONSTANT K = L + |INIT Init + |NEXT Next + """.stripMargin + + val config = TlcConfigParser(text) + assert(config.constAssignments == Map("N" -> "M", "K" -> "L")) + assert(config.constReplacements.isEmpty) + } + + test("CONSTANT replacements") { + val text = + """ + |CONSTANT + |A <- B + |C <- D + |INIT Init + |NEXT Next + """.stripMargin + + val config = TlcConfigParser(text) + assert(config.constAssignments.isEmpty) + assert(config.constReplacements == Map("A" -> "B", "C" -> "D")) + } + + test("CONSTANT assignments and replacements") { + val text = + """ + |CONSTANTS + |N = M + |A <- B + |K = L + |C <- D + |INIT Init + |NEXT Next + """.stripMargin + + val config = TlcConfigParser(text) + assert(config.constAssignments == Map("N" -> "M", "K" -> "L")) + assert(config.constReplacements == Map("A" -> "B", "C" -> "D")) + } + + test("INIT-NEXT and INVARIANTS") { + val text = + """ + |INIT Init + |NEXT Next + |INVARIANT Inv1 + |INVARIANTS Inv2 + """.stripMargin + + val config = TlcConfigParser(text) + assert(config.behaviorSpec == InitNextSpec("Init", "Next")) + assert(config.invariants == List("Inv1", "Inv2")) + } + + test("INIT-NEXT and PROPERTIES") { + val text = + """ + |INIT Init + |NEXT Next + |PROPERTY Prop1 + |PROPERTIES Prop2 + """.stripMargin + + val config = TlcConfigParser(text) + assert(config.behaviorSpec == InitNextSpec("Init", "Next")) + assert(config.temporalProps == List("Prop1", "Prop2")) + } + + test("INIT-NEXT and CONSTRAINTS") { + val text = + """ + |CONSTRAINTS Cons1 + |Cons2 + |INIT Init + |NEXT Next + """.stripMargin + + val config = TlcConfigParser(text) + assert(config.behaviorSpec == InitNextSpec("Init", "Next")) + assert(config.stateConstraints == List("Cons1", "Cons2")) + } + + test("INIT-NEXT and ACTION_CONSTRAINTS") { + val text = + """ + |ACTION_CONSTRAINTS Cons1 + |Cons2 + |INIT Init + |NEXT Next + """.stripMargin + + val config = TlcConfigParser(text) + assert(config.behaviorSpec == InitNextSpec("Init", "Next")) + assert(config.actionConstraints == List("Cons1", "Cons2")) + } + + test("INIT-NEXT and single-line comments") { + val text = + """ + |\* this is the initialization section + |INIT Init + |\* this the transition relation + |NEXT Next + """.stripMargin + + val config = TlcConfigParser(text) + assert(config.behaviorSpec == InitNextSpec("Init", "Next")) + } + + test("INIT-NEXT and multi-line comments") { + val text = + """ + |(* + | this is the initialization section + | *) + |INIT Init + |(* + | * This is the transition predicate + | *) + |NEXT Next + """.stripMargin + + val config = TlcConfigParser(text) + assert(config.behaviorSpec == InitNextSpec("Init", "Next")) + } + + test("all features") { + val text = + """ + |CONSTANTS + |N = M + |A <- B + |CONSTRAINT + |Cons1 + |ACTION_CONSTRAINT + |Cons2 + |INIT Init + |NEXT Next + |INVARIANT + |Inv + |PROPERTY + |Prop + """.stripMargin + + val config = TlcConfigParser(text) + assert(config.constAssignments == Map("N" -> "M")) + assert(config.constReplacements == Map("A" -> "B")) + } +}