2

我是新手Jspin和Promela。我试图实现以下系统：

家庭警报系统可以使用个人 ID 密钥或密码来激活和停用，激活后系统进入大约 30 秒的等待期，该时间允许用户撤离安全区域，之后警报被布防，即使是在入侵时检测到警报有一个内置的等待时间或延迟 15 秒，以允许入侵者输入密码或刷卡钥匙从而识别自己，如果在分配的 15 秒内未进行识别，警报将响起并将一直打开，直到使用身份证或密码将其停用。

这是代码：

mtype = {sigact, sigdeact};
chan signal = [0] of {mtype};
/*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 off;}
    fi;

pending:

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

当我运行代码时，Jspin我收到以下消息：

Error: undeclared variable: sigact

但我在标题中声明了这一点。

我该如何解决这个问题？

4

1 回答 1

1

根据 的文档，Promela您使用mtype正确。

实际上，我无法使用spinversion重现您的错误6.4.3，因此我怀疑这是Jspin未正确更新的特定问题。

除非您想使用spin而不是 ，否则Jspin可以尝试以下解决方法，即使使用Jspin：

#define sigact   0
#define sigdeact 1
chan signal = [0] of {short};   // or bool for only 2 values

...

由于没有人从 中读取signal，我假设系统模型不完整，稍后将添加更多进程。

  1. 请注意，在以下指令序列中：

    atomic { signal!sigdeact; count = 0; alarm_off = false; goto on; }

    由于是同步通道（它具有 size ） ，原子性将暂时丢失，因此必须立即安排另一个进程来读取正在发送的消息。alarmsignal0

  2. 在offstate 中，当count >= 30您重置count回 时0，设置alarm_off = false然后转到 state on。在on状态下，您立即设置alarm_off回true. 这是故意的吗？看起来有些错误，也许你的意思是去 state pending。

  3. 通过阅读系统的描述，看起来好像alarm缺少某种input信号。我怀疑您使用signal频道的方式与其预期目的不同。

  4. 如果使用正确的个人 ID /密码，模型不应该从 state 转换pending到吗？off

于 2017-11-08T12:55:07.427 回答