[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] CHOOSEing a function with a unique range for each element of the domain.
- From: tlaplus-google-group@xxxxxxxxxxx
- Date: Mon, 21 Feb 2022 20:21:57 -0800
- Ironport-data: A9a23:GdTBaazvq+/iwTkNPMB6t+fKwyrEfRIJ4+MujC+fZmUNrF6WrkVSz jQdUDiHP/+MYjP3KN5xaorn8x4E7JCEy9dqGQM+pFhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefQAOOU5NfsYkidfyc9IMsaoU8ly75RbrJA24DjWVvX4 4mq+qUzBXf8s9JKGjJMg068gEg31BjCkGtwUosWOJinFHeH/5UkJMp3yZOZdxMUcaEIdgKOf Nsv+Znilo/vE7jBPfv++lrzWhVirrc/pmFigFIOM0SpqkAqSiDfTs/XOdJEAXq7hQllkPhoz YRCpKegQz4AL63Sos8aDhAHDCNXaPguFL/veRBTsOSWxkzCNnbgmrBgUhhwMoof9eJ6R2pJ8 JT0KhhXNkHF17/wmurrDLc17iggBJGD0Ic3pnVp1TXEFrUsR5vpaIX43fBo8AcZr/pkRtH8P eU4QB9AVTn4XTQVBAs2IJ05m+isi3bldCBAsxSeoq9fD237klIpieS3abI5fPSvBupumne+l FnhvHbhCEgLDsOvyQO8pyfEaujnxHunAur+DoaQ+v9xi0CI3UQPDBRQUECh5Pi/kE+3HdNZM U0dvCQ0xZXe72SuR9j5GhC0+TuK4EdaVN1XHOk3rgqKz8I4/jp1GEAdS29Oeec2vvYfVDw07 HSOwtq2Gj5G5ej9pW2myp+Yqja7OC4wJGAEZDMZQQZt3zUFiNFj5v4oZoYzeJNZnuEZChmrn G/X9HlWa6E7yJ9Uh//irDgrlhr1/sCRJjPZ8Dk7SY5M0++UTIusZojt5FSCqPgedcCWSV6Ou HVCkM+bhAzvMX1vvHPVKAnuNOvxjxpgDNE6qQI0d3XG32jyk0NPhagKvFlDyL5Ba67ogwPBb k7Joh9275ROJnasZqIfS9vvV5l2k/i6TYy+CaG8gj9yjn5ZJF/vEMZGNR744owRuBVEfVwXZ c3CKp71VR7294w+lGXtF4/xLoPHNghnnT+JLXwK5xug1rWaaRaopUQtYTOzghQCxPLUyC2Mq 4g3H5LTl313DbOiCgGKr997BQ1afBATWMGqw+QKJ77rClQ9QgkJVaSOqY7NjqQ090ijvrqQp inVt44x4AGXuEAr3i3QNCg4Meu3BcwXQLBSFXVEAGtEEkMLOe6HhJrzvbNtFVX+3OA8n/NyU dcffMCMXqZGRjjdompPYp76o4hvew6smBqVeSGiZWFnLZJnQgXI/P7ifxfupXlVVXPs6pVhr u3yzB7fTLoCWx9mUJTcZsWpwg7jpnMagu9zAxbFL4ALKkXh+YRnMQLrifozL51eIBnP3GLDh QKbBBIDueTX5YM4qYGbiaeBpoavMu1/AksDQziFt+nrb3GC8zP6k4FaUeuOcTTMb0/O+f2vN bdP0vXxEPwbh1IW4YByJLBmkPAl7Nz1qr4GkwlpESyQPVSmA79tOEOLxc1eqqpJyuMLsAe6Q BvRqNZdPrqNNcz/F0MJP0wuaeHajaMYnTzb7PIUJkTm5X4np+HeChoMYBTc2jZAKLZVMZ8+x btzssAh7QHi2AEhNcyLj3wJ+mmBci4AXqEgus1ICYPnkFBwmFRLYJiZByOvpZ/RMpNDNU4lJ jLSj63H3uwOyk3Hens1NH7MwesN2shU6U4SlAcPdwaTh97Ipv4rxxkNoz45eQJYk0dc2OVpN 2k3akB4dPeK/ix0uc5YQmqoF10TDRGV4BKhmV4AlWnFSBunUWvCKGAyI+GQ5Ftc9mtadzdWv +rHmDe5DGi6I5iogGgvX1V4oefoV917+yXNn8eoG8mKBZ4neSGjiairPDJapxziCMI3pUvGu eg7rL0rMPaka3Ed8/8hFo2X9bUMUxTYdmZMdvdsofESFmbGdTDuhDWDJxzjc89BPaCbo0+kF 9R1dIUIWA65yT6V6D8cAqEILvl/m/tu68AFZ6usOWoPq7+CtX1yrZjL/TL/jmImTok8i8o7M Y+NJTuOHnbK3ilRkm7J6cRIYy+2P4BCawr70+S4tu4OEstb4u1rdEgz1JqyvmmUYFQ7pUPK5 Fubav+E1fFmxKRtg5DoTvdJCTKyJI6hT++P6g2y74lDYN6n3R0ibO/JRoQL/ji6PIf9n/xyn LWJ9dP7hQbL4u9wXGfelJ2MUaJO4K1emQaR3t3fdBFncemqAacAICfvP0i3LptGlN5S/M66X xD+Y8y1HTLQc8kI32VbMkCyDD5EY5karc7cSeeVoPOLBRwQ3hbAMcu8s3TuaAm3s8PO14LWU mfJhhpl2jyUQEmgyvPJ6zGKzqKU+GPeZJY=
- Ironport-hdrordr: A9a23:Yj4R8a1+MUeiT1hHNwMZ5QqjBBAkLtp133Aq2lEZdPULSKDo7/ xGzc53pGbJYWgqMgBHpTngAtj+fZq4z/FICOYqTMeftWXdyReVxcRZnP7fK9OJIVy+ygZyvZ 0QPZSWS+eAR2STtK7BkUaF+q8bsZm6GBXCv5aU854Sd3AfV0gQ1XYGNu/BKDw/eOAuP/NQf+ v5l7E32gZMYU5nFPhTREN1LNQrwee73a4OTiRmO/dN0nj+sdrH0s+JL/BYti1uNg+nAo1DzY EGqWLEDhXJiYD29vYR7R6x03xa8+GRvOeq9Ke3+78ow/zX+2TYA7hJavm5pTgw5Muv5FwpnN SJgxBlEd9092q5RBD5nSfQ
- Ironport-sdr: Pqhtw4spFd1GwEosT8dsspuvpIcebfM3gLNGgACa/mvrXv4Z6FagS3QMTF4llY+56mFa47br0U AA7mwYOZ7LyTsUUeLLggwYk7XRK/JDt8s8REANpqehdEW7fSoNulV7lNUgDb7q/jk/zQnryR5q 42zbiIENVe11V36wixgJbz1/qX2aECfjIyhjxQu1J/8RwxvN7pzYrZrAZnFhGxr7BBvlCWUcyr H3UiWVCJ39/4YO2ubEFX/zXfuQ3IdE+XTrDC6FF6tQLM3/IIr7D0WxFocC+w91YrpTvePQEh/i ReRJiiF18kStwPQYh/SeCu5I
- References: <78987ad6-5fb6-44d9-954f-eeef74557477n@googlegroups.com>
https://github.com/tlaplus/CommunityModules/blob/07ef2bc96e2af839318bbd96ae3ef7b80985f5b4/modules/Functions.tla#L42-L49
Markus
> On Feb 21, 2022, at 7:35 PM, thomas...@xxxxxxxxx <thomasgebert@xxxxxxxxx> wrote:
>
> Hi All,
>
> I would like to have a function that has a unique range for each element in the domain (e.g. like an ideal hash function).
>
> I was trying to CHOOSE my way into a function:
>
> BitString == [1..4 -> {0,1}]
> hash == CHOOSE i \in [0..3 -> BitString] : \A x, y \in 0..3: x /=y /\ i[x] /= i[y]
>
> But when I try running hash[2] in the evaluator, I get this error:
>
> Attempted to compute the value of an expression of form
> CHOOSE x \in S: P, but no element of S satisfied P.
>
> Anyone have an idea of how I can get my desired effect?
--
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/E1381852-74D4-42CC-8CDE-E38118E95B9E%40lemmster.de.