Re: [tlaplus] action never enabled

I do not think your hypothesis is consistent with the description in section 14.2.6 of "Specifying System" which describes how TLC computes states. TLC "should" calculate all possible histories which would prohibit calculating A "first." As far as I understand these things, temporal logic, disjunction in particular, has no notion of calculating something "first", in contrast to a programming language.

Stephan:

My reply above to Jones' explanation also applies to your comment about TLC's evaluation strategy. Also, my post earlier in this thread contains the spec.

I'm really quite stumped!

On Saturday, December 25, 2021 at 1:55:00 AM UTC-8 Stephan Merz wrote:

Hello,

this might be an artefact of TLC evaluating formulas from left to right. Perhaps we could say more if you could share your spec (or a minimum working example if it is too big).

Regards,
Stephan

On 24 Dec 2021, at 17:59, Mark Ettinger <jetti...@xxxxxxxxx> wrote:

TLA+ newbie here with what is probably a newbie-ish question. I'll describe it abstractly with actions A and B. My spec has the form:

Next == A \/ B
Spec == Init /\ []Next_<<vars>>

When I run TLC I get a warning "B is never enabled". If I change the ordering in Next to:

Next == B \/ A

I get the warning "A is never enabled." Am I missing something obvious about disjunction?

Thanks for any insights in advance!

--
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ecbf0cb0-29ad-4af6-81c1-4b6d08a7647an%40googlegroups.com.