fddi12.cta

很好的一本书

/* 
 * File: CTA-model of Token Ring FDDI Protocol.
 * modules: Station, System
 * author:  Dirk Beyer, 2002
 * last change: mvogel 2002-03-12
 * 
 */ 

// This module represents the template for one station.
MODULE Station
{
  INPUT
    // sa:   number of time units for high-speed communication.
    // trtt: number of time units for asynchronous token passing.
    sa:          CONST;
    trtt:        CONST;

    // Signal for take token.
    tt:          SYNC;

  OUTPUT
    // Signal for token release.
    rt:          SYNC;

  // Set initial state of automaton and variable values.
  INITIAL STATE(Station) = z_idle AND y = trtt + 1 AND z = trtt + 1;

  AUTOMATON Station
  {
    STATE z_idle  { TRANS { SYNC ?tt;  
                            DO y' = 0;  
			    GOTO z_sync;
			  }
		  }

    STATE z_sync  { INV y <= sa;
                    TRANS { GUARD y >= sa AND z + 1 <= trtt;
                            //DO y' = trtt + 1;
                            GOTO z_async;
                          }
                    TRANS { GUARD y >= sa AND z >= trtt;
                            SYNC !rt;
                            DO z' = trtt + 1;
                            GOTO y_idle;
                          }
                  }

    STATE z_async { INV z <= trtt;
                    TRANS { SYNC !rt;
                            DO z' = trtt + 1;
                            GOTO y_idle;
                          }
                  }

    STATE y_idle  { TRANS { SYNC ?tt;  
                            DO z' = 0;  
			    GOTO y_sync;
			  }
		  }

    STATE y_sync  { INV z <= sa;
                    TRANS { GUARD z >= sa AND y + 1 <= trtt;
		            //DO z' = trtt + 1;
                            GOTO y_async;
                          }
                    TRANS { GUARD z >= sa AND y >= trtt;
                            SYNC !rt;
                            DO y' = trtt + 1;
                            GOTO z_idle;
                          }
                  }

    STATE y_async { INV y <= trtt;
                    TRANS { SYNC !rt;
                            DO y' = trtt + 1; 
                            GOTO z_idle;
                          }
                  }
  }

  // Clocks to measure the time since last take token.
  LOCAL
    y:           CLOCK(26); // trtt + 1
    z:           CLOCK(26); // trtt + 1
}

