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.de
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.
You have to override the value of Nat to be some set like 0 .. 100 or something.
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.
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.
|