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

  LOCAL                // MULTREST for the submodules.
    k: DISCRETE(9);
    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;
  }
}


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