C-Reducer

Automatic c-reduction of object based modules for the Maude system

Summary

State space reduction techniques such as abstraction, symmetry and partial-order reduction improve automated verification tools by enhancing their performance and their ability to handle larger systems. State space c-reductions exploit  equivalence relations on states (possibly capturing system regularities) that preserve behavioral properties, and explore the induced quotient system. This is done by means of a canonizer function, which maps each state into a (non necessarily unique) canonical representative of its equivalence class. The approach is very general and supports not only traditional symmetry reductions, but also name reuse and name abstraction. The c-reducer tool implements part of the approach in Maude. In its current form the c-reducer tool is able to apply full symmetry reduction for object based Maude modules. Additional reductions, reduction strategies, customization features, and correctness checks are under development.

Publications

  1. Alberto Lluch Lafuente, José Meseguer, Andrea Vandin, State Space c-Reductions of Concurrent Systems in Rewriting Logic, International Conference on Formal Engineering Methods (ICFEM’12), Springer, 2012.

Download

The current version of the tool can be found here: c-reducer.v02.zip.

Requirements

Usage

Invoke the c-reducer script as follows

./c-reduce.sh {module file} {module name} {class sort} {id sort} {reduction}

where {module file} is the file contating the module {module name} on which to apply the reduction {reduction}; {class sort} is the sort of the class of the symmetric objects; {id sort} is the sort of their identifiers; and {reduction} (optional) is the reduction strategy. For example, we can reduce the BANK-ACCOUNT module described in the Maude manual and book (and included in the Maude distribution) as follows:

./c-reduce.sh examples/bank.maude BANK-ACCOUNT Account Aid

Other examples from the examples folder:

./c-reduce.sh examples/dbm.maude DBM Proc Pid
./c-reduce.sh examples/peterson.maude PETERSON Proc Pid
./c-reduce.sh examples/scr.maude SCR Client Pid

The input modules must satisfy some requirements:

  • The modules must be object based (see chapter 8 of the manual);
  • Sorts {class sort} and {id sort} should have views from Elt via a module called {module}-SORTS.

The output model c-{module} can be used as an ordinary module.

For example, we can test the reduction on the BANK-ACCOUNT module as follows. We first save the reduced code into a file and we load it with Maude.

./c-reduce.sh examples/bank.maude BANK-ACCOUNT Account Aid > c-bank.maude
maude c-bank.maude

Next, we explore the module’s state space with the search command.

Maude> search in C-BANK-ACCOUNT : c(top(init)) =>* x:Configuration such that false .
search in C-BANK-ACCOUNT : c(top(init)) =>* x:Configuration such that false = true .

No solution.
states: 70  rewrites: 98166 in 143ms cpu (144ms real) (681765 rewrites/second)

which can be compared with the original module with

Maude> search in BANK-ACCOUNT : init =>* x:Configuration such that false .
search in BANK-ACCOUNT : init =>* x:Configuration such that false .

No solution.
states: 625  rewrites: 4001 in 18ms cpu (18ms real) (213694 rewrites/second)

In this case a reduction of 625 into 70 states have been achieved. The reduction introduces a time overhead, since the current version of the c-reducer does not yet implement the best reduction strategies.

Apart from the reduction strategies, the performance of c-reductions can be accelerated by customizing the functions that define the ordering relation between states and the application of object transpositions. By default, the tool relies on a generic implementation based on the meta-representation of terms which hence adds the overhead of resorting to Maude’s meta-level.

The distribution of the tool comes with some examples of customized ordering relations and transposition application for one of the reduction strategies (namely FULL2). For instance, we can use the ones provided for our example as follows:

./c-reduce.sh examples/bank.maude BANK-ACCOUNT Account Aid FULL2
    examples/bank-custom.maude examples/bank-custom.maude > c-bank.maude
maude c-bank.maude

The resulting c-reduced state space can then be explored faster

Maude> search in C-BANK-ACCOUNT : c(top(init)) =>* x:Configuration such that false .
search in C-BANK-ACCOUNT : c(top(init)) =>* x:Configuration such that false = true .

No solution.
states: 70  rewrites: 26612 in 30ms cpu (30ms real) (885531 rewrites/second)

Note that reduced models are semantically equivalent to the original ones (i.e. bisimilar) only under certain conditions. For instance, some conditions for full symmetry reduction are for the state predicates to be insensitive to object permutations and the transition rules to be coherent with the canonizers.

For more details on this we refer to the above mentioned publication.

Authors

Alberto Lluch Lafuente, Andrea Vandin.

About

For suggestions, remarks, bugs or requests please do not hesitate to contact any of us.

  • andrea.vandin@imtlucca.it
  • alberto.lluch@imtlucca.it