Introduction to Murphi3.1 - II

This is the continuation of previous post which provides an basic introduction to Murphi3.1.

Defining Rulesets

Rulesets defines the flow of the systems defined by the finite state machine, (I will discuss on another post in detail about automata and finite state machines). Also ruleset can be used to provide communication using functions.

ruleset <val>: <Values>do
			rule "<name of rule>"
				preconditions
			==>
				change in states
				function calls
endruleset;

The preconditions can contain single or multiple condition combined using and (&) , or (|).

The change in states, will provide the change of variables

The function calls, will provide communication between other components. (this can be optional)

Defining StartState

Defines the start state of system, probably contains the initial values for the all the global variables. sample statestate definition can be

startstate
	<variable_name> : <initial_value>
	or
	undefined: <varibale_name>
endstartstate

Defining Invariants

Invariants use to identify the loopholes in the implementation, in every system we may be aware of system states which is not practically possible. By placing an invariant we can check whether the system reach such a state or not. In case if the system reach the particular invariant state, then the implementation of system has flaws and need to be fixed.

Sample syntax for invariants

invariant "<name of the invariant"
  ForAll <val> : <Values> Do  
	  if condition
    ->
	  expected implication
  End;

if condition, used to check whether the system in particular states and expected implication used to check whether system in correct state based on the given finite state machine.

Simply speaking, we can define the invariants p => q, if the condition p becomes true, the invariant check whether q is satisfied or not.

In the next post I will discuss on simple examples using the Murphi3.1.

Hope you enjoyed this post.