如何将给定的输入绑定到另一个 proctype 函数？

Question

根据以下问题，我需要一些帮助，我必须使用 jSpin 和 promela 语言来实现它。

A home alarm system can be activated and deactivated using a personal ID key or password, after activation the system enters a waiting period of about 30 seconds, time that allows users to evacuate the secured area after which the alarm is armed, also when an intrusion is detected the alarm has a built in waiting period or delay of 15 seconds to allow the intruder to enter the password or swipe the card key thus identifying himself, in case that the identification is not made within the allocated 15 seconds the alarm will go off and will be on until an id card or password is used to deactivate it.

这是我尝试过的：

mtype = {sigact, sigdeact};
chan signal = [0] of {mtype};
chan password = [0] of { int }; 
/*chan syntax for declaring and initializing message passing channels*/

int count;
bool alarm_off = true; /*The initial state of the alarm is off*/    
active proctype alarm()    
{
    off:
       if 
         :: count >= 30 -> atomic {signal!sigdeact; count = 0;alarm_off = false; goto on;}
         :: else -> atomic {count++; alarm_off = true; goto off;}
       fi;

    on:
        if
          :: count >=15 -> atomic { signal!sigact; count = 0;
    alarm_off = false; goto off;}
          :: else -> atomic {signal!sigact; alarm_off = true; goto pending;}
        fi;

    pending:

        if
           :: count >= 30 -> atomic {count = 0; alarm_off = false; goto on;}
           :: count < 30 -> atomic {count++; alarm_off = false; goto pending;}
        fi;
}

active proctype user()
{    
   password ! 1234 //1234 is the password I sent. 
   input:  atomic { signal?sigact ->  alarm_off = true; goto off; }   
}

在userproctype我发密码

password ! 1234

如何验证密码是否为 1234 以及如何根据验证使它适应自己的情况（on、off、pending）？

Answer 1

由于示例中的代码似乎不符合规范，至少在我的理解中，我从头开始写了一个示例。

请注意以下模型（~~源代码~~）在结构上故意非常冗长和冗余，以便更容易认识它的逻辑块并——希望——理解它。实际上，人们会使用一些 内联函数 来处理输入。我也没有使用原始模型中出现的 SIGACT, SIGDEACT，因为我无法弄清楚谁应该从原始模型中读取这些消息（~~源代码~~) 也不来自规范.

#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 中执行转换。

在示例中，我添加了名称为 event 的 proctype，它将随机发送单个 INPUT_INTRUDER 输入信号到 alarm 系统。这与 user 键入自己的密码相结合，可用于触发事件链，从而导致 警报触发 。

如何将给定的输入绑定到另一个 proctype 函数？

How can I bind the given input to another proctype function?

model-checking

spin

promela