Symmetry Reduction

Symmetry reduction is a technique used in model checking to reduce the state space of a model by exploiting symmetries in the model.

This works, but the document is not complete.

Simple values for IDs

Sometimes you would want a simple value for the ID or Key. Instead of defining the keys as strings or numbers, you can define them as symmetric_values.

Run in playground

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12


# Define the keys as symmetric values instead of strings or numbers
KEYS = symmetric_values('k', 3)  # instead of KEYS = range(0, 3)

action Init:
  switches = {}
  for k in KEYS:
      switches[k] = 'OFF'
  

atomic action On:
  any k in KEYS:
    switches[k] = 'ON'

Symmetric Roles

Mark the role as symmetric, and the model checker will automatically mark the symmetric transitions as equivalent.

Run in playground

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18


Status = enum('INIT', 'DONE')

NUM_ROLES = 5

symmetric role Node:

  action Init:
    self.status = Status.INIT

  atomic action Done:
    self.status = Status.DONE
    done.add(self.__id__)

action Init:
  nodes = bag()
  for i in range(0, NUM_ROLES):
    nodes.add(Node())
  done = set()

You can try it by removing the symmetric keyword and see the difference in the number of states generated.

Order independent data structures

To reduce states explored, remember to use bags when possible instead of lists. This will ensure, the order of operations are not relevant. For more information on the available data structures, see the Data structures tutorial.