gasburner.cta

很好的一本书

/* 
 * model:   Hybrid CTA-model of simple Gasburner example.
 * modules: GasBurner
 * author:  Dirk Beyer, 2000
 * last change: 2001-12-20 mvogel
 * 
 * Based on: Alur, Courcoubetis, Henziger, Ho
 *           "Hybrid Automata: An Algorithmic Approach to the Specification
 *           and Verification of Hybrid Systems"
 */ 

MODULE GasBurner
{
  LOCAL
    x : CLOCK;     // Counts time elapsed in a state.
    y : CLOCK;     // Overall time elapsed.
    z : STOPWATCH; // Counts the time the gasburner was leaking.

  INITIAL
    STATE(Auto) = Leaking AND x = 0 AND y = 0 AND z = 0;

  AUTOMATON Auto
  {
    STATE Leaking
    {
      INV x <= 1 AND 
          x >= 0 AND y >= 0 AND z >= 0;
      DERIV DER(z) = 1;  
      TRANS { DO x' = 0;  
              GOTO NotLeaking;
      }
    }
    STATE NotLeaking
    {
      INV x >= 0 AND y >= 0 AND z >= 0;
      DERIV DER(z) = 0;  
      TRANS { GUARD x >= 30;  
              DO x' = 0;  
              GOTO Leaking;
      }
    }
  }
}

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

  COMMANDS

    initial := INITIALREGION;

    error := (y >= 60) AND (20 * z >= y);

    reached := REACH FROM error BACKWARD;

    IF( EMPTY( reached INTERSECT initial ) )
    {
      PRINT "Requirements satisfied.";
    }
    ELSE
    {
      PRINT "Invalid configuration reachable.";
    }
}