fischer128.cta

很好的一本书

/* 
 * project: CTA-model of Fischer's mutual exclusion protocol.
 * modules: Process, System
 * author:  Dirk Beyer, 2000
 * last change: 2001-03-28 mvogel
 * 
 * Based on: Leslie Lamport, "A fast mutual exclusion algorithm.",
 *           ACM Transactions on Computer Systems, 5(1):1-11, 1987.
 */ 

// This module represents the template for a Fischer process.
MODULE Process
{
  // Constants for time bounds.
  INPUT
    // a is the maximal time the modelled assignment k:=1 needs.
    // b is the minimal time the process waits for assignments
    a:          CONST;
    b:          CONST;
    // Parameter for significant value of k.
    processNo:  CONST;

  MULTREST
    // k is the flag for announcement.
    k: DISCRETE;
    // Counter for number of processes staying in critical section.
    critCnt: DISCRETE;

  // Set initial state of automaton and variable values.
  INITIAL   STATE(Fischer) = uncritical AND x >= 2;  

  AUTOMATON Fischer
  {
    STATE uncritical { TRANS { GUARD   k  = 0;  
                               DO   x' = 0;  
			       GOTO assign;
			     }
		     }

    STATE assign     { INV   x <= a;  
		       TRANS { DO   x' = 0 AND k' = processNo;  
			       GOTO wait;
			     }
                     }

    STATE wait       { TRANS { GUARD   x >= b AND k != processNo;  
			       GOTO uncritical;
			     }
                       TRANS { GUARD   x >= b AND k = processNo;  
                               DO   critCnt' = critCnt + 1;  
			       GOTO critical;
			     }
                     }

    STATE critical   { TRANS { DO   k' = 0 AND critCnt' + 1 = critCnt;  
			       GOTO uncritical;
			     }
    }
  }

  LOCAL
    // A clock to measure the time in a state.
    x:  CLOCK(2);
}

