Creating function sets lazily

[thomas...@gmail.com]

I have the following code in my TLA+ spec:

BitString == [1..6 -> {0,1}]
AllowedStrings == {"a", "b", "c", "d", "e"}
IsInjective(f) == \A a,b \in DOMAIN f : f[a] = f[b] => a = b
hash == CHOOSE i \in [AllowedStrings -> BitString] : IsInjective(i)

I then run hash[2] in the evaluator.

This works as expected, but it takes an *extremely* long time to run, and if I increase my domain (e.g. adding "f" to AllowedStrings), it gives me an error:

Attempted to construct a set with too many elements (>100000000)

I understand the combinatorial complexity makes these giant sets, but I was wondering if there's a way to avoid generating all the sets once it gets something that satisfies CHOOSE.

[thomas...@gmail.com]

Sorry, I meant hash["b"].

[Stephan Merz]

BitString has 2^6 elements, and [AllowedString -> BitString] therefore has (2^6)^5 = 2^30 elements. TLC enumerates these sets, and then evaluates IsInjective for each one of them. One could try to speed this up, as you suggest, but CHOOSE should also satisfy the axiom of determinacy

S = T /\ (\A x \in S : P(x) <=> Q(x) => (CHOOSE x \in S : P(x)) = (CHOOSE x \in T : Q(x))

and evaluate to the same value even if the sets and predicates are presented differently. (TLC already doesn't fully guarantee this.)

As long as the CHOOSE operator only occurs in constant definitions as in this example, you may consider replacing hash by a constant parameter and write

CONSTANT hash

ASSUME hash \in [AllowedStrings -> BitString] /\ IsInjective(hash)

You'll have to provide a hash function in the model, but anyway TLC only checks the spec for one fixed hash function even with the definition. Evaluating the ASSUME clause should take negligible time.

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/aa184e59-2e0c-44d9-a2c3-ea631681edean%40googlegroups.com.

[Igor Konnov]

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.

[tlaplus-go...@lemmster.de]

Hi,

the definition of this hash function maps a universe of six elements to 2^6 bits. Unless this is intentional, you could, e.g., use the identity hash function [ s \in AllowedStrings |-> s ], which is also a perfect hash function. For readers, assume that hash is injective.

Anyway, to expand on Stephan's solution, below is a definition that TLC evaluates quickly. You can use it to define the CONSTANT hash or re-define the original operator hash:

EXTENDS Randomization, FiniteSets

[...]

SomeHash ==
\* Run TLC with the same -fp and -seed for RandomSubset to pick the same subset.
CHOOSE f \in [ AllowedStrings ->
RandomSubset( Cardinality(AllowedStrings), BitString ) ]:
IsInjective(f)


Markus