====== Automatic Train Stop system - version 1 ======

Automatic Train Stop system (ATS system) is a kind of an Automatic Train Protection system used to guarantee a train safety even if the driver is not  capable of controlling the train. ATS system turns on a light signal every 60 seconds to check whether the driver controls the train. If the driver fails to acknowledge the signal within 6 seconds, a sound signal is turned on. Then, if the driver does not disactivate the signals within 3 seconds, using the acknowledge button, the emergency brakes are applied automatically to stop the train. 

===== Files =====

  * {{:alvis:cases:ats1.alvis|Alvis model}}
  * {{:alvis:cases:ats1e.dot|LTS graph}}

===== Model =====

{{:alvis:cases:ats1.png|}}

<code>
environment {
  in wakeup [] (map (60000*) [0..]) durable;
  in off [] (map (1000*) [1..]) signal;
  out warning [0,1,2] [];
  out brake [] [];  
}

agent ATS {
  loop {
    in wakeup;
    out warning 1;
    select {
      alt (ready [in(off)]) {
        in off;
        out warning 0; 
      }
      alt(delay 6000) {
        out warning 2;
        select {
          alt (ready [in(off)]) {
            in off;
            out warning 0; 
          }
          alt (delay 3000) {
            out brake;
            exit; 
          } 
        } 
      } 
    } 
  } 
}
</code>


====== Automatic Train Stop System - version 2 ======

===== Files =====

  * {{:alvis:cases:ats2.alvis|Alvis model}}
  * {{:alvis:cases:ats2e.dot|LTS graph}}

===== Model =====

{{:alvis:cases:ats2.png|}}

<code>
environment {
  in off [] (map (1000*) [1..]) signal;
  out brake [] [];  
}

agent ATS {
  loop {
    in wakeup;
    out warning 1;
    select {
      alt (ready [in(off)]) {
        in off;
        out warning 0; 
      }
      alt(delay 6000) {
        out warning 2;
        select {
          alt (ready [in(off)]) {
            in off;
            out warning 0; 
          }
          alt (delay 3000) {
            out brake;
            exit; 
          } 
        } 
      } 
    } 
  } 
}

agent Timer {
  loop (every 6000) {
    out tick;
  }
}

agent Console {
  state ::Int = 0;
  proc setState { in setState state ; }
}
</code>