Refactor and improve tests for the builder library about apalache HOT 1 OPEN

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.

from apalache.