From 895b94fae2e18e657857afa938ccafb95d778ff7 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 3 May 2021 18:21:34 +0200 Subject: [PATCH 1/7] add tla levels and pbt tests for them --- pom.xml | 2 + .../forsyte/apalache/tla/lir/TlaLevel.scala | 92 +++++++++++++++++ .../apalache/tla/lir/TlaLevelFinder.scala | 39 ++++++++ .../apalache/tla/lir/IrGenerators.scala | 20 +++- .../apalache/tla/lir/TestTlaLevelFinder.scala | 98 +++++++++++++++++++ 5 files changed, 250 insertions(+), 1 deletion(-) create mode 100644 tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaLevel.scala create mode 100644 tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaLevelFinder.scala create mode 100644 tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaLevelFinder.scala diff --git a/pom.xml b/pom.xml index dfefc8d97d..f97ce90a3e 100644 --- a/pom.xml +++ b/pom.xml @@ -43,6 +43,8 @@ tla-assignments tla-bmcmt + + tla-script mod-tool diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaLevel.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaLevel.scala new file mode 100644 index 0000000000..12cb1501e6 --- /dev/null +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaLevel.scala @@ -0,0 +1,92 @@ +package at.forsyte.apalache.tla.lir + +/** + * The level of a TLA+ expression, as explained in: Lamport. Specifying Systems, p. 322. + */ +sealed trait TlaLevel extends Ordered[TlaLevel] { + + /** + * The level number as assigned in the book. + */ + val level: Int + + /** + * A textual representation of the level. + */ + val name: String + + /** + * Compare this level to another level. + * + * @param that the level to compare + * @return 0, if the levels are equal; a negative number if `this` is smaller than `that`, and a positive number + * if `this` is larger than `that`. + */ + override def compare(that: TlaLevel): Int = { + level - that.level + } + + /** + * Join the levels by computing the smallest level that covers both of `this` and `that`. + * + * @param that the level to join with + * @return the minimal level j that satisfies: `j <= this` and `j <= that`. + */ + def join(that: TlaLevel): TlaLevel = { + TlaLevel.fromInt(Math.max(level, that.level)) + } + + /** + * Join the level with a sequence of level + * + * @param otherLevels a sequence of levels + * @return the join of `this` and otherLevels + */ + def join(otherLevels: Seq[TlaLevel]): TlaLevel = { + otherLevels.foldLeft(this) { case (l, r) => l.join(r) } + } +} + +object TlaLevel { + private val INT_TO_LEVEL = Seq(TlaLevelConst, TlaLevelState, TlaLevelAction, TlaLevelTemporal) + + def fromInt(level: Int): TlaLevel = { + if (level < 0 || level >= INT_TO_LEVEL.length) { + throw new IllegalArgumentException(s"Unexpected level of TlaValue: $level") + } else { + INT_TO_LEVEL(level) + } + } +} + +/** + * Constant level: constants and constant-level expressions. + */ +case object TlaLevelConst extends TlaLevel { + override val level: Int = 0 + override val name: String = "Constant" +} + +/** + * State level: the constant-level, state variables, and expressions over them that are not actions or temporal formulas. + */ +case object TlaLevelState extends TlaLevel { + override val level: Int = 1 + override val name: String = "State" +} + +/** + * Action level: the state level, state variables, primed state variables, and action operators. + */ +case object TlaLevelAction extends TlaLevel { + override val level: Int = 2 + override val name: String = "Action" +} + +/** + * Temporal level: the action level and temporal formulas. + */ +case object TlaLevelTemporal extends TlaLevel { + override val level: Int = 3 + override val name: String = "Temporal" +} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaLevelFinder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaLevelFinder.scala new file mode 100644 index 0000000000..2d4c266001 --- /dev/null +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaLevelFinder.scala @@ -0,0 +1,39 @@ +package at.forsyte.apalache.tla.lir + +import at.forsyte.apalache.tla.lir.oper.{TlaActionOper, TlaTempOper} + +/** + * This class computes the level of a TLA+ expression. See Lamport. Specifying Systems, p. 322. + * + * @param nameLevel a function that returns the level of a name. + * @author Igor Konnov + */ +class TlaLevelFinder(nameLevel: String => TlaLevel) { + def apply(ex: TlaEx): TlaLevel = find(ex) + + private def find: TlaEx => TlaLevel = { + case NameEx(name) => + nameLevel(name) + + case OperEx(op, args @ _*) + if op == TlaActionOper.prime || op == TlaActionOper.enabled + || op == TlaActionOper.unchanged || op == TlaActionOper.stutter + || op == TlaActionOper.nostutter || op == TlaActionOper.composition => + TlaLevelAction.join(args.map(find)) + + case OperEx(op, args @ _*) + if op == TlaTempOper.box || op == TlaTempOper.diamond || op == TlaTempOper.leadsTo + || op == TlaTempOper.weakFairness || op == TlaTempOper.strongFairness + || op == TlaTempOper.guarantees || op == TlaTempOper.AA || op == TlaTempOper.EE => + TlaLevelTemporal.join(args.map(find)) + + case OperEx(_, args @ _*) => + TlaLevelConst.join(args.map(find)) + + case LetInEx(body, defs @ _*) => + find(body).join(defs.map(d => find(d.body))) + + case _ => + TlaLevelConst + } +} diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/IrGenerators.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/IrGenerators.scala index ec17e802b8..1f55343edf 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/IrGenerators.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/IrGenerators.scala @@ -62,6 +62,12 @@ trait IrGenerators { */ val simpleOperators = List(TlaOper.eq, TlaOper.ne, TlaOper.chooseBounded, TlaOper.apply) + /** + * The list of propositional operators and quantifiers, excluding unbounded quantifiers. + */ + val logicOperators = List(TlaBoolOper.and, TlaBoolOper.or, TlaBoolOper.not, TlaBoolOper.equiv, TlaBoolOper.implies, + TlaBoolOper.exists, TlaBoolOper.forall) + /** * The list of arithmetic operators that are defined in TlaArithOper. */ @@ -70,12 +76,24 @@ trait IrGenerators { TlaArithOper.uminus) /** - * The list of the most basic operators that are defined in TlaOper. + * The list of all set operators. */ val setOperators = List(TlaSetOper.cap, TlaSetOper.cup, TlaSetOper.enumSet, TlaSetOper.filter, TlaSetOper.funSet, TlaSetOper.in, TlaSetOper.notin, TlaSetOper.map, TlaSetOper.powerset, TlaSetOper.recSet, TlaSetOper.seqSet, TlaSetOper.setminus, TlaSetOper.subseteq, TlaSetOper.times, TlaSetOper.union) + /** + * The list of action operators. + */ + val actionOperators = List(TlaActionOper.prime, TlaActionOper.enabled, TlaActionOper.stutter, TlaActionOper.nostutter, + TlaActionOper.unchanged, TlaActionOper.composition) + + /** + * The list of temporal operators, excluding \AA and \EE, as those are not useful to us. + */ + val temporalOperators = List(TlaTempOper.box, TlaTempOper.diamond, TlaTempOper.leadsTo, TlaTempOper.guarantees, + TlaTempOper.strongFairness, TlaTempOper.weakFairness) + def genTypeTag: Gen[TypeTag] = for { i <- arbitrary[Int] tt <- oneOf(Untyped(), Typed[Int](i)) diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaLevelFinder.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaLevelFinder.scala new file mode 100644 index 0000000000..2df1758a18 --- /dev/null +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaLevelFinder.scala @@ -0,0 +1,98 @@ +package at.forsyte.apalache.tla.lir + +import org.junit.runner.RunWith +import org.scalacheck.Prop.{AnyOperators, forAll, passed} +import org.scalatest.FunSuite +import org.scalatest.junit.JUnitRunner +import org.scalatest.prop.Checkers + +/** + * Tests of TlaLevelFinder. + */ +@RunWith(classOf[JUnitRunner]) +class TestTlaLevelFinder extends FunSuite with Checkers { + + test("non-action operators + constants = constant level") { + val gens = new IrGenerators { + override val maxArgs: Int = 3 + } + // all names are considered constants + val finder = new TlaLevelFinder({ _ => TlaLevelConst }) + val operators = gens.simpleOperators ++ gens.setOperators ++ gens.logicOperators ++ gens.arithOperators + val prop = forAll(gens.genTlaEx(operators)(Seq())) { ex => + finder(ex) =? TlaLevelConst + } + check(prop, minSuccessful(2500), sizeRange(8)) + } + + test("non-action operators + variables = state level") { + val gens = new IrGenerators { + override val maxArgs: Int = 3 + } + // all names are considered constants + val operators = gens.simpleOperators ++ gens.setOperators ++ gens.logicOperators ++ gens.arithOperators + val prop = forAll(gens.genTlaEx(operators)(Seq())) { ex => + val finder = new TlaLevelFinder(_ => TlaLevelState) + val level = finder(ex) + if (containsName(ex)) { + level =? TlaLevelState + } else { + level =? TlaLevelConst + } + } + check(prop, minSuccessful(2500), sizeRange(8)) + } + + test("action operators + variables = action level") { + val gens = new IrGenerators { + override val maxArgs: Int = 3 + } + // all names are considered constants + val operators = gens.actionOperators + val prop = forAll(gens.genTlaEx(operators)(Seq())) { ex => + val finder = new TlaLevelFinder(_ => TlaLevelState) + val level = finder(ex) + ex match { + case OperEx(_, _*) => + level =? TlaLevelAction + + case _ => + passed + } + } + check(prop, minSuccessful(2500), sizeRange(8)) + } + + test("temporal operators + variables = temporal level") { + val gens = new IrGenerators { + override val maxArgs: Int = 3 + } + // all names are considered constants + val operators = gens.temporalOperators + val prop = forAll(gens.genTlaEx(operators)(Seq())) { ex => + val finder = new TlaLevelFinder(_ => TlaLevelState) + val level = finder(ex) + ex match { + case OperEx(_, _*) => + level =? TlaLevelTemporal + + case _ => + passed + } + } + check(prop, minSuccessful(2500), sizeRange(8)) + } + + private def containsName: TlaEx => Boolean = { + case NameEx(_) => + true + + case OperEx(_, args @ _*) => + args.map(containsName).foldLeft(false)(_ || _) + + case LetInEx(body, defs @ _*) => + defs.map(d => containsName(d.body)).foldLeft(containsName(body))(_ || _) + + case _ => false + } +} From 546042d724fc7506027c2ba765640007d1f64b2c Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 6 May 2021 12:51:38 +0200 Subject: [PATCH 2/7] add TlaDeclLevelFinder and property-based tests for it --- .../apalache/tla/lir/TlaDeclLevelFinder.scala | 55 ++++++++ ...velFinder.scala => TlaExLevelFinder.scala} | 2 +- .../apalache/tla/lir/IrGenerators.scala | 107 ++++++++------- .../tla/lir/TestTlaDeclLevelFinder.scala | 128 ++++++++++++++++++ ...inder.scala => TestTlaExLevelFinder.scala} | 18 +-- .../standard/TestPrimePropagation.scala | 5 +- 6 files changed, 257 insertions(+), 58 deletions(-) create mode 100644 tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDeclLevelFinder.scala rename tlair/src/main/scala/at/forsyte/apalache/tla/lir/{TlaLevelFinder.scala => TlaExLevelFinder.scala} (95%) create mode 100644 tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaDeclLevelFinder.scala rename tlair/src/test/scala/at/forsyte/apalache/tla/lir/{TestTlaLevelFinder.scala => TestTlaExLevelFinder.scala} (79%) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDeclLevelFinder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDeclLevelFinder.scala new file mode 100644 index 0000000000..1321861565 --- /dev/null +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDeclLevelFinder.scala @@ -0,0 +1,55 @@ +package at.forsyte.apalache.tla.lir + +/** + * This class computes the level of a TLA+ declaration by using TlaExLevelFinder. See Lamport. Specifying Systems, p. 322. + * + * @param module a TLA module that contains the declarations to query + * @author Igor Konnov + */ +class TlaDeclLevelFinder(module: TlaModule) { + private val consts = Set(module.constDeclarations.map(_.name): _*) + private val vars = Set(module.varDeclarations.map(_.name): _*) + private val defs = Map(module.operDeclarations map { d => d.name -> d }: _*) + private var levelCacheMap: Map[String, TlaLevel] = Map() + + def apply(decl: TlaDecl): TlaLevel = { + decl match { + case TlaConstDecl(_) => + TlaLevelConst + + case TlaVarDecl(_) => + TlaLevelState + + case TlaAssumeDecl(_) => + TlaLevelConst + + case TlaOperDecl(name, _, _) => + cacheLevel(Set(name), name) + levelCacheMap(name) + + case TlaTheoremDecl(_, _) => + TlaLevelConst + } + } + + private def cacheLevel(callers: Set[String], name: String): Unit = { + def levelOfName(name: String): TlaLevel = { + if (consts.contains(name)) { + TlaLevelConst + } else if (vars.contains(name)) { + TlaLevelState + } else { + if (!callers.contains(name) && defs.contains(name)) { + // as the module comes from the parser, we assume that defs contains a definition for the name `name` + cacheLevel(callers + name, name) + levelCacheMap(name) + } else { + TlaLevelConst + } + } + } + + val level = new TlaExLevelFinder(levelOfName)(defs(name).body) + levelCacheMap += name -> level + } +} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaLevelFinder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaExLevelFinder.scala similarity index 95% rename from tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaLevelFinder.scala rename to tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaExLevelFinder.scala index 2d4c266001..69e3af0c19 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaLevelFinder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaExLevelFinder.scala @@ -8,7 +8,7 @@ import at.forsyte.apalache.tla.lir.oper.{TlaActionOper, TlaTempOper} * @param nameLevel a function that returns the level of a name. * @author Igor Konnov */ -class TlaLevelFinder(nameLevel: String => TlaLevel) { +class TlaExLevelFinder(nameLevel: String => TlaLevel) { def apply(ex: TlaEx): TlaLevel = find(ex) private def find: TlaEx => TlaLevel = { diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/IrGenerators.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/IrGenerators.scala index 1f55343edf..cf90ead87e 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/IrGenerators.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/IrGenerators.scala @@ -34,12 +34,12 @@ trait IrGenerators { case class UserOperSig(name: String, nparams: Int) // an internal context of the generated operator definitions - type UserContext = Seq[UserOperSig] + type UserContext = Map[String, UserOperSig] /** * An empty user context. */ - val emptyContext: UserContext = Seq[UserOperSig]() + val emptyContext: UserContext = Map[String, UserOperSig]() /** * The maximal number of arguments in user-defined operators and built-in operators. @@ -142,8 +142,8 @@ trait IrGenerators { * * @return a generator of `NameEx(_)`. */ - def genNameEx: Gen[NameEx] = for { - s <- identifier + def genNameEx(ctx: UserContext): Gen[NameEx] = for { + s <- oneOf(ctx.keys) tt <- genTypeTag } yield NameEx(s).withTag(tt) @@ -155,8 +155,7 @@ trait IrGenerators { */ def genOperApply(exGen: UserContext => Gen[TlaEx])(ctx: UserContext): Gen[TlaEx] = sized { size => for { - declNo <- choose(0, ctx.size - 1) - decl = ctx(declNo) + decl <- oneOf(ctx.values) argGen = resize(size - 1, exGen(ctx)) args <- argsByArity(argGen)(FixedArity(decl.nparams)) tt <- genTypeTag @@ -178,11 +177,11 @@ trait IrGenerators { ndefs <- choose(1, maxDefsPerLetIn) defs <- listOfN(ndefs, resize(size - 1, genTlaOperDecl(exGen)(ctx))) suchThat { ds => // no new name is present in the context - ds.map(_.name).toSet.intersect(ctx.map(_.name).toSet).isEmpty && + ds.map(_.name).toSet.intersect(ctx.keySet).isEmpty && // and all new names are mutually unique ds.map(_.name).toSet.size == ds.size } - body <- resize(size - 1, exGen(ctx ++ defs.map(d => UserOperSig(d.name, d.formalParams.length)))) + body <- resize(size - 1, exGen(ctx ++ defs.map(d => d.name -> UserOperSig(d.name, d.formalParams.length)))) tt <- genTypeTag } yield LetInEx(body, defs: _*).withTag(tt) } @@ -199,7 +198,11 @@ trait IrGenerators { sized { size => if (size <= 1) { // no gas to generate one more operator expression - oneOf(genValEx, genNameEx) + if (ctx.nonEmpty) { + oneOf(genValEx, genNameEx(ctx)) + } else { + genValEx + } } else { for { operNo <- choose(0, builtInOpers.length - 1) @@ -211,12 +214,11 @@ trait IrGenerators { if (ctx.nonEmpty) { // a value, a name, // an application of a user-defined operator in the context, an application of a built-in operator - oneOf(genValEx, genNameEx, genOperApply(genTlaEx(builtInOpers))(ctx), + oneOf(genValEx, genNameEx(ctx), genOperApply(genTlaEx(builtInOpers))(ctx), genLetInEx(genTlaEx(builtInOpers))(ctx), const(OperEx(oper, args: _*).withTag(tt))) } else { // as above but no user-defined operators - oneOf(genValEx, genNameEx, genLetInEx(genTlaEx(builtInOpers))(ctx), - const(OperEx(oper, args: _*).withTag(tt))) + oneOf(genValEx, genLetInEx(genTlaEx(builtInOpers))(ctx), const(OperEx(oper, args: _*).withTag(tt))) } } yield result } @@ -232,7 +234,7 @@ trait IrGenerators { */ def genTlaOperDecl(exGen: UserContext => Gen[TlaEx])(ctx: UserContext): Gen[TlaOperDecl] = { for { - name <- identifier + name <- identifier suchThat (n => !ctx.contains(n)) body <- exGen(ctx) nparams <- choose(0, maxArgs) params <- listOfN(nparams, identifier) @@ -261,7 +263,7 @@ trait IrGenerators { */ def genTlaConstDecl(ctx: UserContext): Gen[TlaConstDecl] = { for { - name <- identifier suchThat (n => ctx.forall(d => d.name != n)) + name <- identifier suchThat (n => !ctx.contains(n)) tt <- genTypeTag } yield TlaConstDecl(name).withTag(tt) } @@ -274,7 +276,7 @@ trait IrGenerators { */ def genTlaVarDecl(ctx: UserContext): Gen[TlaVarDecl] = { for { - name <- identifier suchThat (n => ctx.forall(d => d.name != n)) + name <- identifier suchThat (n => !ctx.contains(n)) tt <- genTypeTag } yield TlaVarDecl(name).withTag(tt) } @@ -287,51 +289,64 @@ trait IrGenerators { */ def genTlaDecl(exGen: UserContext => Gen[TlaEx])(ctx: UserContext): Gen[TlaDecl] = { for { - name <- identifier - decl <- oneOf(const(TlaConstDecl(name)), const(TlaVarDecl(name)), genTlaAssumeDecl(exGen(ctx)), - genTlaOperDecl(exGen)(ctx)) + decl <- oneOf(genTlaConstDecl(ctx), genTlaVarDecl(ctx), genTlaAssumeDecl(exGen(ctx)), genTlaOperDecl(exGen)(ctx)) + } yield decl + } + + /** + * Generate a declaration of: a constant, an operator definition, an assumption. + * + * @param ctx a context of user declarations. + * @return a generator of constant declarations + */ + def genTlaDeclButNotVar(exGen: UserContext => Gen[TlaEx])(ctx: UserContext): Gen[TlaDecl] = { + for { + decl <- oneOf(genTlaConstDecl(ctx), genTlaAssumeDecl(exGen(ctx)), genTlaOperDecl(exGen)(ctx)) } yield decl } /** - * Generate a module + * Generate a module by providing an expression generator. * * @param exGen a generator of TLA expressions * @return a generator of modules */ def genTlaModule(exGen: UserContext => Gen[TlaEx]): Gen[TlaModule] = { + genTlaModuleWith(genTlaDecl(exGen)) + } + + /** + * Generate a module by providing the declaration generator and expression generator. + * + * @param declGen generator of TLA declarations + * @return a generator of modules + */ + def genTlaModuleWith(declGen: UserContext => Gen[TlaDecl]): Gen[TlaModule] = { for { name <- identifier - ndecls <- choose(1, maxDeclsPerModule) - decls <- listOfN(ndecls, genTlaDecl(exGen)(Seq.empty)) suchThat { lst => - val defs = lst.collect { case d: TlaOperDecl => d } - // find the names of the definitions inside the bodies of the global definitions - val internal = defs.foldLeft(Set.empty[String]) { (set, d) => - set ++ internalDefs(d.body) - } - // and the name of the global definitions - val global = defs.foldLeft(Set.empty[String]) { (set, d) => - set + d.name - } - global.intersect(internal).isEmpty - } - } yield new TlaModule(name, decls) + decls <- genTlaDeclList(declGen)(emptyContext) + } yield TlaModule(name, decls) } - // compute the set of names that are declared in an expression - private def internalDefs: TlaEx => Set[String] = { - case LetInEx(body, defs @ _*) => - defs.foldLeft(internalDefs(body)) { (names, d) => - names + d.name - } - - case OperEx(_, args @ _*) => - args.foldLeft(Set.empty[String]) { (names, arg) => - internalDefs(arg) ++ names + // generate a list of declarations and avoid duplicates in the operator names + private def genTlaDeclList(declGen: UserContext => Gen[TlaDecl])(ctx: UserContext): Gen[List[TlaDecl]] = { + sized { size => + if (size <= 1) { + for { + decl <- declGen(ctx) + } yield List(decl) + } else { + for { + head <- declGen(ctx) + operSig = UserOperSig(head.name, + head match { + case TlaOperDecl(_, params, _) => params.length + case _ => 0 + }) + tail <- resize(size - 1, genTlaDeclList(declGen)(ctx + (head.name -> operSig))) + } yield head :: tail } - - case _ => - Set.empty[String] + } } // Given operator arity and an element generator, produce a list of arguments diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaDeclLevelFinder.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaDeclLevelFinder.scala new file mode 100644 index 0000000000..0ed953f61a --- /dev/null +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaDeclLevelFinder.scala @@ -0,0 +1,128 @@ +package at.forsyte.apalache.tla.lir + +import at.forsyte.apalache.tla.lir.oper.TlaOper +import org.junit.runner.RunWith +import org.scalacheck.Prop +import org.scalacheck.Prop.{AnyOperators, all, forAll, passed} +import org.scalatest.FunSuite +import org.scalatest.junit.JUnitRunner +import org.scalatest.prop.Checkers + +/** + * Tests of TlaDeclLevelFinder. + */ +@RunWith(classOf[JUnitRunner]) +class TestTlaDeclLevelFinder extends FunSuite with Checkers { + + test("non-action operators + constants = constant level") { + val gens = new IrGenerators { + override val maxArgs: Int = 3 + } + // all names are considered constants + val operators = gens.simpleOperators ++ gens.setOperators ++ gens.logicOperators ++ gens.arithOperators + val genDecl = gens.genTlaDeclButNotVar(gens.genTlaEx(operators))(_) + val prop = forAll(gens.genTlaModuleWith(genDecl)) { module => + val finder = new TlaDeclLevelFinder(module) + + all(module.operDeclarations map { + finder(_) =? TlaLevelConst + }: _*) && + all(module.constDeclarations map { + finder(_) =? TlaLevelConst + }: _*) + } + check(prop, minSuccessful(500), sizeRange(4)) + } + + test("non-action operators + variables = state level") { + val gens = new IrGenerators { + override val maxArgs: Int = 3 + } + // all names are considered constants + val operators = gens.simpleOperators ++ gens.setOperators ++ gens.logicOperators ++ gens.arithOperators + + val prop = forAll(gens.genTlaModule(gens.genTlaEx(operators))) { module => + val finder = new TlaDeclLevelFinder(module) + val vars = module.varDeclarations.map(_.name).toSet + + def expectedLevel(decl: TlaOperDecl): Prop = { + val level = finder(decl) + // it's hard to figure whether a declaration should be constant-level or state-level, + // because operators may call one another + s"operator ${decl.name}" |: + (level =? TlaLevelState || level =? TlaLevelConst) + } + + all(module.operDeclarations map expectedLevel: _*) && + all(module.constDeclarations map { + finder(_) =? TlaLevelConst + }: _*) && + all(module.varDeclarations map { + finder(_) =? TlaLevelState + }: _*) + } + check(prop, minSuccessful(1000), sizeRange(6)) + } + + test("action operators + variables = action level") { + val gens = new IrGenerators { + override val maxArgs: Int = 3 + } + // all names are considered constants + val operators = gens.actionOperators + val prop = forAll(gens.genTlaModule(gens.genTlaEx(operators))) { module => + val finder = new TlaDeclLevelFinder(module) + + def expectedLevel(decl: TlaOperDecl): Prop = { + val level = finder(decl) + // it's hard to figure the exact level of a declaration, + // because operators may call one another + s"operator ${decl.name}" |: + (level =? TlaLevelState || level =? TlaLevelConst || level =? TlaLevelAction) + } + + all(module.operDeclarations map expectedLevel: _*) && + all(module.constDeclarations map { + finder(_) =? TlaLevelConst + }: _*) && + all(module.varDeclarations map { + finder(_) =? TlaLevelState + }: _*) + } + + check(prop, minSuccessful(1000), sizeRange(6)) + } + + test("temporal operators + variables = temporal level") { + val gens = new IrGenerators { + override val maxArgs: Int = 3 + override val maxDeclsPerModule: Int = 4 + } + // all names are considered constants + val operators = gens.temporalOperators + val genEx = gens.genTlaEx(operators)(_) + val prop = forAll(gens.genTlaModuleWith(gens.genTlaOperDecl(genEx))) { module => + val finder = new TlaDeclLevelFinder(module) + + def expectedLevel(decl: TlaOperDecl): Prop = { + val level = finder(decl) + decl.body match { + case OperEx(TlaOper.apply, _*) => + // this operator immediately applies another operator that may have a constant level + passed + + case OperEx(_, _*) => + s"operator ${decl.name}" |: + level =? TlaLevelTemporal + + case _ => + passed + } + } + + all(module.operDeclarations map expectedLevel: _*) + } + + check(prop, minSuccessful(2000), sizeRange(5)) + } +} diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaLevelFinder.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaExLevelFinder.scala similarity index 79% rename from tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaLevelFinder.scala rename to tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaExLevelFinder.scala index 2df1758a18..5aca7a7e9f 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaLevelFinder.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTlaExLevelFinder.scala @@ -10,16 +10,16 @@ import org.scalatest.prop.Checkers * Tests of TlaLevelFinder. */ @RunWith(classOf[JUnitRunner]) -class TestTlaLevelFinder extends FunSuite with Checkers { +class TestTlaExLevelFinder extends FunSuite with Checkers { test("non-action operators + constants = constant level") { val gens = new IrGenerators { override val maxArgs: Int = 3 } // all names are considered constants - val finder = new TlaLevelFinder({ _ => TlaLevelConst }) + val finder = new TlaExLevelFinder({ _ => TlaLevelConst }) val operators = gens.simpleOperators ++ gens.setOperators ++ gens.logicOperators ++ gens.arithOperators - val prop = forAll(gens.genTlaEx(operators)(Seq())) { ex => + val prop = forAll(gens.genTlaEx(operators)(gens.emptyContext)) { ex => finder(ex) =? TlaLevelConst } check(prop, minSuccessful(2500), sizeRange(8)) @@ -31,8 +31,8 @@ class TestTlaLevelFinder extends FunSuite with Checkers { } // all names are considered constants val operators = gens.simpleOperators ++ gens.setOperators ++ gens.logicOperators ++ gens.arithOperators - val prop = forAll(gens.genTlaEx(operators)(Seq())) { ex => - val finder = new TlaLevelFinder(_ => TlaLevelState) + val prop = forAll(gens.genTlaEx(operators)(gens.emptyContext)) { ex => + val finder = new TlaExLevelFinder(_ => TlaLevelState) val level = finder(ex) if (containsName(ex)) { level =? TlaLevelState @@ -49,8 +49,8 @@ class TestTlaLevelFinder extends FunSuite with Checkers { } // all names are considered constants val operators = gens.actionOperators - val prop = forAll(gens.genTlaEx(operators)(Seq())) { ex => - val finder = new TlaLevelFinder(_ => TlaLevelState) + val prop = forAll(gens.genTlaEx(operators)(gens.emptyContext)) { ex => + val finder = new TlaExLevelFinder(_ => TlaLevelState) val level = finder(ex) ex match { case OperEx(_, _*) => @@ -69,8 +69,8 @@ class TestTlaLevelFinder extends FunSuite with Checkers { } // all names are considered constants val operators = gens.temporalOperators - val prop = forAll(gens.genTlaEx(operators)(Seq())) { ex => - val finder = new TlaLevelFinder(_ => TlaLevelState) + val prop = forAll(gens.genTlaEx(operators)(gens.emptyContext)) { ex => + val finder = new TlaExLevelFinder(_ => TlaLevelState) val level = finder(ex) ex match { case OperEx(_, _*) => diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestPrimePropagation.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestPrimePropagation.scala index a0e8784ef0..8c73ed360b 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestPrimePropagation.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestPrimePropagation.scala @@ -97,8 +97,9 @@ class TestPrimePropagation extends FunSuite with BeforeAndAfter with Checkers { } val prop = { - forAll(gens.genTlaEx(gens.simpleOperators ++ gens.arithOperators :+ TlaActionOper.prime)(Seq())) { ex => - onlyNamesArePrimed(transformer(ex)) + forAll(gens.genTlaEx(gens.simpleOperators ++ gens.arithOperators :+ TlaActionOper.prime)(gens.emptyContext)) { + ex => + onlyNamesArePrimed(transformer(ex)) } } From ed6ded1d411c400be1c6800182279982207d0c3e Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 6 May 2021 14:35:59 +0200 Subject: [PATCH 3/7] remove tla-script from this branch --- pom.xml | 2 -- 1 file changed, 2 deletions(-) diff --git a/pom.xml b/pom.xml index f97ce90a3e..dfefc8d97d 100644 --- a/pom.xml +++ b/pom.xml @@ -43,8 +43,6 @@ tla-assignments tla-bmcmt - - tla-script mod-tool From c14b8287506ed8e71312e9d540b51d6f78bf4b5c Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 6 May 2021 18:40:19 +0200 Subject: [PATCH 4/7] entry in unreleased --- UNRELEASED.md | 1 + 1 file changed, 1 insertion(+) diff --git a/UNRELEASED.md b/UNRELEASED.md index 5ffc9c8ee2..959f7ffc16 100644 --- a/UNRELEASED.md +++ b/UNRELEASED.md @@ -14,6 +14,7 @@ * Docker: Use openjdk-16 for the runtime in the app image, see #807 * Documentation: Introduce TypeAlises operator convention, see #808 +* tlair: TlaExLevelFinder and TlaDeclLevelFinder to compute TLA+ levels, see #811 ### Bug fixes From c57de8adcd6766acea58ae22bf0872de6b0662f3 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 6 May 2021 19:59:46 +0200 Subject: [PATCH 5/7] introduced a map of levels --- .../apalache/tla/lir/TlaExLevelFinder.scala | 36 +++++++++++-------- 1 file changed, 22 insertions(+), 14 deletions(-) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaExLevelFinder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaExLevelFinder.scala index 69e3af0c19..c12885159a 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaExLevelFinder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaExLevelFinder.scala @@ -15,20 +15,9 @@ class TlaExLevelFinder(nameLevel: String => TlaLevel) { case NameEx(name) => nameLevel(name) - case OperEx(op, args @ _*) - if op == TlaActionOper.prime || op == TlaActionOper.enabled - || op == TlaActionOper.unchanged || op == TlaActionOper.stutter - || op == TlaActionOper.nostutter || op == TlaActionOper.composition => - TlaLevelAction.join(args.map(find)) - - case OperEx(op, args @ _*) - if op == TlaTempOper.box || op == TlaTempOper.diamond || op == TlaTempOper.leadsTo - || op == TlaTempOper.weakFairness || op == TlaTempOper.strongFairness - || op == TlaTempOper.guarantees || op == TlaTempOper.AA || op == TlaTempOper.EE => - TlaLevelTemporal.join(args.map(find)) - - case OperEx(_, args @ _*) => - TlaLevelConst.join(args.map(find)) + case OperEx(op, args @ _*) => + val level = TlaExLevelFinder.levelOfOper.getOrElse(op, TlaLevelConst) + level.join(args.map(find)) case LetInEx(body, defs @ _*) => find(body).join(defs.map(d => find(d.body))) @@ -37,3 +26,22 @@ class TlaExLevelFinder(nameLevel: String => TlaLevel) { TlaLevelConst } } + +object TlaExLevelFinder { + private val levelOfOper = Map( + TlaActionOper.prime -> TlaLevelAction, + TlaActionOper.enabled -> TlaLevelAction, + TlaActionOper.unchanged -> TlaLevelAction, + TlaActionOper.stutter -> TlaLevelAction, + TlaActionOper.nostutter -> TlaLevelAction, + TlaActionOper.composition -> TlaLevelAction, + TlaTempOper.box -> TlaLevelTemporal, + TlaTempOper.diamond -> TlaLevelTemporal, + TlaTempOper.leadsTo -> TlaLevelTemporal, + TlaTempOper.weakFairness -> TlaLevelTemporal, + TlaTempOper.strongFairness -> TlaLevelTemporal, + TlaTempOper.guarantees -> TlaLevelTemporal, + TlaTempOper.AA -> TlaLevelTemporal, + TlaTempOper.EE -> TlaLevelTemporal + ) +} From a0014106f85d530222fa0deb285992d4e64b4405 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 6 May 2021 20:05:01 +0200 Subject: [PATCH 6/7] more logical cache lookup --- .../forsyte/apalache/tla/lir/TlaDeclLevelFinder.scala | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDeclLevelFinder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDeclLevelFinder.scala index 1321861565..905ee7dfc3 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDeclLevelFinder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaDeclLevelFinder.scala @@ -32,7 +32,7 @@ class TlaDeclLevelFinder(module: TlaModule) { } } - private def cacheLevel(callers: Set[String], name: String): Unit = { + private def cacheLevel(callers: Set[String], name: String): TlaLevel = { def levelOfName(name: String): TlaLevel = { if (consts.contains(name)) { TlaLevelConst @@ -41,8 +41,11 @@ class TlaDeclLevelFinder(module: TlaModule) { } else { if (!callers.contains(name) && defs.contains(name)) { // as the module comes from the parser, we assume that defs contains a definition for the name `name` - cacheLevel(callers + name, name) - levelCacheMap(name) + levelCacheMap.get(name) match { + case Some(level) => level + + case None => cacheLevel(callers + name, name) + } } else { TlaLevelConst } @@ -51,5 +54,6 @@ class TlaDeclLevelFinder(module: TlaModule) { val level = new TlaExLevelFinder(levelOfName)(defs(name).body) levelCacheMap += name -> level + level } } From 36faf8c5ebbc01c61c9091ed2651d0ae5deaf71c Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Thu, 6 May 2021 20:14:10 +0200 Subject: [PATCH 7/7] addressing comments by Shon --- .../at/forsyte/apalache/tla/lir/TlaLevel.scala | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaLevel.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaLevel.scala index 12cb1501e6..16e349cdf6 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaLevel.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaLevel.scala @@ -27,7 +27,7 @@ sealed trait TlaLevel extends Ordered[TlaLevel] { } /** - * Join the levels by computing the smallest level that covers both of `this` and `that`. + * Join the levels by computing the maximum of the levels of `this` and `that`. * * @param that the level to join with * @return the minimal level j that satisfies: `j <= this` and `j <= that`. @@ -37,7 +37,7 @@ sealed trait TlaLevel extends Ordered[TlaLevel] { } /** - * Join the level with a sequence of level + * Join the level with a sequence of level. * * @param otherLevels a sequence of levels * @return the join of `this` and otherLevels @@ -50,11 +50,12 @@ sealed trait TlaLevel extends Ordered[TlaLevel] { object TlaLevel { private val INT_TO_LEVEL = Seq(TlaLevelConst, TlaLevelState, TlaLevelAction, TlaLevelTemporal) - def fromInt(level: Int): TlaLevel = { - if (level < 0 || level >= INT_TO_LEVEL.length) { - throw new IllegalArgumentException(s"Unexpected level of TlaValue: $level") - } else { - INT_TO_LEVEL(level) + def fromInt(levelNo: Int): TlaLevel = { + INT_TO_LEVEL.find(_.level == levelNo) match { + case Some(level) => level + + case None => + throw new IllegalArgumentException(s"Unexpected level: $levelNo") } } }