title: How can I bind the given input to another proctype function?
body: <p>I need some help according to follow problem which I have to implemented it using <code>jSpin</code> and <code>promela</code> language.</p>
  
  <blockquote>
    <p>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.</p>
  </blockquote>
  
  <p>Here is what I tried:</p>
  
  <pre><code>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 &gt;= 30 -&gt; atomic {signal!sigdeact; count = 0;alarm_off = false; goto on;}
           :: else -&gt; atomic {count++; alarm_off = true; goto off;}
         fi;
  
      on:
          if
            :: count &gt;=15 -&gt; atomic { signal!sigact; count = 0;
      alarm_off = false; goto off;}
            :: else -&gt; atomic {signal!sigact; alarm_off = true; goto pending;}
          fi;
  
      pending:
  
          if
             :: count &gt;= 30 -&gt; atomic {count = 0; alarm_off = false; goto on;}
             :: count &lt; 30 -&gt; atomic {count++; alarm_off = false; goto pending;}
          fi;
  }
  
  active proctype user()
  {    
     password ! 1234 //1234 is the password I sent. 
     input:  atomic { signal?sigact -&gt;  alarm_off = true; goto off; }   
  }
  </code></pre>
  
  <p>In the <code>user</code> <strong>proctype</strong> I send the password</p>
  
  <pre><code>password ! 1234
  </code></pre>
  
  <p>How can I verify if the password is <code>1234</code> and how can I adapt it to own cases ( <code>on</code>, <code>off</code> , <code>pending</code>) based on the verification ? </p>