由于示例中的代码似乎不符合规范，至少在我理解的方面，我写道从头开始的例子.

As the code in the example doesn't appear to follow the specification, at least in the way I understand it, I wrote an example from scratch.

请注意，以下 model (源代码)故意在结构上非常冗长和多余，以便更轻松地识别其逻辑块并-希望 - 明白它.在实践中，可以使用一些内联函数来处理输入.我也没有使用原始模型中出现的SIGACT, SIGDEACT，因为我无法弄清楚谁应该从原始模型(源代码)或规范.

Please note that the following model (source code) is purposely very verbose and redundant in its structure, so that its easier to recognise its logic blocks and --hopefully-- understand it. In practice, one would use some inline function to handle input. I also didn't use SIGACT, SIGDEACT which appeared in the original model, since I could not figure out who was supposed to read those messages neither from the original model (source code) nor from the specification.

#define ALARM_OFF        1
#define ALARM_COUNTDOWN  2
#define ALARM_ARMED      4
#define ALARM_INTRUSION  8
#define ALARM_FIRED     16

#define INPUT_SET_PASSWORD   1
#define INPUT_CHECK_PASSWORD 2
#define INPUT_INTRUDER       4

mtype = { SIGACT, SIGDEACT };

init {
    chan alarm_out = [1] of { mtype };
    chan alarm_in =  [1] of { byte, short };

    run alarm(alarm_in, alarm_out);
    run user(alarm_in);
    run event(alarm_in);
}

proctype alarm(chan input, output)
{
    byte count;
    byte state   = ALARM_OFF;
    short passwd = 1234;
    short tmp    = 0;

off:
    if
        :: nempty(input) ->
            if
                :: input?INPUT_SET_PASSWORD(tmp) ->
                    passwd = tmp;
                :: input?INPUT_CHECK_PASSWORD(tmp) ->
                if
                    :: tmp == passwd ->
                        atomic {
                            state = ALARM_COUNTDOWN;
                            count = 0;
                            goto countdown;
                        }
                    :: else ->
                        skip;
                fi;
                :: input?INPUT_INTRUDER(tmp) ->
                    skip;
            fi;
        :: empty(input) -> skip;
    fi;
    goto off;

countdown:
    if
        :: count < 30 ->
            if
                :: nempty(input) ->
                    if
                        :: input?INPUT_SET_PASSWORD(tmp) ->
                            skip; // error: cannot be done now (?)
                        :: input?INPUT_CHECK_PASSWORD(tmp) ->
                            if
                                :: tmp == passwd ->
                                    atomic {
                                        state = ALARM_OFF;
                                        count = 0;
                                        goto off;
                                    }
                                :: else ->
                                    skip; // error: incorrect password (?)
                            fi;
                        :: input?INPUT_INTRUDER(tmp) ->
                            skip;
                    fi;
                :: empty(input) ->
                    skip;
            fi;
        :: else ->
            atomic {
                state = ALARM_ARMED;
                count = 0;
                goto armed;
            }
    fi;
    count++;
    goto countdown;

armed:
    if
        :: nempty(input) ->
            if
                :: input?INPUT_SET_PASSWORD(tmp) ->
                    skip; // error: cannot be done now (?)
                :: input?INPUT_CHECK_PASSWORD(tmp) ->
                    if
                        :: tmp == passwd ->
                            atomic {
                                state = ALARM_OFF;
                                count = 0;
                                goto off;
                            }
                        :: else ->
                            skip; // error: incorrect password (?)
                                  // maybe it should be handled like
                                  // INPUT_INTRUDER(tmp)
                    fi;
                :: input?INPUT_INTRUDER(tmp) ->
                    atomic {
                        state = ALARM_INTRUSION;
                        count = 0;
                        goto intruder_detected;
                    }
            fi;
        :: empty(input) ->
            skip;
    fi;
    goto armed;

intruder_detected:
    if
        :: count < 15 ->
            if
                :: nempty(input) ->
                    if
                        :: input?INPUT_SET_PASSWORD(tmp) ->
                            skip; // error: cannot be done now (?)
                        :: input?INPUT_CHECK_PASSWORD(tmp);
                            if
                                :: tmp == passwd ->
                                    atomic {
                                        state = ALARM_ARMED;
                                        count = 0;
                                        goto armed;
                                    }
                                :: else ->
                                    skip; // error: incorrect password (?)
                            fi;
                        :: input?INPUT_INTRUDER(tmp) ->
                            skip;
                    fi;
                :: empty(input) ->
                    skip;
            fi;
        :: count >= 15 ->
            atomic {
                state = ALARM_FIRED;
                count = 0;
                goto alarm_fired;
            }
    fi;
    count++;
    goto intruder_detected;

alarm_fired:
    if
        :: nempty(input) ->
            if
                :: input?INPUT_SET_PASSWORD(tmp) ->
                    skip; // error: cannot be done now (?)
                :: input?INPUT_CHECK_PASSWORD(tmp);
                    if
                        :: tmp == passwd ->
                            atomic {
                                state = ALARM_OFF;
                                count = 0;
                                goto off;
                            }
                        :: else ->
                            skip; // error: incorrect password (?)
                                  // warn user but keep alarm on
                    fi;
                :: input?INPUT_INTRUDER(tmp) ->
                    skip;
            fi;
        :: empty(input) ->
            skip;
    fi;
    goto alarm_fired;
};

proctype user(chan output)
{
    output ! INPUT_CHECK_PASSWORD(1234);
};

proctype event(chan output)
{
    output ! INPUT_INTRUDER(0);
};

因此，基本上，您必须检查两者 input (如果有！)和count的值，以执行转换在alarm系统的内部 FSM 中.

So, basically you have to check both the input (if any!) and the value of count in order to perform a transition in the internal FSM of the alarm system.

在示例中，我添加了一个名称为event的proctype，它将向alarm系统随机发送一个单独的INPUT_INTRUDER输入信号.结合user键入自己的密码，该密码可用于触发一系列事件，这些事件将导致警报触发.

In the example I added a proctype of name event which will randomly send a single INPUT_INTRUDER input signal to the alarm system. This, in combination with the user typing his own password, can be used to trigger the chain of events which would cause the alarm to fire.