Refactor and improve tests for the builder library

[shonfeder]

The current tests use a lot of machinery around ScalaCheck that doesn't add any value afaict. On the contrary, it seem to make it considerably more difficult to read and understand the tests than it would be if we were using the usual PBT idioms advised by scalacheck. It is also difficult to know what has gone wrong when the tests fail, since the tests are doing too many things in each case and have undescriptive names.

Here is an example of a test case in the current approach:

apalache/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestBaseBuilder.scala

Lines 109 to 159 in 325f21c

	test("choose3") {
	type T = (TBuilderInstruction, TBuilderInstruction, TBuilderInstruction)
	def mkWellTyped(tt: TlaType1): T =
	(
	builder.name("x", tt),
	builder.name("set", SetT1(tt)),
	builder.name("p", BoolT1),
	)
	def mkIllTyped(tt: TlaType1): Seq[T] =
	Seq(
	(
	builder.name("x", InvalidTypeMethods.differentFrom(tt)),
	builder.name("set", SetT1(tt)),
	builder.name("p", BoolT1),
	),
	(
	builder.name("x", tt),
	builder.name("set", SetT1(InvalidTypeMethods.differentFrom(tt))),
	builder.name("p", BoolT1),
	),
	(
	builder.name("x", tt),
	builder.name("set", InvalidTypeMethods.notSet),
	builder.name("p", BoolT1),
	),
	(
	builder.name("x", tt),
	builder.name("set", SetT1(tt)),
	builder.name("p", InvalidTypeMethods.notBool),
	),
	)
	def resultIsExpected = expectEqTyped[TlaType1, T](
	TlaOper.chooseBounded,
	mkWellTyped,
	ToSeq.ternary,
	tt => tt,
	)
	checkRun(Generators.singleTypeGen)(
	runTernary(
	builder.choose,
	mkWellTyped,
	mkIllTyped,
	resultIsExpected,
	)
	)
	assertThrowsBoundVarIntroductionTernary(builder.choose)
	}

Here are two cases in the approach I propose as an improvement:

apalache/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestBaseBuilder.scala

Lines 126 to 154 in de453fe

	test("building `CHOOSE x \\in S: p` RESPECTS and ENSURES type correctness") {
	import org.scalacheck.Prop._
	// The generator for TlaType1 provided by ArbTBuilderInstruction
	// will only generate concrete supported types
	import pbt.ArbTBuilderInstruction._
	val prop = forAll { (nameType: TlaType1, elemType: TlaType1) =>
	// Build an expression of the form
	// CHOOSE x \in set: p
	val x = builder.name("x", nameType)
	val set = builder.name("S", SetT1(elemType))
	val p = builder.name("p", BoolT1)
	val instruction = builder.choose(x, set, p)
	// We RESPECT type correctness if we succeed whenever the type of `x` is the same as the type of elements in `S`
	val wellTypedChooseSucceeds = (nameType == elemType) ==> succeeds(instruction)
	// We ENSURE type correctness if we raise a type exception whenever the types conflict
	val illTypedChooseFails = (nameType != elemType) ==> throwsTBuilderTypeException(instruction)
	(wellTypedChooseSucceeds || illTypedChooseFails)
	}
	check(prop, sizeRange(4))
	}
	test("""building CHOOSE "x" \\in S: TRUE raises an IllegalArgumentException""") {
	// Since "CHOOSE" requires a name
	assertThrowsBoundVarIntroductionTernary(builder.choose)
	}

Benefits of my proposed approach:

• Less than half the length (and that's after the addition of clarifying comments and imports that wouldn't be included in the actual code)
• Better coverage, since we test for arbitrary invalid types
• More readable expression of the property being tested for
• Clearer naming of the test cases, so it is clear what test case or property is failing

[Kukovec]

I'd like to see others weigh in on this too, but the tests you have proposed are not equivalent.

• The following case is never addressed:

         ( 
             builder.name("x", tt), 
             builder.name("set", SetT1(tt)), 
             builder.name("p", InvalidTypeMethods.notBool), 
         ) 

• (nameType != elemType) ==> throwsTBuilderTypeException(instruction) does not perform the same function as

( 
             builder.name("x", InvalidTypeMethods.differentFrom(tt)), 
             builder.name("set", SetT1(tt)), 
             builder.name("p", BoolT1), 
         ), 
         ( 
             builder.name("x", tt), 
             builder.name("set", SetT1(InvalidTypeMethods.differentFrom(tt))), 
             builder.name("p", BoolT1), 
         ), 
         ( 
             builder.name("x", tt), 
             builder.name("set", InvalidTypeMethods.notSet), 
             builder.name("p", BoolT1), 
         ), 

The more verbose collection above is a decomposition of the equivalence classes of builder failure. They are all instances of nameType != elemType, and every instance of nameType != elemType falls into one of the above buckets, however, unlike the probabilistic approach, they guarantee that all of these varied failure scenarios get tested with 100% probability. Also, typically each of these sub-cases corresponds to a different way in which e.g. the signature implementation could be wrong.

• succeeds(instruction) only checks whether a type failure was raised during execution (IIRC). It notably does nothing to check that the expression constructed has the correct syntax for the given operator. For instance, if builder.forall actually constructed a TlaOper(TlaBoolOper.exists, ...) expression, which has the exact same type signature, the new tests would fail to detect this bug in any way.

Ultimately, by my assessment:

Less than half the length (and that's after the addition of clarifying comments and imports that wouldn't be included in the actual code)

Yes, because it skips structure checking, and because it collapses all failure scenarios into one, which I'm not sure you can even do for all operators.

Better coverage, since we test for arbitrary invalid types

Untrue, since the mkIllTyped tests are just a decomposition of (nameType != elemType) (for the example above), and Generators.singleTypeGen generates arbitrary types.

More readable expression of the property being tested for
Clearer naming of the test cases, so it is clear what test case or property is failing

Subjective, but I'm not opposed to more verbose test names, or splintering away IllegalArgumentException tests.