Hi,
This looks like an interesting example for Apalache.
Stephan, your suggestion regarding hash as a constant works nicely. Here is a minimal working example:
--------------- MODULE TestHash2 --------------
\* Check the invariant for all combinations of hashes
\*
\* apalache-mc check --cinit=ConstInit --inv=Inv TestHash2.tla
EXTENDS Integers
BitString == [1..6 -> {0,1}]
AllowedStrings == {"a", "b", "c", "d", "e"}
\* @type: (a -> b) => Bool;
IsInjective(f) ==
\A a,b \in DOMAIN f : f[a] = f[b] => a = b
CONSTANT
\* @type: Str -> (Int -> Int);
hash
\* this assumption is redundant when using ConstInit
\* ASSUME hash \in [AllowedStrings -> BitString] /\ IsInjective(hash)
ConstInit ==
hash \in [AllowedStrings -> BitString] /\ IsInjective(hash)
Init == TRUE
Next == TRUE
Inv == \A x, y \in AllowedStrings:
x /= y => hash[x] /= hash[y]
==============================================
Best regards,
Igor
> To view this discussion on the web visit
https://groups.google.com/d/msgid/tlaplus/B7126745-9C62-44D7-868E-D439C81331CD%40gmail.com.