fischer96.cta

很好的一本书

  INST Proc41 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo41;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc42 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo42;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc43 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo43;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc44 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo44;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc45 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo45;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc46 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo46;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc47 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo47;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc48 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo48;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc49 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo49;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc50 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo50;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc51 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo51;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc52 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo52;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc53 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo53;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc54 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo54;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc55 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo55;
    k         AS k;
    critCnt   AS critCnt;
  }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  INST Proc96 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo96;
    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"; 
    } 
}