# Re: [tlaplus] Creating function sets lazily

• From: Igor Konnov <igor.konnov@xxxxxxxxx>
• Date: Wed, 23 Feb 2022 09:19:55 +0100
• Cc: Igor Konnov <igor.konnov@xxxxxxxxx>
• Ironport-data: A9a23:rnc3xKqcMOzJ/UJw6ZMYYBc5nW1eBmKOYBIvgKrLsJaIsI4StFCzt garIBmBbvrYZ2f3ft1xat+w90JQ6pbSyYdmSgZpqXo3EH8bpePIVI+TRqvSF3PLf5ebFCqLz O1HN4KedJhsJpP4jk3wWlQ0hSAkjclkfpKlVKicfHkZqTZMEE/Nszo68wICqtMu0YjR7z+l4 4uo+ZWFYgT9glaYD0pNg069gEM31BjNkGhA1rAOTagjUIj2yhH5pLpGTU2AByOQrrt8RoZWd M6fpF2NxV41yj92Yj+TfhkXRWVRKlLaFVDmZnO7wMFOiDAazsA5+v5T2Pbx9S67hh3R9+2dx umhurSODlp2Yaf3pd0/cAFSEXt7I6sbqJPYdC3XXcy7lyUqclPpyvRqSUU4ZMgWp7kxDmZJ+ vgVbjsKa3hvhcrsmOP9GrQq35p8apS0VG8ckikIITXxEfIvWZTeWObA49Ry9wlsoPtxMKv3Q eAzTWQzNkrhSjhgA3orJ6MBuNiJrnb4dDJcpV2Porcv+C7YywkZPL3FaoCKJYzRFJ49ckCwr Uj7/37+LDcjFZ+t4DWuwy70nfPTpHauMG4VPOTgqqQCbEeo7mASExYLTkCTvf2wzEulQZdeL VYV82wvq7Iz/QqlVLHAswaQpXeFulsYVYMVHbBlrg6KzaXQ7kCSAW1soiN9hMIOiohrGmMg7 WKwvfDxDz41taOTFCKx6eLBxd+tAhQ9IWgHbC4CaAIK5dj/vY0+5i4jqP4zQMZZafWlSVnNL yC2QDsW3OpM0JZav0mv1RWW3GL2/8mhohsdv12PBgqYAhVFiJlJjrFEBHDe5PdEaYKXFxyP4 SdClM+Z4+QDS5qKkURhodnh/pn2vJ5p0xWG2jaD+qXNERzxphZPmqgNuVlDyL9BaJpsRNMQS Ba7VfltzJFSJmC2SqR8fpi8Dc8npYC5S4i4C62IMIIWM8QoHONiwM2ITR7At4wKuBh8+ZzTx b/GGSpRJSpAUP8/lWLeqxk1iOd7mn5WKZzvqWDTlkz7i9JylVaaTrAKNFbmUwzKxPLsnekhy P4Gb5Hi40wHDoXWO3CHmaZOcw1iBSVlVPje9pwGHsbec1YOMDxwW5f5n+h7E6Q7xPs9qws91 iDVtrlwlQKn3RUq6GyiMRheVV8Ydcwh9SliZXR0Zz5FGRELOO6S0UvWTLNvFZFPyQCp5aQco yAtd5rSD/JRZC7A/jhBP5DxoJY7KkakggWBOyeqej8iZ4UmTAvMo4e2cgzq/SgILyy2qcpv8 +b7j1iEH8UOF1Z4EcLbSPOz1Fft73ITr+R/AhnTKd5JdUSwrYVncnSjjvI+L8wWBw/Ewz+Wi 1SfDRsC9LvCpoY09J/CgqXd99WlFO53H0x7GWjH7ObuZXOKoDb7mYIZCbSGZzHQUm/w6Z6OX +QNwqGuKuADkXZLr5F4TORmwKc40N3l+O1XwwFiK3PUNgj5B75lJE6G6slBrKh6wLFU5FmtU UWV99gGYLiENZq+Ql4cLQYodN6OzfUFhj7W4ahnKUn2/nYprrWAVkpWMhaWjzFFN/1+N4Z8m bUtv8sf6gqejBs2M4fW1XsNrDvScXFQAb86spw6AZPwjlZ5wF91Z5GBWDT954uCaokRP0Qnf m2Uia7Fi+gOz0bOaSBoR33E3O4YgZpX/R4XkxkNIFOGnteDjfgyhUUD/TMyRwVT7xNGz+MjZ TQxZhMtff2Dr2VymcxOf2GwAAUdVheXzUr8lgkSn2rDQkj0C2HAfT85OP2RwUYC7mhYcmQJ9 b2U0ji1AzPjfcXt2Xk9Xklqr/HsV9ts7haHncmhFsuIXMJlMWu53/H+OjNR9Vj6B9gsjlbMv +hg8c5/bqr0MSMfuaomE5Lc3rMVEUjWKGtHSPBn3aUIAWCNKGrpgGPRdR+8KpFXOvjH0U6kE MgydMhBYBKziXSVpTcBCK9QfrJ5kKJ77dYOYO+6d24ar6OE/H0uv4jX6zDlwmAsRNpqnIA2L YaWeCiFD3TXmX9dg2vQt45fJ2CjasMFbgDx0bzn6ukPDJ5f4uhgfVtoiemxtnSRdQ9pplea4 VyFaKjRwOhvj49rmtK0QKlEAgy1L/L1VfiJoF/v6YUQNYuXPJecrR4Rp3nmIx9SYekbVeNxm Onfq9Xwxk7E4Os7Xm2xd0NtzEWVCRhenda7M/4b6FFflCqGHcviul4Npj/+JptOn9dQoMKgQ mNUrSd2mcE9A79gKL99MkCy0Crxz4z4aaDvoS6ytfOREgNb2gvCRD9i3WG8dnlVL0fkJLWnY jIZeJ+SChRwo4NLCxsJCOthHodjZlTkXMPKsjE3WSawVgGVv79JhlcuedfMJ90G5rlo3fsWO a74eyU=
• Ironport-hdrordr: A9a23:84FR/qECkxY5F7W5pLqEj8eALOsnbusQ8zAXPidKJiC9E/b0qy nApoV56faZslcssRIb9exoWpPwI080nKQdieJ6AV7IZmfbUQWTTL1f0Q==
• Ironport-sdr: TtGCgjNwBsyF9m5hiR6JiIr0Qd1SwqYyn2q3p3QXzrAkF3TiLuZkhRvmgAWZ3OnRPiR7LRl7HX IGA2es/DJzfqGXVwmFq2sR0OK7GYXe2kyjdeHq0xR/XYukN90DwkkKlyofxT2iKhF0Ff2/wwP2 Dpf05fY42+usOJrwtDsFxaPo44XBwqbnfdjMqlp+3vUdA7fPW42ST4zcSQZXtTr8F8dhjjuxI+ ceJabUSSVM0oCCklb51V2TprsFmIWRFyl0ddy8BqZMTL3GvrZDRlLpvaYza5VA8k15cUCAwwzU HO5gZ3+LnzQ5zOddi/GN9hiL

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.