waterlevel.cta

很好的一本书

/* 
 * model:   Hybrid CTA-model of a water level monitor.
 * modules: WaterLevel
 * 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 WaterLevel
{
    LOCAL
      x: CLOCK;
      y: ANALOG;

    INITIAL
      STATE(WaterLevel) = On0 AND y = 1;

    AUTOMATON WaterLevel
    {
      STATE On0
      {
	INV   y <= 10;  
	DERIV   DER(y) = 1;  
	TRANS { GUARD   y = 10;  
	        DO   x' = 0;  
                GOTO On1;
        }
      }
      STATE On1
      {
        INV   x <= 2;  
        DERIV   DER(y) = 1;  
        TRANS { GUARD   x = 2;  
                DO   TRUE;  
                GOTO Off0;
	}
      }
      STATE Off0
      {
        INV   y >= 5;  
        DERIV   DER(y) = -2;  
        TRANS { GUARD   y = 5;  
                DO   x' = 0;  
		GOTO Off1;
	}
      }
      STATE Off1
      {
        INV   x <= 2;  
        DERIV   DER(y) = -2;  
        TRANS { GUARD   x = 2;  
                DO   TRUE;  
		GOTO On0;
	}
      }
    }
}

REACHABILITY CHECK WaterLevel
USE DDM
{
  VAR 
    initial, error, property, reachable: REGION;

  COMMANDS
    initial := STATE(WaterLevel) = On0 AND y = 1;
    error := (y <= 1) UNION (y >= 12);
    property := (y >= 1) INTERSECT (y <= 12);

    reachable := REACH FROM initial FORWARD IN 100 STEPS;

    IF(property CONTAINS reachable)
    { 
      PRINT "Invariant satisfied."; 
    }
    ELSE 
    { 
      PRINT "Invariant violated."; 
    }     
}