[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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...@xxxxxxxxx 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 TLC

The 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:
Nat

It 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.