fischer4.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;
    pNo3 = 3: CONST;
    pNo4 = 4: CONST;

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

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

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

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

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

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

  COMMANDS
    initial := INITIALREGION;

    error   :=       (    STATE(Process1.Fischer) = critical
                      INTERSECT STATE(Process2.Fischer) = critical)
               UNION (    STATE(Process1.Fischer) = critical
                      INTERSECT STATE(Process3.Fischer) = critical)
               UNION (    STATE(Process1.Fischer) = critical
                      INTERSECT STATE(Process4.Fischer) = critical)
	       UNION (    STATE(Process2.Fischer) = critical
                      INTERSECT STATE(Process3.Fischer) = critical)
	       UNION (    STATE(Process2.Fischer) = critical
                      INTERSECT STATE(Process4.Fischer) = critical)
	       UNION (    STATE(Process3.Fischer) = critical
                      INTERSECT STATE(Process4.Fischer) = critical);

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