fix: Set/ValueVec support searching distinct typed elements

[lalo]

• relax equals() - returns false instead of throwing (we can revert case by case)
• add more advanced tests - nested sets
• keep happy path for set of same typed elements
• types are order based on their "ValueImage"/Kind int

See diff of tlatools/org.lamport.tlatools/test/tlc2/REPLTest.java for more info.

[lalo]

this fixes un-normalized sets being classified as normalized, issue in latest main

[lemmy]

@lalo We appreciate your efforts and willingness to contribute. :-) Note though that we are generally very, very careful when it comes to changing the core of TLC. Without judging the quality of this PR (I haven't looked at it), please don't be discouraged should we decide that the proposed changes are too risky to be accepted. Real-world specs tend to be "well-typed".

[lalo]

I understand. It would be nice to see a spec that gets broken with this change, or have the full CI run to see how much damage this change is making. I've only ran the REPLtest and played around with the REPL.

[lemmy]

Tests only ever confirm the presence of bugs, but you can run the TLC test suite with: ant -f tlatools/org.lamport.tlatools/customBuild.xml -Dtest.halt=true compile compile-test test.

[lalo]

tlaplus/tlatools/org.lamport.tlatools/test/tlc2/debug/EWD840ErrorActionDebuggerTest.java

Line 74 in 3ad453f

assertEquals("Attempted to check equality of integer 0 with non-integer:\n\"abc\"", expVar[0].getValue());

This would return false now instead of raising exception.

[lemmy]

The goal of this assertion is to test that the debugger raises an error on silly expressions. Thus, you could simply replace this particular expression with another silly expression.