// Module of the whole system.
MODULE System
{
  LOCAL
    // Constants for time bounds.
    //  td = 0:    CONST; // number of time units for the token ring delay.
    sa = 1:    CONST; // number of time units for high-speed communication.
    trtt = 25: CONST; // token round trip time .. 2 * #processes + 1

    // Take token signals.
    tt01:        SYNC;
    tt02:        SYNC;
    tt03:        SYNC;
    tt04:        SYNC;
    tt05:        SYNC;
    tt06:        SYNC;
    tt07:        SYNC;
    tt08:        SYNC;
    tt09:        SYNC;
    tt10:        SYNC;
    tt11:        SYNC;
    tt12:        SYNC;

    // Release token signals.
    rt01:        SYNC;
    rt02:        SYNC;
    rt03:        SYNC;
    rt04:        SYNC;
    rt05:        SYNC;
    rt06:        SYNC;
    rt07:        SYNC;
    rt08:        SYNC;
    rt09:        SYNC;
    rt10:        SYNC;
    rt11:        SYNC;
    rt12:        SYNC;

  // Instances of process template.
  INST iStation01 FROM Station WITH
  {
    sa        AS sa;
    trtt      AS trtt;
    tt        AS tt01;
    rt        AS rt01;
  }

  INST iStation02 FROM Station WITH
  {
    sa        AS sa;
    trtt      AS trtt;
    tt        AS tt02;
    rt        AS rt02;
  }

  //LOCAL
  //  x:         CLOCK(1); // Clock for token delay.

  INITIAL STATE(Ring)= ring_to_01;// AND x = 1;
 
  AUTOMATON Ring
  {
    STATE ring_to_01 { INV FALSE;
                       TRANS { SYNC !tt01;
                               // DO x' = 1;  
			       GOTO ring_01;
			     }
		     }

    STATE ring_01    { TRANS { SYNC ?rt01;  
			       // DO x' = 0;
                               GOTO ring_to_02;
			     }
		     }

    STATE ring_to_02 { INV FALSE;
                       TRANS { SYNC !tt02; // DO x' = 1;   
			       GOTO ring_02;
			     }
		     }

    STATE ring_02    { TRANS { SYNC ?rt02;  
			       // DO x' = 0;
                               GOTO ring_to_03;
			     }
		     }
 
    STATE ring_to_03 { INV FALSE;
                       TRANS { SYNC !tt03; // DO x' = 1;   
			       GOTO ring_03;
			     }
		     }

    STATE ring_03    { TRANS { SYNC ?rt03;  
			       // DO x' = 0;
                               GOTO ring_to_04;
			     }
		     }

    STATE ring_to_04 { INV FALSE;
                       TRANS { SYNC !tt04; // DO x' = 1;   
			       GOTO ring_04;
			     }
		     }

    STATE ring_04    { TRANS { SYNC ?rt04;  
			       // DO x' = 0;
                               GOTO ring_to_05;
			     }
		     }
   
    STATE ring_to_05 { INV FALSE;
                       TRANS { SYNC !tt05;  // DO x' = 1;  
			       GOTO ring_05;
			     }
		     }

    STATE ring_05    { TRANS { SYNC ?rt05;  
			       // DO x' = 0;
                               GOTO ring_to_06;
			     }
		     }

    STATE ring_to_06 { INV FALSE;
                       TRANS { SYNC !tt06;// DO x' = 1;    
			       GOTO ring_06;
			     }
		     }

    STATE ring_06    { TRANS { SYNC ?rt06;  
			       // DO x' = 0;
                               GOTO ring_to_07;
			     }
		     }
 
    STATE ring_to_07 { INV FALSE;
                       TRANS { SYNC !tt07;  // DO x' = 1;  
			       GOTO ring_07;
			     }
		     }

    STATE ring_07    { TRANS { SYNC ?rt07;  
			       // DO x' = 0;
                               GOTO ring_to_08;
			     }
		     }

    STATE ring_to_08 { INV FALSE;
                       TRANS { SYNC !tt08;  // DO x' = 1;  
			       GOTO ring_08;
			     }
		     }

    STATE ring_08    { TRANS { SYNC ?rt08;  
			       // DO x' = 0;
                               GOTO ring_to_09;
			     }
		     }

    STATE ring_to_09 { INV FALSE;
                       TRANS { SYNC !tt09;  // DO x' = 1;  
			       GOTO ring_09;
			     }
		     }

    STATE ring_09    { TRANS { SYNC ?rt09;  
			       // DO x' = 0;
                               GOTO ring_to_10;
			     }
		     }

    STATE ring_to_10 { INV FALSE;
                       TRANS { SYNC !tt10;  // DO x' = 1;  
			       GOTO ring_10;
			     }
		     }

    STATE ring_10    { TRANS { SYNC ?rt10;  
			       // DO x' = 0;
                               GOTO ring_to_11;
			     }
		     }
 
    STATE ring_to_11 { INV FALSE;
                       TRANS { SYNC !tt11; // DO x' = 1;   
			       GOTO ring_11;
			     }
		     }

    STATE ring_11    { TRANS { SYNC ?rt11;  
			       // DO x' = 0;
                               GOTO ring_to_12;
			     }
		     }

    STATE ring_to_12 { INV FALSE;
                       TRANS { SYNC !tt12; // DO x' = 1;   
			       GOTO ring_12;
			     }
		     }

    STATE ring_12    { TRANS { SYNC ?rt12;  
			       // DO x' = 0;
                               GOTO ring_to_01;
			     }
		     }
  }

  INST iStation03 FROM Station WITH
  {
    sa        AS sa;
    trtt      AS trtt;
    tt        AS tt03;
    rt        AS rt03;
  }

  INST iStation04 FROM Station WITH
  {
    sa        AS sa;
    trtt      AS trtt;
    tt        AS tt04;
    rt        AS rt04;
  }

  INST iStation05 FROM Station WITH
  {
    sa        AS sa;
    trtt      AS trtt;
    tt        AS tt05;
    rt        AS rt05;
  }

  INST iStation06 FROM Station WITH
  {
    sa        AS sa;
    trtt      AS trtt;
    tt        AS tt06;
    rt        AS rt06;
  }

  INST iStation07 FROM Station WITH
  {
    sa        AS sa;
    trtt      AS trtt;
    tt        AS tt07;
    rt        AS rt07;
  }

  INST iStation08 FROM Station WITH
  {
    sa        AS sa;
    trtt      AS trtt;
    tt        AS tt08;
    rt        AS rt08;
  }

  INST iStation09 FROM Station WITH
  {
    sa        AS sa;
    trtt      AS trtt;
    tt        AS tt09;
    rt        AS rt09;
  }

  INST iStation10 FROM Station WITH
  {
    sa        AS sa;
    trtt      AS trtt;
    tt        AS tt10;
    rt        AS rt10;
  }

  INST iStation11 FROM Station WITH
  {
    sa        AS sa;
    trtt      AS trtt;
    tt        AS tt11;
    rt        AS rt11;
  }

  INST iStation12 FROM Station WITH
  {
    sa        AS sa;
    trtt      AS trtt;
    tt        AS tt12;
    rt        AS rt12;
  }
}

// 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 variables. 
  VAR
    reached, error : REGION;

  COMMANDS

    // Define an error region. If this region is reachable from the initial
    // region the ... is violated
    //error := 

    reached := REACH FROM INITIALREGION FORWARD;
}