From 90c20d308badc952dd36d28ce2e2b37e4703b65f Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Wed, 27 Apr 2022 16:28:18 +0200 Subject: [PATCH 1/4] Add shrinkers for PBT-generated TlaType1 and TlaEx --- .../tla/bmcmt/CrossTestEncodings.scala | 57 +++++++++++++++++-- 1 file changed, 51 insertions(+), 6 deletions(-) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala index bf145a0179..b1d6656d55 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala @@ -7,18 +7,21 @@ import at.forsyte.apalache.tla.bmcmt.trex.{IncrementalExecutionContext, Transiti import at.forsyte.apalache.tla.lir.TypedPredefs._ import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.convenience.tla -import at.forsyte.apalache.tla.lir.oper.{TlaFunOper, TlaOper} +import at.forsyte.apalache.tla.lir.oper.{TlaFunOper, TlaOper, TlaSetOper} import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker import at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming import ch.qos.logback.classic.{Level, Logger} import org.scalacheck.Arbitrary.arbitrary import org.scalacheck.Gen import org.scalacheck.Gen.{const, listOf, lzy, nonEmptyListOf, oneOf, sized} -import org.scalacheck.Prop.{forAll, AnyOperators} +import org.scalacheck.Prop.{forAllShrink, AnyOperators} +import org.scalacheck.Shrink.shrink import org.scalatest.funsuite.AnyFunSuite import org.scalatestplus.scalacheck.Checkers import org.slf4j.LoggerFactory +import scala.annotation.nowarn + /** * Test encodings against each other. Override [[AnyFunSuite.withFixture]] to set up SMT encodings used for oracle and * verifier. @@ -98,6 +101,7 @@ trait CrossTestEncodings extends AnyFunSuite with Checkers { oneOf(genPrimitive, genSet, genSeq, genFun, /*genOper,*/ genTup, genRec /*, genRowRec, genVariant, genRow*/ ) } } + // Override to avoid reals, constants, and typevar-typed expressions. override def genPrimitive: Gen[TlaType1] = oneOf(const(BoolT1()), const(IntT1()), const(StrT1()) /*, const(RealT1()), genConst, genVar*/ ) @@ -171,7 +175,7 @@ trait CrossTestEncodings extends AnyFunSuite with Checkers { // check the outcome val outcome = checker.run() assert(Error(1) == outcome, - if (moduleName == "Verifier") s"If outcome=Deadlock, this probably indicates a problem with one encoding." + if (moduleName == "Verifier") "If outcome=Deadlock, this probably indicates a problem with one encoding." else "") // extract witness expression from the counterexample @@ -271,6 +275,7 @@ trait CrossTestEncodings extends AnyFunSuite with Checkers { /** * Generate TLA+ expressions of a given [[TlaType1]]. + * * @param witnessType * [[TlaType1]] of the expression to generate. * @return @@ -311,6 +316,7 @@ trait CrossTestEncodings extends AnyFunSuite with Checkers { /** * Generate TLA+ expressions of type `Set(witnessType)`. + * * @param witnessType * Element [[TlaType1]] of the set expression to generate. * @return @@ -335,15 +341,54 @@ trait CrossTestEncodings extends AnyFunSuite with Checkers { } } - // Ignore this test until the bug described in https://github.com/informalsystems/apalache/issues/1660 is fixed. + @nowarn("cat=deprecation&msg=Stream") // ScalaCheck's Shrink still uses Stream, which is deprecated since Scala 2.13.0 + private def shrinkType(tp: TlaType1): Stream[TlaType1] = tp match { + case IntT1() | RealT1() | BoolT1() | StrT1() => Stream.empty + case FunT1(arg, res) => Stream(arg, res) + case SetT1(elem) => Stream(elem) + case SeqT1(elem) => Stream(elem) + case TupT1(elems @ _*) => + Stream.concat( + // shrink to one of the element types + Stream(elems: _*), + // recursively shrink one tuple element type + elems.zipWithIndex.foldLeft(Stream.empty[TlaType1]) { case (acc, (tp, idx)) => + acc ++ shrink(tp).map(shrunkType => TupT1(elems.updated(idx, shrunkType): _*)) + }, + // tuples over a subset of the current element types + Stream(shrink(elems).filterNot(_.isEmpty).map(elems => TupT1(elems: _*)): _*), + ) + case RecT1(fieldTypes) => + Stream.concat( + // shrink to one of the field types + Stream(fieldTypes.values.toSeq: _*), + // recursively shrink one record field type + fieldTypes.foldLeft(Stream.empty[TlaType1]) { case (acc, (fieldName, tp)) => + acc ++ shrink(tp).map(shrunkType => RecT1(fieldTypes.updated(fieldName, shrunkType))) + }, + // tuples over a subset of the current field types + Stream(shrink(fieldTypes).filterNot(_.isEmpty).map(elems => RecT1(elems)): _*), + ) + case ConstT1(_) | OperT1(_, _) | RealT1() | RecRowT1(_) | RowT1(_, _) | SparseTupT1(_) | VarT1(_) | VariantT1(_) => + throw new IllegalArgumentException(s"Shrinking unsupported type ${tp}. Should be disabled in type generator.") + } + + @nowarn("cat=deprecation&msg=Stream") // ScalaCheck's Shrink still uses Stream, which is deprecated since Scala 2.13.0 + private def shrinkEx(ex: TlaEx): Stream[TlaEx] = ex match { + case OperEx(TlaSetOper.enumSet, args @ _*) => + Stream(shrink(args).filterNot(_.isEmpty).map(elems => tla.enumSet(elems: _*).as(ex.typeTag.asTlaType1())): _*) + case _ => Stream.empty + } + // TODO(#1668): Regularly run the encodings comparison. + // Ignore this test until all bugs are fixed. ignore("encodings are consistent") { // TODO(#1666): Loggers in SeqModelChecker produce a lot of output; divert logger output. // Disable logger output as long as this test is `ignore`. LoggerFactory.getLogger(org.slf4j.Logger.ROOT_LOGGER_NAME).asInstanceOf[Logger].setLevel(Level.OFF) - val prop = forAll(typeGen.genType1 :| "witness type") { witnessType => - forAll(genWitnessSet(witnessType) :| "witnesses set") { witnesses => + val prop = forAllShrink(typeGen.genType1 :| "witness type", shrinkType) { witnessType => + forAllShrink(genWitnessSet(witnessType) :| "witnesses set", shrinkEx) { witnesses => // Uncomment for debugging: // println(s"Looking for witness of type ${witnessType} in set ${witnesses}") val witness = getWitness(witnessType, witnesses) From 7ce74cbbc1681590cac5026df15ed79c5bfabdf0 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Fri, 20 May 2022 09:31:49 +0200 Subject: [PATCH 2/4] Apply suggestions from code review Co-authored-by: Shon Feder --- .../at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala index b1d6656d55..1927cc2c07 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala @@ -310,7 +310,8 @@ trait CrossTestEncodings extends AnyFunSuite with Checkers { } yield tla.funDef(res, name, set).as(tp) case ConstT1(_) | OperT1(_, _) | RealT1() | RecRowT1(_) | RowT1(_, _) | SparseTupT1(_) | VarT1(_) | VariantT1(_) => - throw new IllegalArgumentException(s"Unsupported type ${witnessType}. Should be disabled in type generator.") + throw new IllegalArgumentException( + s"Unsupported type ${witnessType}. Should have been filtered by the override in the declaration of 'CrossTestEncodings.typeGen'.") } } @@ -351,7 +352,7 @@ trait CrossTestEncodings extends AnyFunSuite with Checkers { Stream.concat( // shrink to one of the element types Stream(elems: _*), - // recursively shrink one tuple element type + // tuples with a single element type shrunk, keeping the other types as-is elems.zipWithIndex.foldLeft(Stream.empty[TlaType1]) { case (acc, (tp, idx)) => acc ++ shrink(tp).map(shrunkType => TupT1(elems.updated(idx, shrunkType): _*)) }, @@ -366,7 +367,7 @@ trait CrossTestEncodings extends AnyFunSuite with Checkers { fieldTypes.foldLeft(Stream.empty[TlaType1]) { case (acc, (fieldName, tp)) => acc ++ shrink(tp).map(shrunkType => RecT1(fieldTypes.updated(fieldName, shrunkType))) }, - // tuples over a subset of the current field types + // records with a subset of the current field types Stream(shrink(fieldTypes).filterNot(_.isEmpty).map(elems => RecT1(elems)): _*), ) case ConstT1(_) | OperT1(_, _) | RealT1() | RecRowT1(_) | RowT1(_, _) | SparseTupT1(_) | VarT1(_) | VariantT1(_) => From a42bfcd82fff14791cc0d302aaa03762ff427746 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Mon, 23 May 2022 09:01:15 +0200 Subject: [PATCH 3/4] Add TODO comment to expr shrinker --- .../at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala index 1927cc2c07..824daef7cc 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala @@ -378,6 +378,8 @@ trait CrossTestEncodings extends AnyFunSuite with Checkers { private def shrinkEx(ex: TlaEx): Stream[TlaEx] = ex match { case OperEx(TlaSetOper.enumSet, args @ _*) => Stream(shrink(args).filterNot(_.isEmpty).map(elems => tla.enumSet(elems: _*).as(ex.typeTag.asTlaType1())): _*) + // TODO: Shrink further operators. For now, the main obstacle to interpreting the bugs uncovered by this class + // is that the expression generator produces sets of more elements than necessary. case _ => Stream.empty } From ac04bf2f6193c350148ef22491eca380f26d03a4 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Tue, 24 May 2022 19:06:56 +0200 Subject: [PATCH 4/4] Fix syntax after merge --- .../apalache/tla/bmcmt/CrossTestEncodings.scala | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala index b4e53da084..816e71b6d6 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala @@ -385,8 +385,8 @@ trait CrossTestEncodings extends AnyFunSuite with Checkers { set <- genWitnessSet(arg) res <- genWitness(res) } yield tla.funDef(res, name, set).as(tp) - case ConstT1(_) | OperT1(_, _) | RealT1() | RecRowT1(_) | RowT1(_, _) | SparseTupT1(_) | VarT1(_) | - VariantT1(_) => + // TODO(#401): Enable rows, variants when supported by the model checker. + case ConstT1(_) | OperT1(_, _) | RealT1 | RecRowT1(_) | RowT1(_, _) | SparseTupT1(_) | VarT1(_) | VariantT1(_) => throw new IllegalArgumentException( s"Unsupported type ${witnessType}. Should have been filtered by the override in the declaration of 'CrossTestEncodings.typeGen'.") } @@ -427,10 +427,10 @@ trait CrossTestEncodings extends AnyFunSuite with Checkers { @nowarn("cat=deprecation&msg=Stream") // ScalaCheck's Shrink still uses Stream, which is deprecated since Scala 2.13.0 private def shrinkType(tp: TlaType1): Stream[TlaType1] = tp match { - case IntT1() | RealT1() | BoolT1() | StrT1() => Stream.empty - case FunT1(arg, res) => Stream(arg, res) - case SetT1(elem) => Stream(elem) - case SeqT1(elem) => Stream(elem) + case IntT1 | RealT1 | BoolT1 | StrT1 => Stream.empty + case FunT1(arg, res) => Stream(arg, res) + case SetT1(elem) => Stream(elem) + case SeqT1(elem) => Stream(elem) case TupT1(elems @ _*) => Stream.concat( // shrink to one of the element types @@ -453,7 +453,8 @@ trait CrossTestEncodings extends AnyFunSuite with Checkers { // records with a subset of the current field types Stream(shrink(fieldTypes).filterNot(_.isEmpty).map(elems => RecT1(elems)): _*), ) - case ConstT1(_) | OperT1(_, _) | RealT1() | RecRowT1(_) | RowT1(_, _) | SparseTupT1(_) | VarT1(_) | VariantT1(_) => + // TODO(#401): Enable rows, variants when supported by the model checker. + case ConstT1(_) | OperT1(_, _) | RecRowT1(_) | RowT1(_, _) | SparseTupT1(_) | VarT1(_) | VariantT1(_) => throw new IllegalArgumentException(s"Shrinking unsupported type ${tp}. Should be disabled in type generator.") }