Jspinでmtypeを使用するときの宣言されていない変数エラー

Question

JspinとPromelaを初めて使用しています。 、家庭用警報システムは、個人のIDキーまたはパスワードを使用して活性化し、無効にすることができ

、システムは約30秒の待機期間に入る活性化した後、ユーザーが避難することを可能にする時間を：私は、次のシステムを実装してみました警報が発令された後の安全区域、侵入が検知されたときにも警報器には待機時間または15秒の遅延があり、侵入者がパスワードを入力するかカードキーをスワイプして割り当てられた15秒以内に識別が行われない場合、アラームはオフになり、IDカードまたはパスワードを使用して無効にするまでオンになります。

これはコードです：

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 

をしかし、私は、ヘッダーでこれを宣言しました。

どうすればこの問題を解決できますか？

Answer 1

documentationのPromelaによれば、mtypeが正しく使用されています。

実際にはspinバージョン6.4.3でエラーを再現できません。この問題は、Jspinが正しく更新されていないと思われます。

あなたがspin代わりのJspinを使用する場合を除き、あなたは以下の回避策を試すことができ、でもJspinで動作するはず：誰もsignalから読まないので

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

... 

---

、私は、システムモデルがであり、未完成のものがであり、後でさらにプロセスが追加されると仮定します。

1. 以下命令シーケンスであることに注意してください：signalは同期チャネルあるため

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

   アトミックがalarmによってtemporarily lostであろう（それはサイズ0を有する）としたがって、別のプロセスは、送信されるメッセージを読むためにすぐににスケジュールする必要があります。あなたが戻っ0からcountをリセットcount >= 30off状態で

2. は、alarm_off = falseを設定し、状態onに行きます。 on州では、すぐにalarm_offをtrueに戻します。これは意図されていますか？何らかの間違いのように見えますが、おそらく状態pendingに行くことを意味していました。

3. alarmには、ある種類のinput信号が欠落しているように見えます。 signalチャンネルを意図した目的とは異なる方法で使用していると思われます。適切な個人ID/パスワードが使用されている場合には

4. モデルは、offの状態pendingからいくつかの変遷を持っていないでしょうか？あなたの答えのための