fischer2.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
    // initiated from other processes.
    a:          CONST;
    b:          CONST;
    // Parameter for significant value of k.
    processNo:  CONST;

  MULTREST
    // k is the flag for announcement.
    k:  DISCRETE;

  LOCAL
    // A clock to measure the time in a state.
    x:  ANALOG;

  INITIAL STATE(Fischer) = uncritical AND k = 0;  

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

    STATE assign     { INV x <= a;  
                       DERIV DER(x) = 1;
                       TRANS { DO x' = 0 AND k' = processNo;  
                               GOTO wait;
                             }
                     }

    STATE wait       { DERIV DER(x) = 1;
                       TRANS { GUARD x >= b AND k != processNo;
                               DO x' = 0;
			       GOTO uncritical;			 
			     }
                       TRANS { GUARD x > b AND k = processNo;
                               DO x' = 0;
                               GOTO critical;
                             }
                     }

    STATE critical   { TRANS { DO k' = 0 AND x' = 0;  
			       GOTO uncritical;
                             }
                     }
  }
}

MODULE System
{
  LOCAL
    a = 3 : CONST;
    b = 3 : CONST;

    pNo1 = 1: CONST;
    pNo2 = 2: CONST;

  LOCAL // MULTREST for the submodules.
    k:     DISCRETE;

  INST Proc1 FROM Process WITH
  {
    a         AS a;
    b         AS b;
    processNo AS pNo1;
    k         AS k;
  }

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

REACHABILITY CHECK System
USE DDM
{
  VAR
    initial, error: REGION;

  COMMANDS

    initial :=  INITIALREGION;

    error   :=  STATE(Proc1.Fischer) = critical
      INTERSECT STATE(Proc2.Fischer) = critical;

    IF( ISREACHABLE FROM initial TO error FORWARD ) 
    {
      PRINT "Mutual exclusion violated.";
    }
    ELSE 
    {
      PRINT "Mutual exclusion satisfied."; 
    } 
}