Symmetry Based Model Checker

The program employs the latest results on symmetry for checking safety and liveness properties of concurrent system of processes. The input to the system consists of a concurrent program given as a set of processes specified as transition systems. It also takes as input a Buchi automaton on infinite strings that accepts all the incorrect computations, that is, the automaton accepts the complement of the correctness property. The system checks if there exists a fair computation of the program that is accepted by the automaton, i.e., if there exists an incorrect computation. If such a computation exists it outputs a ``YES'' answer, otherwise it terminates with a ``NO'' answer indicating that the program satisfies the correctness property. SMC can handle both weak fairness and strong fairness. The user can specify either option as part of the command line.

The program first reads the code of the concurrent program written in the input language specified below as well as the finite state automaton that provides the negation of the property to be checked. From the read code the compressed computation space, called Annotated Quotient Structure (AQS), is constructed. Finally, the product of the automaton and the AQS is constructed (called the BBar structure) and a search for a reachable strongly connected component is performed. For brief introduction follow SMC: A Symmetry based Model Checker for Verification of Safety and Liveness Properties. For details on the theoretical background, see On-the-Fly Model checking under Fairness that Exploits Symmetry.

Syntax of SMC

OPTIONS:
-s<num>

This parameter controls the symmetry option. If the value of <num> is zero then symmetry compression is not used. If the program has no symmetry then this option is the best. If the value of <num> is 2 or 4 or 6 then only process symmetry is employed. The higher the value, the more sophisticated is the equivalence checking algorithm employed, resulting in fewer number of states in the constructed structure. If the value of <num> is 3 or 5 or 7 then both process symmetry and state symmetry are employed. As before, the higher the value, the more sophisticated is the employed equivalence checking algorithm. If the value of <num> is 3 then both process symmetry and state symmetry are employed. This gives maximum compression but it also has more overhead for detecting process as well as state symmetry.

This parameter controls the on-the-fly option. If the value of <num> is 0 then on-the-fly option is used. If it is 1 then on-the-fly option is used.

This parameter controls the fairness option. Here <C> is a character with value "w" or "s". Value "w" specifies weak fairness, while value "s" specifies strong fairness. The default is weak fairness.

This parameter allows counter example to be printed; it also allows printing of AQS, BBar states and transitions. It controls the output verbosity. Bit 0: basic information on performance. Bit 1: the parsed input text is printed in a lengthy way. Bit 2: information on each AQS state is printed. Bit 3: counter example is printed. The counter example consists of a strongly connected component in BBar and a path leading to it. Bit 4: information on each BBar state is printed. For example, an option value of 24 (where bits 3 and 4 have value 1) prints all the BBar states and trasitions; it also prints a counter example.

Specifies the name of the program file. Default is ClientServer.prg.

The Input language

An input consists of commands separated by semicolon. A command is one of module declaration, variable declaration, index variable declaration or module description. All variables need to be declared, but index variables can be declared implicitly. A module description is a set of module commands. A module command is of the form condition -> actions. A condition is an expression with positive value. An expression is built from variables and constants using the following operands:

• arithmetical: + - * ? %,
• logical: < > <= >= == != <> and & or | not !,
• i == j and i != j where i and j are index variables,
• <quantor>( <ind_var> : <expression>) where <quantor> is one of ALL EXISTS AND OR PRODUCT SUM NUMBEROF.

program   : Program commands

commands  : commands command
          | command

command : Module  name = value ;                        
        | name [ some_module_names ] = value ;                            
        | ind_var : module
        | ind_var ;

some_module_names : 
                  | module_names 

module_names      : name 
                  | name,  module_names

ind_var : name
        | name `of' name 

module  : { module_commands }
        | module_command 

module_commands : module_commands module_command 
                | 

module_command  : condition -> actions ;
                
actions : action 
        | action , actions 
       
action  : variable  = condition
        | ALL ( ind_var : actions ) 

Program
Module controller = 1;
Module client     = 49;
lc[controller]              = 0;
lk[client]                  = 0;
reply[controller, client]   = 0;
request[controller, client] = 0;
buzy[controller]            = 0;

c of controller :
{ 
lc[c] == 0 &  request[c, k] == 1  -> 
                reply[c, k] = 1, buzy[c] = 1 , lc[c] = 1;
lc[c] == 1 & buzy[c] == 0  -> 
                lc[c] = 0 ;
}

k of client :
{
lk[k] == 0  ->  request[c, k] = 1 , lk[k] = 1;
lk[k] == 1 & reply[c, k] == 1 ->
                reply[c, k] = 0, request[c, k] = 0, lk[k] = 2;
lk[k] == 2 ->   buzy[c] = 0 , lk[k] = 0;
}

The language of the automata specification

automata :  InitialState name ; a_commands      

a_commands:
                | a_command ; a_commands
        
a_command       : FinalState 
                | FinalState a_fin_states 
                | Tracking             
                | Tracking a_trackings   
                | a_transition 
 
a_fin_states    : name
                | name , a_fin_states  

a_trackings     : a_tracking
                | a_tracking , a_trackings

a_tracking      : number `of' name 

a_transition    : condition -> name : name

InitialState M0;

FinalState M1; 
ALL(k1 of client: ALL(k2 of client: k1== k2 or  lk[k1] + lk[k2] < 4)) -> M0:M0;
EXISTS(k1:EXISTS(k2: k1!=k2 & lk[k1]==2 & lk[k2]==2)) -> M0:M1;
True              -> M1:M1;