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

Question

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

家庭报警系统可以使用个人ID密钥或密码，激活后系统进入等待状态大约30秒的时间，允许用户撤离安全区域，在该区域之后报警，也在发生入侵时检测到报警有一个内置的等待期或延迟15秒，允许入侵者输入密码或刷卡钥匙，从而表明自己的身份，以防身份不是在分配的15秒内发出警报直到使用身份证或密码将其停用。

这是我尝试过的：

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; }   
}

在user程序类型中，我发送密码

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，它将随机向alarm系统发送单个INPUT_INTRUDER输入信号。这与user键入自己的密码相结合，可用于触发将导致警报启动的事件链。