Murphi Syntax

Here we will describe the syntax used in the system description language, Murphi-- (so called since it is a subset of Murphi). At its core, the description language is just a list of guarded commands.

Each command has a guard expression and an action statemment. If in a given state, the guard evaluates to true, then the statement is said to be enabled. To compute the next state of the system, we will first find all the guarded commands that are enabled. Then one of the enabled rules is chosen non-deterministically and it's action executed to compute the next state.

The language itself is quite simple. We will describe all the different elements of the syntax with an example. For that we will consider the PetersonMutualExclusion protocol.

;;; Peterson's Algorithm for Mutual Exclusion.

(murphi-program

 ;; State Variables
 (global-state (s bool)
	       (y1 bool)
	       (y2 bool)
	       (pc1 rat)
	       (pc2 rat))
 ;; Initialization
 (initialize
  (progn
    (setq s false)
    (setq y1 false)
    (setq y2 false)
    (setq pc1 1)
    (setq pc2 1)))

 ;; Rules for process 1...
 (rules
  (==> (= pc1 1)                             ;Req_1
       (progn
         (setq y1 true)
	 (setq s true)
	 (setq pc1 2)))
  (==> (and (= pc1 2))                       ;In_1
       (ite (or (not y2) (not s))
            (setq pc1 3)
            (skip)))
  (==> (= pc1 3)                             ;Out_1
       (progn
	 (setq y1 false)
	 (setq pc1 1))))

 ;; Rules for process 2...
 (rules
  (==> (= pc2 1)                             ;Req_2
       (progn
	 (setq y2 true)
	 (setq s false)
	 (setq pc2 2)))
  (==> (and (= pc2 2) (or (not y1) s))       ;In_2
       (setq pc2 3))
  (==> (= pc2 3)                             ;Out_2
       (progn
	 (setq y2 false)
	 (setq pc2 1))))

 ;; Mutual Exclusion property
 (invariant
  (not (and (= pc1 3) (= pc2 3))))

 ;; Abstraction
 (abstraction
  ;; Initial predicates...
  (B0 (= pc1 3))
  (B1 (= pc2 3))

  ;; Iteration 1
  (C01 (= PC2 2))

  ;; Iteration 2
  (C02 (= PC1 2))

  ;; Iteration 3
  (C03 (NOT (= Y1 TRUE)))
  (C04 (= Y2 Y1))

  ;; Iteration 4
  (C05 (NOT (= S TRUE)))))

Then the initialize declaration is used to compute the initial state of the system. any arbitrary statement can appear in it. The statement syntax will be described when we get to guarded commands.

The rules declaration is used to describe the guarded commands. Each of the rules declaration contains a list of guarded commands. Any number of this declaration is allowed. For instance we have two sets of rules in this example. The semantics is to combine all the rules into one list and the actions to execute is chosen non-deterministically from this list. Each of the individual rules is a list of three things. The first is the token ==>, which is just syntactic sugar. The second element is the guard which is a boolean expression over the state variables. It is written in prefix notation and all the usual boolean connectives like and, or, not, forall and exists, the arithmetic operators of +, -, *, >, < etc are available. The last element in the list is the action statement. The operators allowed in the statement in addition to the expression operators above are:

• (progn stmt_1 stmt_2 ... stmt_n ) :: This denotes a sequence of statements that are executed one after another.
• (ite IF-EXPR THEN-STMT ELSE-STMT ) :: This denotes a conditional statement. If the IF-EXPR is true then the statement THEN-STMT is executed, otherwise ELSE-STMT is executed. The statements themselves can be as compound statements. In the ex
• (skip) :: This denotes a nop statement. Nothing changes as a result of executing this. This is combination with the ite statement can be used to write one sided conditionals, like the when and unless operators of Common Lisp.
• (setq VAR EXPR ) :: This denotes an assignment statement. VAR can be an atom in which case the variable is assigned. It can also be an aref expression in which case only one of the elements in the array will be modified. EXPR can be an arbitrary expression.

The invariant declaration is used to describe the safety invariant that is to be proved. It can be an arbitrary expression over the state variable of boolean type.

The abstraction block is used to specify the abstraction predicates. Each predicate is defined by a symbolic name. This name is used in the abstract system that is generated. The boolean expression is the actual predicate. For instance in the above example, B0 is the symbolic name of the predicate (= pc1 3).