fischer64.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:=a 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;

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

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

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


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