Model reversal

The model reversal modifier constructs a model with a reversed asynchronous dynamics: the successors of a state in the reversed model correspond to it's predecessors in the original model. Multivalued models are supported through model booleanization, with some changes to handle non-admissible states.

The reversal is a simple modifier without parameters: just use the -m reverse switch on the command line or lqm.modifyModel(model, "reverse") in scripts.

This service is provided by ReverseService.