csma32.cta

很好的一本书

                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin29;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin30;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin31;
                                 DO x' = 0;
                                 GOTO collDetected;
                               }
                         TRANS { GUARD x + 1 <= propTime;
                                 SYNC #begin32;
                                 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 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin20;
    end        AS end20;
    busy       AS busy20;
  }

  INST iSender21 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin21;
    end        AS end21;
    busy       AS busy21;
  }

  INST iSender22 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin22;
    end        AS end22;
    busy       AS busy22;
  }

  INST iSender23 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin23;
    end        AS end23;
    busy       AS busy23;
  }

  INST iSender24 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin24;
    end        AS end24;
    busy       AS busy24;
  }

  INST iSender25 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin25;
    end        AS end25;
    busy       AS busy25;
  }

  INST iSender26 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin26;
    end        AS end26;
    busy       AS busy26;
  }

  INST iSender27 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin27;
    end        AS end27;
    busy       AS busy27;
  }

  INST iSender28 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin28;
    end        AS end28;
    busy       AS busy28;
  }

  INST iSender29 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin29;
    end        AS end29;
    busy       AS busy29;
  }

  INST iSender30 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin30;
    end        AS end30;
    busy       AS busy30;
  }

  INST iSender31 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin31;
    end        AS end31;
    busy       AS busy31;
  }

  INST iSender32 FROM Sender WITH
  {
    propTime   AS propTime;
    transmTime AS transmTime;
    collDetect AS collDetect;
    begin      AS begin32;
    end        AS end32;
    busy       AS busy32;
  }

}

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