Rewrite strategies

From MCRL2

Tools that use the mCRL2 rewriter allow the user the specify the rewrite strategy that the rewriter should use. For command-line tools this is done with the option -r/--rewriter. The default strategy is jitty.

The following rewrite strategies are available:

inner

The interpreting innermost strategy. This strategy will fit most non critical rewriting uses, such as simulation, (simple) LPS manipulation and generation of (very) small state spaces.

innerp

inner with prover. With this strategy terms are rewritten as with inner but also a prover is used to apply BDD techniques for further reduction of (boolean) expressions.

innerc<ref name="availability_compiling">The compiling rewriter strategies are not available on all platforms. Currently it needs a Unix-based environment with gcc and appropriate headers and libraries.</ref>

The compiling innermost strategy. This is a high performance implementation of inner that is useful in time critical cases (such as generation of large state spaces). The essence of this strategy is that it generates (and compiles) a specialised rewriter for the given specification. This means that it has a slow initialisation (up to several minutes in some cases) but is many times faster when it actually starts rewriting terms.

jitty

The interpreting JITty<ref>Jaco van de Pol, Just-in-time: On Strategy Annotations, in Bernhard Gramlich and Salvador Lucas, WRS 2001, 1st International Workshop on Reduction Strategies in Rewriting and Programming, volume 57 of Electronic Notes in Theoretical Computer Science, 2001, pp. 41-63</ref><ref>Muck van Weerdenburg, An Account of Implementing Applicative Term Rewriting, in Sergio Antoy, Proceedings of the Sixth International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2006), volume 174/10 of Electronic Notes in Theoretical Computer Science, 2007, pp.139-155</ref> strategy. This strategy can avoid a lot of unnecessary rewriting in certain cases and can handle some rewrite rules that cause the innermost rewriters to rewrite infinitely.

jittyp

jitty with prover. Similiar to innerp but with JITty.

jittyc<ref name="availability_compiling"/>

Similar to innerc but with JITty.

References

<references/>