The program demonstrates the latest results on how the symmetry of a concurrent program can be utilized in compressing the computation space. 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.
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 Liveness Properties. For details on the theoretical background, see On-the-Fly Model checking under Fairness that Exploits Symmetry.
OPTIONS:
-s<num>
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:
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 )An example program is the client server driver specification:
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; }
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 : nameThe Mutual Exclusion property for the client server program is coded in the following example.
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;