MODULE System
{
  LOCAL 
    // a is the maximal time the modelled assignment k:=1 needs.
    // b is the minimal time the process waits for assignments
    a = 1: CONST;
    b = 2: CONST;

    // Process ID's.
    pNo1 = 1: CONST;
    pNo2 = 2: CONST;
    pNo3 = 3: CONST;
    pNo4 = 4: CONST;
    pNo5 = 5: CONST;
    pNo6 = 6: CONST;
    pNo7 = 7: CONST;
    pNo8 = 8: CONST;
    pNo9 = 9: CONST;
    pNo10 = 10: CONST;
    pNo11 = 11: CONST;
    pNo12 = 12: CONST;
    pNo13 = 13: CONST;
    pNo14 = 14: CONST;
    pNo15 = 15: CONST;
    pNo16 = 16: CONST;
    pNo17 = 17: CONST;
    pNo18 = 18: CONST;
    pNo19 = 19: CONST;
    pNo20 = 20: CONST;
    pNo21 = 21: CONST;
    pNo22 = 22: CONST;
    pNo23 = 23: CONST;
    pNo24 = 24: CONST;
    pNo25 = 25: CONST;
    pNo26 = 26: CONST;
    pNo27 = 27: CONST;
    pNo28 = 28: CONST;
    pNo29 = 29: CONST;
    pNo30 = 30: CONST;
    pNo31 = 31: CONST;
    pNo32 = 32: CONST;
    pNo33 = 33: CONST;
    pNo34 = 34: CONST;
    pNo35 = 35: CONST;
    pNo36 = 36: CONST;
    pNo37 = 37: CONST;
    pNo38 = 38: CONST;
    pNo39 = 39: CONST;
    pNo40 = 40: CONST;
    pNo41 = 41: CONST;
    pNo42 = 42: CONST;
    pNo43 = 43: CONST;
    pNo44 = 44: CONST;
    pNo45 = 45: CONST;
    pNo46 = 46: CONST;
    pNo47 = 47: CONST;
    pNo48 = 48: CONST;
    pNo49 = 49: CONST;
    pNo50 = 50: CONST;
    pNo51 = 51: CONST;
    pNo52 = 52: CONST;
    pNo53 = 53: CONST;
    pNo54 = 54: CONST;
    pNo55 = 55: CONST;
    pNo56 = 56: CONST;
    pNo57 = 57: CONST;
    pNo58 = 58: CONST;
    pNo59 = 59: CONST;
    pNo60 = 60: CONST;
    pNo61 = 61: CONST;
    pNo62 = 62: CONST;
    pNo63 = 63: CONST;
    pNo64 = 64: CONST;
    pNo65 = 65: CONST;
    pNo66 = 66: CONST;
    pNo67 = 67: CONST;
    pNo68 = 68: CONST;
    pNo69 = 69: CONST;
    pNo70 = 70: CONST;
    pNo71 = 71: CONST;
    pNo72 = 72: CONST;
    pNo73 = 73: CONST;
    pNo74 = 74: CONST;
    pNo75 = 75: CONST;
    pNo76 = 76: CONST;
    pNo77 = 77: CONST;
    pNo78 = 78: CONST;
    pNo79 = 79: CONST;
    pNo80 = 80: CONST;
    pNo81 = 81: CONST;
    pNo82 = 82: CONST;
    pNo83 = 83: CONST;
    pNo84 = 84: CONST;
    pNo85 = 85: CONST;
    pNo86 = 86: CONST;
    pNo87 = 87: CONST;
    pNo88 = 88: CONST;
    pNo89 = 89: CONST;
    pNo90 = 90: CONST;
    pNo91 = 91: CONST;
    pNo92 = 92: CONST;
    pNo93 = 93: CONST;
    pNo94 = 94: CONST;
    pNo95 = 95: CONST;
    pNo96 = 96: CONST;
    pNo97 = 97: CONST;
    pNo98 = 98: CONST;
    pNo99 = 99: CONST;
    pNo100 = 100: CONST;
    pNo101 = 101: CONST;
    pNo102 = 102: CONST;
    pNo103 = 103: CONST;
    pNo104 = 104: CONST;
    pNo105 = 105: CONST;
    pNo106 = 106: CONST;
    pNo107 = 107: CONST;
    pNo108 = 108: CONST;
    pNo109 = 109: CONST;
    pNo110 = 110: CONST;
    pNo111 = 111: CONST;
    pNo112 = 112: CONST;
    pNo113 = 113: CONST;
    pNo114 = 114: CONST;
    pNo115 = 115: CONST;
    pNo116 = 116: CONST;
    pNo117 = 117: CONST;
    pNo118 = 118: CONST;
    pNo119 = 119: CONST;
    pNo120 = 120: CONST;
    pNo121 = 121: CONST;
    pNo122 = 122: CONST;
    pNo123 = 123: CONST;
    pNo124 = 124: CONST;
    pNo125 = 125: CONST;
    pNo126 = 126: CONST;
    pNo127 = 127: CONST;
    pNo128 = 128: CONST;

  LOCAL                // MULTREST for the submodules.
    k: DISCRETE(129);
    critCnt: DISCRETE(3);
	
  INITIAL k = 0 AND critCnt = 0;  

  // Instances of process template.
  INST Proc001 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo1;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc002 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo2;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc003 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo3;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc004 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo4;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc005 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo5;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc006 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo6;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc007 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo7;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc008 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo8;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc009 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo9;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc010 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo10;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc011 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo11;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc012 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo12;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc013 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo13;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc014 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo14;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc015 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo15;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc016 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo16;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc017 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo17;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc018 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo18;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc019 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo19;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc020 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo20;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc021 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo21;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc022 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo22;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc023 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo23;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc024 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo24;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc025 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo25;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc026 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo26;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc027 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo27;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc028 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo28;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc029 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo29;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc030 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo30;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc031 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo31;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc032 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo32;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc033 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo33;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc034 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo34;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc035 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo35;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc036 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo36;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc037 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo37;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc038 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo38;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc039 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo39;
    k         AS k;
    critCnt   AS critCnt;
  }

  INST Proc040 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo40;
    k         AS k;
    critCnt   AS critCnt;
  }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  INST Proc055 FROM Process WITH
  {