csma64.cta

很好的一本书

                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin40;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin41;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin42;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin43;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin44;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin45;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin46;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin47;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin48;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin49;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin50;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin51;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin52;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin53;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin54;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin55;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin56;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin57;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin58;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin59;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin60;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin61;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin62;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin63;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin64;
                                 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;
  }

  INST iSender9 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin9;
    end        AS end9;
    busy       AS busy9;
  }

  INST iSender10 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin10;
    end        AS end10;
    busy       AS busy10;
  }

  INST iSender11 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin11;
    end        AS end11;
    busy       AS busy11;
  }

  INST iSender12 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin12;
    end        AS end12;
    busy       AS busy12;
  }

  INST iSender13 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin13;
    end        AS end13;
    busy       AS busy13;
  }

  INST iSender14 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin14;
    end        AS end14;
    busy       AS busy14;
  }

  INST iSender15 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin15;
    end        AS end15;
    busy       AS busy15;
  }

  INST iSender16 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin16;
    end        AS end16;
    busy       AS busy16;
  }

  INST iSender17 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin17;
    end        AS end17;
    busy       AS busy17;
  }

  INST iSender18 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin18;
    end        AS end18;
    busy       AS busy18;
  }

  INST iSender19 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin19;
    end        AS end19;
    busy       AS busy19;
  }

  INST iSender20 F