csma8.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;

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

    // Busy signals for every Sender.
    busy1         : SYNC;
    busy2         : SYNC;
    busy3         : SYNC;
    busy4         : SYNC;
    busy5         : SYNC;
    busy6         : SYNC;
    busy7         : SYNC;
    busy8         : 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;
                               }
                       }

    STATE transmit     {
                         TRANS { GUARD x >= propTime;
                                 SYNC #busy1;
                                 DO x' = propTime + 1;
                                 GOTO transmit;
                               }
                         TRANS { GUARD x >= propTime;
                                 SYNC #busy2;
                                 DO x' = propTime + 1;
                                 GOTO transmit;
                               }
                         TRANS { GUARD x >= propTime;
                                 SYNC #busy3;
                                 DO x' = propTime + 1;
                                 GOTO transmit;
                               }
                         TRANS { GUARD x >= propTime;
                                 SYNC #busy4;
                                 DO x' = propTime + 1;
                                 GOTO transmit;
                               }
                         TRANS { GUARD x >= propTime;
                                 SYNC #busy5;
                                 DO x' = propTime + 1;
                                 GOTO transmit;
                               }
                         TRANS { GUARD x >= propTime;
                                 SYNC #busy6;
                                 DO x' = propTime + 1;
                                 GOTO transmit;
                               }
                         TRANS { GUARD x >= propTime;
                                 SYNC #busy7;
                                 DO x' = propTime + 1;
                                 GOTO transmit;
                               }
                         TRANS { GUARD x >= propTime;
                                 SYNC #busy8;
                                 DO x' = propTime + 1;
                                 GOTO transmit;
                               }

                         TRANS { SYNC #end1;
                                 DO x' = propTime + 1;
                                 GOTO init;
                               }
                         TRANS { SYNC #end2;
                                 DO x' = propTime + 1;
                                 GOTO init;
                               }
                         TRANS { SYNC #end3;
                                 DO x' = propTime + 1;
                                 GOTO init;
                               }
                         TRANS { SYNC #end4;
                                 DO x' = propTime + 1;
                                 GOTO init;
                               }
                         TRANS { SYNC #end5;
                                 DO x' = propTime + 1;
                                 GOTO init;
                               }
                         TRANS { SYNC #end6;
                                 DO x' = propTime + 1;
                                 GOTO init;
                               }
                         TRANS { SYNC #end7;
                                 DO x' = propTime + 1;
                                 GOTO init;
                               }
                         TRANS { SYNC #end8;
                                 DO x' = propTime + 1;
                                 GOTO init;
                               }

                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin1;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin2;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin3;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin4;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin5;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin6;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin7;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin8;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                       }

    STATE collDetected { INV x <= propTime;
                         TRANS { SYNC !collDetect;
                                 DO x' = propTime + 1;
                                 GOTO init;
                               }
                       }
  }

  LOCAL
    x:         CLOCK(2); // propTime + 1

  // Instances of Sender template.
  INST iSender1 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin1;
    end        AS end1;
    busy       AS busy1;
  }

  INST iSender2 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin2;
    end        AS end2;
    busy       AS busy2;
  }

  INST iSender3 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin3;
    end        AS end3;
    busy       AS busy3;
  }

  INST iSender4 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin4;
    end        AS end4;
    busy       AS busy4;
  }

  INST iSender5 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin5;
    end        AS end5;
    busy       AS busy5;
  }

  INST iSender6 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin6;
    end        AS end6;
    busy       AS busy6;
  }

  INST iSender7 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin7;
    end        AS end7;
    busy       AS busy7;
  }

  INST iSender8 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin8;
    end        AS end8;
    busy       AS busy8;
  }

}

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