Redundancy Check option in the Tool Bar uses Spin
-A option to apply a property-based slicing
algorithm for the model, which can detect eventual redundancies in the
model and generate suggestions on how the model could be revised in order
to use less memory.