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;
begin
master_dequeue:
print "await master_dequeue";
await MasterInQueue /= <<>>;
(* print << "master pre-dequeue:", MasterInQueue>>; *)
rpc:=Head(MasterInQueue);
MasterInQueue:=Tail(MasterInQueue);
(* print << "master post-dequeue:", MasterInQueue>>; *)
master_combine:
rpc := rpc \o << MasterSequence >>;
Message := Message \o rpc;
MasterSequence:=MasterSequence+1;
master_handler:
if (rpc[RpcOpIdx]=OP_GET)
then
skip;
else
call masterWrite(rpc);
end if;
master_cont:
assert FALSE;
print "goto master_dequeue";
goto master_dequeue;
end process;