fischer128.cta

很好的一本书

    a         AS a;
    b         AS b;
    processNo AS pNo55;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc056 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo56;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc057 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo57;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc058 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo58;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc059 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo59;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc060 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo60;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc061 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo61;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc062 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo62;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc063 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo63;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc064 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo64;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc065 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo65;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc066 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo66;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc067 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo67;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc068 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo68;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc069 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo69;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc070 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo70;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc071 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo71;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc072 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo72;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc073 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo73;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc074 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo74;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc075 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo75;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc076 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo76;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc077 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo77;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc078 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo78;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc079 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo79;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc080 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo80;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc081 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo81;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc082 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo82;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc083 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo83;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc084 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo84;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc085 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo85;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc086 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo86;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc087 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo87;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc088 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo88;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc089 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo89;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc090 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo90;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc091 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo91;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc092 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo92;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc093 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo93;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc094 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo94;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc095 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo95;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc096 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo96;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc097 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo97;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc098 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo98;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc099 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo99;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc100 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo100;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc101 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo101;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc102 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo102;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc103 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo103;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc104 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo104;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc105 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo105;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc106 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo106;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc107 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo107;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc108 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo108;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc109 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo109;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc110 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo110;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc111 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo111;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc112 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo112;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc113 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo113;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc114 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo114;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc115 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo115;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc116 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo116;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc117 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo117;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc118 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo118;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc119 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo119;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc120 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo120;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc121 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo121;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc122 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo122;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc123 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo123;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc124 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo124;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc125 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo125;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc126 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo126;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc127 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo127;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc128 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo128;
    k         AS k;
    critCnt   AS critCnt;
  }

}


// 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 mutual exclusion is violated - this means there are two
    // Fischer processes staying in the critical section at the same time.
    // This region (situation) should not be reachable (possible).
    error := critCnt = 2;

    // The ISREACHABLE command executes an 'on the fly-' reachability check
    // to verify if the specified region 'error' is reachable or not.
    IF( ISREACHABLE FROM INITIALREGION TO error FORWARD ) 
    {
      PRINT "Mutual exclusion violated";
    }
    ELSE 
    {
      PRINT "Mutual exclusion satisfied"; 
    } 
}