csma256.cta

很好的一本书

/*
 * File: CTA-model of Carrier Sense Multiple Access Collision Detect
 *       Protocol (CSMA/CD).
 * modules: Sender, Medium
 * author:  Dirk Beyer, 2002
 * last change: mvogel 2002-03-18
 * 
 * Based on: "A case study: the CSMA/CD protocol", Sergio Yovine,
 *           VERIMAG-SPECTRE, November 18, 1994
 */ 

// This module represents the template for one sender.
MODULE Sender
{
  INPUT
    propTime   : CONST; // time for signal propagation. (paper: Sigma)
    transmTime : CONST; // time for data transmission. (paper: Lambda)

    collDetect : SYNC;  // Collision detection by medium.

  MULTREST
    // Senders syncronisation events.
    begin      : SYNC; // Begin of data transmitting
    end        : SYNC; // End of data transmitting
    busy       : SYNC; // Busy signaling by medium.

  // Set initial state of automaton and clock values.
  INITIAL STATE(Sender) = init AND x = transmTime + 1;

  AUTOMATON Sender
  {
    STATE init         { TRANS { SYNC ?collDetect;
                                 DO x' = x;
                                 GOTO init;
                               }
                         TRANS { DO x' = x;
                                 GOTO send;
                               }
                       }

    STATE send         { INV FALSE;
                         TRANS { SYNC #begin;
                                 DO x' = 0;
                                 GOTO transmit;
                               }
                         TRANS { SYNC #busy;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { SYNC ?collDetect;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                       }

    STATE collDetected { INV x <= 2 * propTime;
                         TRANS { SYNC ?collDetect;
                                 DO x' = x;
                                 GOTO collDetected;
                               }
                         TRANS { DO x' = transmTime + 1;
                                 GOTO send;
                               }
                       }

    STATE transmit     { INV x <= transmTime;
                         TRANS { SYNC ?collDetect;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x = transmTime;
                                 SYNC #end;
                                 DO x' = transmTime + 1;
                                 GOTO init;
                               }
                       }
  }

  LOCAL
    // A clock to measure the time in a state.
    x:  CLOCK(5);  // transmTime + 1
}

// Module of the whole system.
MODULE System
{
  LOCAL
    // Constants for time bounds.
    propTime = 1   : CONST; // time for signal propagation. (paper: Sigma)
    transmTime = 4 : CONST; // time for data transmission. (paper: Lambda)

    collDetect     : SYNC;  // Collision detect signal. (Same signal for all)

    // Begin signals for every Sender.
    begin1        : SYNC;
    begin2        : SYNC;
    begin3        : SYNC;
    begin4        : SYNC;
    begin5        : SYNC;
    begin6        : SYNC;
    begin7        : SYNC;
    begin8        : SYNC;
    begin9        : SYNC;
    begin10        : SYNC;
    begin11        : SYNC;
    begin12        : SYNC;
    begin13        : SYNC;
    begin14        : SYNC;
    begin15        : SYNC;
    begin16        : SYNC;
    begin17        : SYNC;
    begin18        : SYNC;
    begin19        : SYNC;
    begin20        : SYNC;
    begin21        : SYNC;
    begin22        : SYNC;
    begin23        : SYNC;
    begin24        : SYNC;
    begin25        : SYNC;
    begin26        : SYNC;
    begin27        : SYNC;
    begin28        : SYNC;
    begin29        : SYNC;
    begin30        : SYNC;
    begin31        : SYNC;
    begin32        : SYNC;
    begin33        : SYNC;
    begin34        : SYNC;
    begin35        : SYNC;
    begin36        : SYNC;
    begin37        : SYNC;
    begin38        : SYNC;
    begin39        : SYNC;
    begin40        : SYNC;
    begin41        : SYNC;
    begin42        : SYNC;
    begin43        : SYNC;
    begin44        : SYNC;
    begin45        : SYNC;
    begin46        : SYNC;
    begin47        : SYNC;
    begin48        : SYNC;
    begin49        : SYNC;
    begin50        : SYNC;
    begin51        : SYNC;
    begin52        : SYNC;
    begin53        : SYNC;
    begin54        : SYNC;
    begin55        : SYNC;
    begin56        : SYNC;
    begin57        : SYNC;
    begin58        : SYNC;
    begin59        : SYNC;
    begin60        : SYNC;
    begin61        : SYNC;
    begin62        : SYNC;
    begin63        : SYNC;
    begin64        : SYNC;
    begin65        : SYNC;
    begin66        : SYNC;
    begin67        : SYNC;
    begin68        : SYNC;
    begin69        : SYNC;
    begin70        : SYNC;
    begin71        : SYNC;
    begin72        : SYNC;
    begin73        : SYNC;
    begin74        : SYNC;
    begin75        : SYNC;
    begin76        : SYNC;
    begin77        : SYNC;
    begin78        : SYNC;
    begin79        : SYNC;
    begin80        : SYNC;
    begin81        : SYNC;
    begin82        : SYNC;
    begin83        : SYNC;
    begin84        : SYNC;
    begin85        : SYNC;
    begin86        : SYNC;
    begin87        : SYNC;
    begin88        : SYNC;
    begin89        : SYNC;
    begin90        : SYNC;
    begin91        : SYNC;
    begin92        : SYNC;
    begin93        : SYNC;
    begin94        : SYNC;
    begin95        : SYNC;
    begin96        : SYNC;
    begin97        : SYNC;
    begin98        : SYNC;
    begin99        : SYNC;
    begin100        : SYNC;
    begin101        : SYNC;
    begin102        : SYNC;
    begin103        : SYNC;
    begin104        : SYNC;
    begin105        : SYNC;
    begin106        : SYNC;
    begin107        : SYNC;
    begin108        : SYNC;
    begin109        : SYNC;
    begin110        : SYNC;
    begin111        : SYNC;
    begin112        : SYNC;
    begin113        : SYNC;
    begin114        : SYNC;
    begin115        : SYNC;
    begin116        : SYNC;
    begin117        : SYNC;
    begin118        : SYNC;
    begin119        : SYNC;
    begin120        : SYNC;
    begin121        : SYNC;
    begin122        : SYNC;
    begin123        : SYNC;
    begin124        : SYNC;
    begin125        : SYNC;
    begin126        : SYNC;
    begin127        : SYNC;
    begin128        : SYNC;
    begin129        : SYNC;
    begin130        : SYNC;
    begin131        : SYNC;
    begin132        : SYNC;
    begin133        : SYNC;
    begin134        : SYNC;
    begin135        : SYNC;
    begin136        : SYNC;
    begin137        : SYNC;
    begin138        : SYNC;
    begin139        : SYNC;
    begin140        : SYNC;
    begin141        : SYNC;
    begin142        : SYNC;
    begin143        : SYNC;
    begin144        : SYNC;
    begin145        : SYNC;
    begin146        : SYNC;
    begin147        : SYNC;
    begin148        : SYNC;
    begin149        : SYNC;
    begin150        : SYNC;
    begin151        : SYNC;
    begin152        : SYNC;
    begin153        : SYNC;
    begin154        : SYNC;
    begin155        : SYNC;
    begin156        : SYNC;
    begin157        : SYNC;
    begin158        : SYNC;
    begin159        : SYNC;
    begin160        : SYNC;
    begin161        : SYNC;
    begin162        : SYNC;
    begin163        : SYNC;
    begin164        : SYNC;
    begin165        : SYNC;
    begin166        : SYNC;
    begin167        : SYNC;
    begin168        : SYNC;
    begin169        : SYNC;
    begin170        : SYNC;
    begin171        : SYNC;
    begin172        : SYNC;
    begin173        : SYNC;
    begin174        : SYNC;
    begin175        : SYNC;
    begin176        : SYNC;
    begin177        : SYNC;
    begin178        : SYNC;
    begin179        : SYNC;
    begin180        : SYNC;
    begin181        : SYNC;
    begin182        : SYNC;
    begin183        : SYNC;
    begin184        : SYNC;
    begin185        : SYNC;
    begin186        : SYNC;
    begin187        : SYNC;
    begin188        : SYNC;
    begin189        : SYNC;
    begin190        : SYNC;
    begin191        : SYNC;
    begin192        : SYNC;
    begin193        : SYNC;
    begin194        : SYNC;
    begin195        : SYNC;
    begin196        : SYNC;
    begin197        : SYNC;
    begin198        : SYNC;
    begin199        : SYNC;
    begin200        : SYNC;
    begin201        : SYNC;
    begin202        : SYNC;
    begin203        : SYNC;
    begin204        : SYNC;
    begin205        : SYNC;
    begin206        : SYNC;
    begin207        : SYNC;
    begin208        : SYNC;
    begin209        : SYNC;
    begin210        : SYNC;
    begin211        : SYNC;
    begin212        : SYNC;
    begin213        : SYNC;
    begin214        : SYNC;
    begin215        : SYNC;
    begin216        : SYNC;
    begin217        : SYNC;
    begin218        : SYNC;
    begin219        : SYNC;
    begin220        : SYNC;
    begin221        : SYNC;
    begin222        : SYNC;
    begin223        : SYNC;
    begin224        : SYNC;
    begin225        : SYNC;
    begin226        : SYNC;
    begin227        : SYNC;
    begin228        : SYNC;
    begin229        : SYNC;
    begin230        : SYNC;
    begin231        : SYNC;
    begin232        : SYNC;
    begin233        : SYNC;
    begin234        : SYNC;
    begin235        : SYNC;
    begin236        : SYNC;
    begin237        : SYNC;
    begin238        : SYNC;
    begin239        : SYNC;
    begin240        : SYNC;
    begin241        : SYNC;
    begin242        : SYNC;
    begin243        : SYNC;
    begin244        : SYNC;
    begin245        : SYNC;
    begin246        : SYNC;
    begin247        : SYNC;
    begin248        : SYNC;
    begin249        : SYNC;
    begin250        : SYNC;
    begin251        : SYNC;
    begin252        : SYNC;
    begin253        : SYNC;
    begin254        : SYNC;
    begin255        : SYNC;
    begin256        : SYNC;

    // End signals fro every Sender.
    end1          : SYNC;
    end2          : SYNC;
    end3          : SYNC;
    end4          : SYNC;
    end5          : SYNC;
    end6          : SYNC;
    end7          : SYNC;
    end8          : SYNC;
    end9          : SYNC;
    end10          : SYNC;
    end11          : SYNC;
    end12          : SYNC;