Re: [tlaplus] Creating function sets lazily

[Igor Konnov <igor.konnov@xxxxxxxxx>]

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

> On 23.02.2022, at 08:18, Stephan Merz <stephan.merz@xxxxxxxxx> wrote:
> 
> 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
> 
>> On 23 Feb 2022, at 04:16, thomas...@xxxxxxxxx <thomasgebert@xxxxxxxxx> wrote:
>> 
>> 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.
>> 
>> -- 
>> 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+unsubscribe@xxxxxxxxxxxxxxxx.
>> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/aa184e59-2e0c-44d9-a2c3-ea631681edean%40googlegroups.com.
> 
> 
> -- 
> 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+unsubscribe@xxxxxxxxxxxxxxxx.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/B7126745-9C62-44D7-868E-D439C81331CD%40gmail.com.

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2EEDA290-8802-4F1C-AE87-3166265C5463%40gmail.com.