fischer96.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;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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