fddi4.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;
                          }
                  }
  }

  LOCAL
    // A clock to measure the time in a state.
    y:           CLOCK(10); // trtt + 1
    z:           CLOCK(10); // 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 = 9:  CONST; // token round trip time .. 2 * #processes + 1

    // Take token signals.
    tt01:        SYNC;
    tt02:        SYNC;
    tt03:        SYNC;
    tt04:        SYNC;

    // Release token signals.
    rt01:        SYNC;
    rt02:        SYNC;
    rt03:        SYNC;
    rt04:        SYNC;

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

  //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;  
			       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;  
			       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;  
			       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;  
			       GOTO ring_04;
			     }
		     }

    STATE ring_04     { TRANS { SYNC ?rt04;  
			       // DO x' = 0;
                               GOTO ring_to_01;
			     }
		     }
  }

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

  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;
  }
}

// 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;
}