[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] How come TLA never hits the assert?
- From: recepient recepient <netsmaza@xxxxxxxxx>
- Date: Sun, 15 Nov 2020 13:59:58 -0800 (PST)
Consider this process definition in which everything seems to run except, that once the if-then is evaluated, the assert is never hit. Without the assert, the process never seems to run the goto command either.
process MainProc \in NumClients+1..NumClients+1
variable rpc, msg;
print "await master_dequeue";
await MasterInQueue /= <<>>;
(* print << "master pre-dequeue:", MasterInQueue>>; *)
(* print << "master post-dequeue:", MasterInQueue>>; *)
rpc := rpc \o << MasterSequence >>;
Message := Message \o rpc;
print "goto master_dequeue";
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/05225570-30ba-45a6-ae5f-41a0c47cf2aan%40googlegroups.com.