"mcresponse is undefined" when model does not match its specification

[frans-bergman]

When model checking a model which does not match one or more of its specifications, an alert with the message "mcresponse is undefined" is shown, followed by a react.js debugging page.

Example to trigger this issue:

channels: ctos, stoc

enum msgvals {SYN, SACK, ACK, DATA, FIN}

enum tcpstate {listening, connecting, connected, closing}

message-structure: MSG : msgvals, SEQ : int
communication-variables: nop : int

agent Client
    local: tstate : tcpstate, seq : int, in : channel, out : channel
    init: tstate == connecting && seq == 20
    relabel:
        nop <- 0
    receive-guard: (channel == in)

    repeat: (
                <tstate == connecting> out ! (TRUE) (MSG := SYN, SEQ := seq) [seq := seq + 1];
                <MSG == SACK> in ? [tstate := connecting];
                <tstate == connecting> out ! (TRUE) (MSG := ACK, SEQ := seq) [tstate := connected, seq := seq + 1];
                <tstate == connected && MSG == DATA> in ? [];

                <TRUE> out ! (TRUE) (MSG := FIN, SEQ := seq) [seq := seq + 1];
                <MSG == ACK> in ? [tstate := listening];

                <MSG == FIN> in ? [tstate := closing];
                <TRUE> out ! (TRUE) (MSG := ACK, SEQ := seq) [seq := seq + 1]
            )

agent Server
    local: tstate : tcpstate, seq : int, in : channel, out : channel
    init: tstate == listening && seq == 10
    relabel:
        nop <- 0
    receive-guard: (channel == in)

    repeat: (
                <tstate == listening & MSG == SYN> in ? [tstate := connecting];
                <tstate == connecting> out ! (TRUE) (MSG := SACK, SEQ := seq) [seq := seq + 1];
                <MSG == ACK> in ? [tstate := connected];
                <tstate == connected> out ! (TRUE) (MSG := DATA, SEQ := seq) [seq := seq + 1];

                <tstate == connected & MSG == FIN> in ? [tstate := closing];
                <tstate == closing> out ! (TRUE) (MSG := ACK, SEQ := seq) [seq := seq + 1];

                <tstate == connected> out ! (TRUE) (MSG := FIN, SEQ := seq) [seq := seq + 1];
                <tstate == connected & MSG == ACK> in ? [tstate := listening]
            )

system = Server(server, in == ctos && out == stoc) | Client(client, in == stoc && out == ctos)

SPEC G (server-tstate == connected && client-tstate == connected)

[lou1306]

Fixed in ebff8d7

I tried re-running your example with the current version on main (commit 9bba67c): there is no error anymore and the counterexample is loaded correctly into the interpreter (as far as I can see).