twostate6.cta

很好的一本书

/* 
 * project: CTA-model of parallel running simple TwoState automata.
 * modules: TwoState, System
 * author:  Dirk Beyer, 2000
 * last change: 2001-03-28 mvogel
 * 
 * Based on: Marius Bozga, Oded Maler, Amir, Pnuelli, Sergio Yovine,
 *            "Some Progress in the Symbolic Verification of Timed Automata",
 *           In O. Grumberg, editor, Proceedings of the 9th International
 *           Conference on Computer Aided Verification (CAV'97), LNCS 1254,
 *           pages 179-190, Springer Verlag, 1997,
 *
 * The model uses internal clocks in every instance of TwoState.
 * Compare with TwoState models using external clocks, signed by the
 * filename with 'extClock' postfix. 
 */

// This module represents the template for a TwoState process.
MODULE TwoState
{
  INPUT
    // l is the minimal time (lower timebound) the automaton has to
    // stay in a state, while u is the maximal time (upper timebound)
    // it has to stay.
    l:            CONST;
    u:            CONST;
 
  // Set initial state of automaton and value of clock variable c.
  INITIAL   STATE(twoState) = one
                   AND c = 0;  
    
  AUTOMATON twoState
  {
    STATE one  { INV   c + 1 <= u;  
                 TRANS { GUARD   c >= l;  
                         DO   c' = 0;  
		         GOTO two;
                       }
               }
    
    STATE two  { INV   c + 1 <= u;  
                 TRANS { GUARD   c >= l;  
	                 DO   c' = 0;  
                         GOTO one;
		       }
               }
  }
 
  LOCAL
    c:            CLOCK(13);  // (u + 1)

}

MODULE System
{
  LOCAL
    // l is the minimal time the automaton has to stay in a state,
    // while u is the maximal time it has to stay.
    l = 9       : CONST;
    u = 12      : CONST;

  // Instances of TwoState template.
  INST automaton1 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton2 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton3 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton4 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton5 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton6 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

}



// Analysis section:
// The module name which should be checked and the type of the internal
// representation for the region of reachable configurations is specified.
REACHABILITY CHECK System
USE BDD
{
  // Declaration of region variable. 
  VAR
    reached: REGION;

  COMMANDS

    // Use On-the-fly-Reachability-Analysis.
    IF( ISREACHABLE FROM INITIALREGION TO FALSE FORWARD )
    {
      PRINT "Error.";
    }
    ELSE
    {
      PRINT "Reachable configurations calculated.";
    }
}