csma16.cta

很好的一本书

                         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 { SYNC #end9;
                                 DO x' = propTime + 1;
                                 GOTO init;
                               }
                         TRANS { SYNC #end10;
                                 DO x' = propTime + 1;
                                 GOTO init;
                               }
                         TRANS { SYNC #end11;
                                 DO x' = propTime + 1;
                                 GOTO init;
                               }
                         TRANS { SYNC #end12;
                                 DO x' = propTime + 1;
                                 GOTO init;
                               }
                         TRANS { SYNC #end13;
                                 DO x' = propTime + 1;
                                 GOTO init;
                               }
                         TRANS { SYNC #end14;
                                 DO x' = propTime + 1;
                                 GOTO init;
                               }
                         TRANS { SYNC #end15;
                                 DO x' = propTime + 1;
                                 GOTO init;
                               }
                         TRANS { SYNC #end16;
                                 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;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin9;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin10;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin11;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin12;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin13;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin14;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin15;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin16;
                                 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;
  }

}

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