# Re: [tlaplus] Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat

• From: Stephan Merz <stephan.merz@xxxxxxxxx>
• Date: Tue, 2 Aug 2022 18:30:00 +0200
• Ironport-data: A9a23:KhLC2aLIJojGAdU/FE+RTJAlxSXFcZb7ZxGr2PjKsXjdYENS3jEDz GceX2zTbq3fMDTyfI9zbI+1oElX6JPcm9IyQAQd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6jefSLlbFILas1hpZHGeIcw98z0M48wIFqtQw24LhU1vX4 YiaT/D3YTdJ5RYkagr41IrY8HuDjNyq0N/PlgFWiVhj5TcyplFNZH4tDfnZw0jQHuG4KtWHq 9Prl9lVyI92EyAFUbtJmp6jGqEDryW70QKm0hK6UID66vROS7BbPqsTbJIhhUlrZzqhu8hq8 vBSipyMEyQ2FfHjyMkYdEF3HHQrVUFG0OevzXmXtMWSywjZaSKpzas3Sk4xOoIc96B8BmQmG f4wcmhcKEDewbjsmfTlE4GAhex7RCXvFJ8bs2lk0CqaB/Ata7vsH53624Jp7RcKrOxwNsvhQ /M8RgNCRzfxOS90E38YD5UxmOqnnH7iayYeo1WQzUYyyzKLklIsjOC2WDbTUtCqHuhrkRy2n 23t8U3/PDxGKISe+APQpxpAgceWxX+hMG4IL5W09+VhnUaI7nAXAVsTTkH+oP+ji0f4WtRFK kVS9DBGkEQp3EmiT924QAfh5XDa51gTXN1fF+B84waIokbJ3+qHLkwcVQRkd+MmiJUVWhd2+ Q+kmvSxKjM65dV5Vkmh3ruTqDqzPw0cImkDeTIIQGM5Dz/L8NFbYvXnHoYLLUKlsjHmMWqvn G3S/UDSk51W3JFbjfzqlbzSq2v0/sChc+Ij2unAsouYAu5RYYekY8m38wGe46gZaomeSVaFs T4PnM32AAEy4XOly3DlrAYlRunBCxO53Nv03Q8H834Jq2rFxpJbVdoMiAyS3W8wWir+RRfnY VXIpSRa74JJMX2hYMdfOtzsWp91nfa6SI+/C5g4i+aihLAhK2drGwk+NSatM5zFzSDAbIlkZ MnFL5/0ZZrkIf03k2PmLwvi7VPb7nlmmTm7qWHTwBOg3r6TDEN5up9UWGZimtsRvfPsiFyNr b53bpLaoz0CDrGWSnSIqeY7cABbRVBmVMueg5EGJoarfFA6cEl/UKW56e16K+RYc1F9yo8kC FngAREIoLc+7FWcQTi3hodLMuy/Bccu8S9rbETB/z+AghAeXGpm149HH7NfQFXt3LULISdcQ 6ZXdsOeLO5ITzibqT0RYYOk8t5tcxOkgQ+BJS24eCN5dJllHlSb9tjhdwrp1S8PEivm5ZBl+ ub/iFzWEcgZWgBvLMfKc/bznVm/in4QxbBpVEzSL9gPJUjhqdA4KyH4gvItDdsLLBHPmmmT2 wqMUEUXoODMp8k+99yQ3fKIqIKgEu1fGEtGHjmDvezma3WCpmf6mN1OSueFezzZRVjYwqT6a LUH1ez4Pd0GgE1O7NhxHrNt+qQ0uIniqrpc+QJ7RSmZYlmuDIRgFXmIx8x4sKNAm+1CsgysV 0PTo9RXNOzSasPoGVIcPjAoduCSyfYQlmWA5Pg5OhyktiBw+7WDXEpIOASUk2pWK74saNEpx uIoucg37Q2ji0t6aY3f1X8KqGncfGYdV6gHt40BBNO5gAQczFwfM4fXDTX74c3SZthBbhsqL zuTiPaQjrhQ3BCZIX86FHyIwvAEwJpQ4VZFy1gNI1nPkd3A36dl0BpU+DUxbwJU0hQXjL4pa zYzbxV4dfeU4jNlpMlfRGTwSQtPMxuUpx7qwFwTmWyFEkSlBz7JLXYhBOCW4Uod/z4OdzRX5 u/ImmPsUDL2e5P+2Sw9XUNqsfv+Vcc08wTEkc+qXJ/aT8hmPGS13fb3OykVrQD6C9g6nkzNq MFl++F/baD0LykNu7Z9AI6fjOxCRBeBLW1EYPdg4KJYTTqHIWrth2eDexKrZ8dAB/3W6kvkW cZgEcRCCkal3yGUozFHWKMBL+MmlfIl/oZTKLP3OXYd4fzYoSBurYrLsCf5g2AvTpNllsN6J ZnWairFDmiZnX9JgCjWscNfMXC5a9QJaVGuxuyz6+lVRZsPvPs2KhM327qw+mqPaU5poUvSs wTEaKvbiedlzN00zYfrF6xCASSyKM/yBLvUqlHt64wWYIOdK9rKuiMUtkLjY1ZcM4wXVoklj r+KqtP2gB7Isbtev7o1QHVd+3SlJPleXda79uryJXhe2DSYAYrivUJF9Ge/JphE1tha46FLg ud+hNSYLbYotxV1nRW5qBSy1z4SDKP4aqrvvySgt+/KAR8YueACBM3y7mfnNAm3aQdRU6ATy WbIVzKG6ddfo4BBCwUDGul9RZR/JTcPnEfgm8LZ7VGlM4Vjvr9OVnYOW/btBfEnx0RoyPrH3 K8=
• Ironport-hdrordr: A9a23:DhDsjaFHVc2Z8PuRpLqFtpHXdLJyesId70hD6qkvc3AlCfBwxv rC7YwmPEHP4kdpZJhAo6HxBEDkexyzyXcb2/hlAV7PZniWhILsFvAV0WMNqweQXhEX2IZmpO VdmutFeZPN5WETt7e43ODAKadl/DEzm5rYyts2sU0dBD2CGpsQnDuRUTzrXnGeLTMubfFJc+ vnl7Y32QZMYU5nE/hTREN1K9Qrwee72a4OTiRnO/dN0nj9sdrH0s+ML/BYti1uNw+nAo1Skl QtUTaZ2k0S2MvLiiM0G1Wjjai+4OGRgueqCae3+4IowsWGsHfiWG2pYczmzVZF392H2RIRid HJ5z0gM85w536UXmbwjwDqxxCI6kdu10Pf
• Ironport-sdr: i/O+jMPWiJkfoWTfRKboLiuqXZcNOCTfeelapLnaHJv5wJ8srodovsJgG56GKPM7X1yw9RNaNE KJ29jBYKwrgMK0zciLrVgQTcl27R+C8Lqmm2/74WFLjmfEbU4/m2dhogthONuckcGeRFPowxQ/ 6Dk+ld3dDg/lKCWICDYpm8UOfK00/HKMGN8KmY78RFxgB3NVuGP5D4bwM/fQ8EaZalvAL5+d+O 3cK4z1JAk1tFAeohX3BshFwnarNrejzgxPYQHEkaotF6QDeDhw6tX910cX74dpxRw6Ad8pksDy F/G3pfIrW2L1BSPmNhO6j5Ge
 TLC will choke whenever you quantify over or try to enumerate an infinite set – even if the end result is finite as in{ n \in Nat : 0 < n /\ n < 10 }.ProB [1] accepts TLA+, it is based on a constraint solver and can handle such cases.Apalache is mostly restricted to finite data structures, in particular any sets occurring as values have to be finite. You can (usually) get away with unbounded integers as data because SMT solvers handle them natively, so you may not need a state constraint bounding integer values in the same way as in TLC.Indeed, TLAPS has no restrictions when it comes to reasoning about infinite sets – but you have to write a proof in the first place.Stephan[1] https://prob.hhu.deOn 2 Aug 2022, at 18:14, Andrew Helwer wrote:You can't enumerate infinite sets with the TLC model checker, although I think you can do simple checks like n \in Nat without overriding Nat. TLAPS and (I think?) Apalache support reasoning over infinite sets.On Tuesday, August 2, 2022 at 10:11:20 AM UTC-4 brandon...@gmail.com wrote:Got it, makes sense - I suppose in time I will see some use for infinite sets, since they exist in TLA.On Tuesday, August 2, 2022 at 8:20:51 AM UTC-4 andrew...@xxxxxxxxx wrote:You have to override the value of Nat to be some set like 0 .. 100 or something.On Monday, August 1, 2022 at 4:35:03 PM UTC-4 brandon...@xxxxxxxxx wrote:Apologies, minor typo (though the issue is unrelated) - due to a refactor I should have had randomActiveCampaign[c], not randomActiveCampaign[c.id], in the last snippet. Like this:CreateActiveCampaign ==  /\ campaign' = \E c \in CAMPAIGN :    IF campaign[c.id] = {} THEN      [campaign EXCEPT ![c.id] = c /\ randomActiveCampaign[c]]    ELSE campaign[c.id]On Monday, August 1, 2022 at 4:31:59 PM UTC-4 Brandon Barker wrote:A little more context. Although those are the only places I'm referencing startDate directly, I am positing the existence of a campaign (of which campaign details is a member of) here:CreateActiveCampaign ==  /\ campaign' = \E c \in CAMPAIGN :    IF campaign[c.id] = {} THEN      [campaign EXCEPT ![c.id] = c /\ randomActiveCampaign[c.id]]    ELSE campaign[c.id]I'm not sure how TLC is handling this under the hood; in principle, I'm constraining the values of startDate to be finite by using randomActiveCampaign, but I'm not sure if that is how things are composing here.On Monday, August 1, 2022 at 4:14:59 PM UTC-4 Brandon Barker wrote:Hello,I'm having an issue running TLC on a model where, so far, I'm just "creating" a somewhat complex record, and not doing much else. Here is one component of the record:CAMPAIGN_DETAILS == [    startDate: Nat  , endDate: Nat  ]\*randomFutureCampaignDetails[details \in CAMPAIGN_DETAILS] ==  /\ details.startDate \in currentTime..monthsToSeconds[3]  /\ details.endDate \in (details.startDate+1)..monthsToSeconds[3]randomFutureCampaignDetails is used, indirectly, from Next. This results in the following error from TLCThe exception was a java.lang.RuntimeException: Attempted to enumerate a set of the form [l1 : v1, ..., ln : vn],but can't enumerate the value of the `startDate' field:NatIt seems like I have bounded startDate to a finite set in: details.startDate \in currentTime..monthsToSeconds[3]Are there any suggestions for debugging this sort of error? -- 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/692789fc-88b9-4d44-8251-a21dc2e93ad7n%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/70E6C0D0-61EE-4927-B98E-DAFC12A2EBB1%40gmail.com.