[tlaplus] How come TLA never hits the assert?

[recepient recepient <netsmaza@xxxxxxxxx>]

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;

-- 
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.