railroad.cta

很好的一本书

-- This is a model for a train-gate-controller.

// This is the so called "enviroment".
MODULE Train
{
    OUTPUT
      app: SYNC;
      exit: SYNC;
      
    LOCAL
      x: ANALOG;    // Distance of the train.

    INITIAL
     
      STATE(Train) = Far AND x >= 1000;
     

    AUTOMATON Train
    {
      STATE Far
      {
	INV   x >= 1000;  
	DERIV   DER(x) >= -50 AND DER(x) <= -40;  
	TRANS { GUARD   x = 1000;   SYNC !app; GOTO Near;}
      }

      STATE Near
      {
        INV   x >= 0;  
        DERIV   DER(x) >= -50 AND DER(x) <= -30;  
        TRANS { GUARD   x = 0;   GOTO Past;}
      }

      STATE Past
      {
        INV   x <= 100;  
        DERIV   DER(x) >= 30 AND DER(x) <= 50;  
        TRANS { GUARD   x = 100;   SYNC !exit; DO   x' = 1000;   GOTO Far;}
      }
    }
  }

  MODULE Controller
  {

    LOCAL
      t: CLOCK;    // Timer for the controller.

    INPUT
      app: SYNC;
      exit: SYNC;

    OUTPUT
      lower: SYNC;  // Lower the gate.
      raise: SYNC;  // Raise the gate.

    INITIAL
     
      STATE(Controller) = Idle;
     

    AUTOMATON Controller
    {
      STATE Idle   // Waiting for a signal from train.
      {
	TRANS { SYNC ?app;  DO   t' = 0;   GOTO ToLower;}
	TRANS { SYNC ?exit; DO   t' = 0;   GOTO ToRaise;}
      }

      STATE ToLower
      {
        INV   t <= 5;  
	TRANS {SYNC ?app; GOTO ToLower; }

	TRANS { SYNC !lower; GOTO Idle; }

	TRANS { SYNC ?exit; DO   t' = 0;   GOTO ToRaise; }
      }

      STATE ToRaise
      {
	INV   t <= 5;  
	TRANS { SYNC ?exit; GOTO ToRaise; }
	TRANS { SYNC !raise; GOTO Idle; }
	TRANS { SYNC ?app; DO   t' = 0;   GOTO ToLower; }
      }
    }
  }

  MODULE Gate
  {
    LOCAL
      g: ANALOG;    // Degree of the gate.

    INPUT
      lower: SYNC;  // Lower the gate.
      raise: SYNC;  // Raise the gate.

    INITIAL
     
      STATE(Gate) = Open AND g = 90;
     

    AUTOMATON Gate
    {
      STATE Open
      {
	INV   g = 90;  
	DERIV   DER(g) = 0;  
	TRANS { SYNC ?raise; GOTO Open; }
        TRANS { SYNC ?lower; GOTO Down; }
      }

      STATE Up
      {
	INV   g <= 90;  
	DERIV   DER(g) = 9;  
	TRANS { SYNC ?raise; GOTO Up; }
        TRANS { SYNC ?lower; GOTO Down; }
        TRANS { GUARD   g = 90;  GOTO Open; }
      }

      STATE Down
      {
        INV   g >= 0;  
        DERIV   DER(g) = -9;  
        TRANS { GUARD   g= 0;  GOTO Closed; }
        TRANS { SYNC ?raise; GOTO Up; }
        TRANS { SYNC ?lower; GOTO Down; }
      }
      STATE Closed
      {
        INV   g = 0;  
        DERIV   DER(g) = 0;  
        TRANS { SYNC ?raise; GOTO Up; }
        TRANS { SYNC ?lower; GOTO Closed; }  
      }
    }
  }

  MODULE RailRoadCrossing
  {
    LOCAL
    app  : SYNC;
    exit : SYNC;
    lower: SYNC;
    raise: SYNC;

    INST Process_Train FROM Train WITH
    {
      app AS app;
      exit AS exit;
    }

    INST Process_Gate FROM Gate WITH
    {
      lower AS lower;
      raise AS raise;
    }

    INST Process_Controller FROM Controller WITH
    {
      app AS app;
      exit AS exit;
      lower AS lower;
      raise AS raise;
    }
}

REACHABILITY CHECK RailRoadCrossing
{
    VAR
      initial, error, reached : REGION;

    COMMANDS
      // We use the initial regions from the modules.
      initial := INITIALREGION;

      error   :=   COMPLEMENT( STATE(Process_Gate.Gate) = Closed )
                 INTERSECT
                   Process_Train.x < 250;

      reached := REACH FROM initial FORWARD;

      IF( EMPTY(error INTERSECT reached) )
      {
        PRINT "Safety requirement satisfied.";
      }
      ELSE {
        PRINT "Safety requirement violated";
        PRINT "The resulting region:" reached " !";
      } 

}