csma64.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 <= propTime + 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;

    // 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;
    end13          : SYNC;
    end14          : SYNC;
    end15          : SYNC;
    end16          : SYNC;
    end17          : SYNC;
    end18          : SYNC;
    end19          : SYNC;
    end20          : SYNC;
    end21          : SYNC;
    end22          : SYNC;
    end23          : SYNC;
    end24          : SYNC;
    end25          : SYNC;
    end26          : SYNC;
    end27          : SYNC;
    end28          : SYNC;
    end29          : SYNC;
    end30          : SYNC;
    end31          : SYNC;
    end32          : SYNC;
    end33          : SYNC;
    end34          : SYNC;
    end35          : SYNC;
    end36          : SYNC;
    end37          : SYNC;
    end38          : SYNC;
    end39          : SYNC;
    end40          : SYNC;
    end41          : SYNC;
    end42          : SYNC;
    end43          : SYNC;
    end44          : SYNC;
    end45          : SYNC;
    end46          : SYNC;
    end47          : SYNC;
    end48          : SYNC;
    end49          : SYNC;
    end50          : SYNC;
    end51          : SYNC;
    end52          : SYNC;
    end53          : SYNC;
    end54          : SYNC;
    end55          : SYNC;
    end56          : SYNC;
    end57          : SYNC;
    end58          : SYNC;
    end59          : SYNC;
    end60          : SYNC;
    end61          : SYNC;
    end62          : SYNC;
    end63          : SYNC;
    end64          : SYNC;

    // Busy signals for every Sender.
    busy1         : SYNC;
    busy2         : SYNC;
    busy3         : SYNC;
    busy4         : SYNC;
    busy5         : SYNC;
    busy6         : SYNC;
    busy7         : SYNC;
    busy8         : SYNC;
    busy9         : SYNC;
    busy10         : SYNC;
    busy11         : SYNC;
    busy12         : SYNC;
    busy13         : SYNC;
    busy14         : SYNC;
    busy15         : SYNC;
    busy16         : SYNC;
    busy17         : SYNC;
    busy18         : SYNC;
    busy19         : SYNC;
    busy20         : SYNC;
    busy21         : SYNC;
    busy22         : SYNC;
    busy23         : SYNC;
    busy24         : SYNC;
    busy25         : SYNC;
    busy26         : SYNC;
    busy27         : SYNC;
    busy28         : SYNC;
    busy29         : SYNC;
    busy30         : SYNC;
    busy31         : SYNC;
    busy32         : SYNC;
    busy33         : SYNC;
    busy34         : SYNC;
    busy35         : SYNC;
    busy36         : SYNC;
    busy37         : SYNC;
    busy38         : SYNC;
    busy39         : SYNC;
    busy40         : SYNC;
    busy41         : SYNC;
    busy42         : SYNC;
    busy43         : SYNC;
    busy44         : SYNC;
    busy45         : SYNC;
    busy46         : SYNC;
    busy47         : SYNC;
    busy48         : SYNC;
    busy49         : SYNC;
    busy50         : SYNC;
    busy51         : SYNC;
    busy52         : SYNC;
    busy53         : SYNC;
    busy54         : SYNC;
    busy55         : SYNC;
    busy56         : SYNC;
    busy57         : SYNC;
    busy58         : SYNC;
    busy59         : SYNC;
    busy60         : SYNC;
    busy61         : SYNC;
    busy62         : SYNC;
    busy63         : SYNC;
    busy64         : SYNC;

  INITIAL STATE(Medium)= init AND x = propTime + 1;

  AUTOMATON Medium
  {
    STATE init         { INV FALSE;
                         TRANS { SYNC #begin1;
                                 DO x' = 0;
                                 GOTO transmit;
                               }
                         TRANS { SYNC #begin2;
                                 DO x' = 0;
                                 GOTO transmit;
                               }
                         TRANS { SYNC #begin3;
                                 DO x' = 0;
                                 GOTO transmit;
                               }
                         TRANS { SYNC #begin4;
                                 DO x' = 0;
                                 GOTO transmit;
                               }
                         TRANS { SYNC #begin5;
                                 DO x' = 0;
                                 GOTO transmit;
                               }
                         TRANS { SYNC #begin6;
                                 DO x' = 0;
                                 GOTO transmit;
                               }
                         TRANS { SYNC #begin7;
                                 DO x' = 0;
                                 GOTO transmit;
                               }
                         TRANS { SYNC #begin8;
                                 DO x' = 0;
                                 GOTO transmit;
                               }
                         TRANS { SYNC #begin9;
                                 DO x' = 0;
                                 GOTO transmit;
                               }