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.

• Alvis model
• LTS graph

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

• Alvis model
• LTS graph

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