Hello,From your example, it seems Spec should be: Init /\ [][Next]_vars, assuming vars is already a tuple/sequence. I am not sure if that solves your problem, though.JonesOn Friday, 24 December 2021 at 13:59:20 UTC-3 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 \/ BSpec == 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 \/ AI get the warning "A is never enabled." Am I missing something obvious about disjunction?Thanks for any insights in advance!