fischer5.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;
      pNo5 = 5: 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;
    }

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

REACHABILITY CHECK System
{
  VAR
    initial, error, reached : 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(Process1.Fischer) = critical
                  INTERSECT 
    			    STATE(Process5.Fischer) = critical
			)
	 	UNION 
			(    
			    STATE(Process2.Fischer) = critical
                  INTERSECT 
			    STATE(Process3.Fischer) = critical
			)
	 	UNION 
			(    
			    STATE(Process2.Fischer) = critical
                  INTERSECT 
			    STATE(Process4.Fischer) = critical
			)
	 	UNION 
			(    
			    STATE(Process2.Fischer) = critical
                  INTERSECT 
			    STATE(Process5.Fischer) = critical
			)
	 	UNION 
			(    
			    STATE(Process3.Fischer) = critical
                  INTERSECT 
			    STATE(Process4.Fischer) = critical
			)
	 	UNION 
			(    
			    STATE(Process3.Fischer) = critical
                  INTERSECT 
			    STATE(Process5.Fischer) = critical
			)
	 	UNION 
			(    
			    STATE(Process4.Fischer) = critical
               	  INTERSECT 
			    STATE(Process5.Fischer) = critical
			);

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