Shorthands in process expressions

[markuzzz]

In equations it is possible to use the construction whr z = x + y end. This is a very convenient way of using shorthands in complex data expressions.

In (complex) process expressions it is often also desirable to use such shorthands. As far as I know the only way to do this at the moment is to use a sum: sum z:Int. (z == x + y) -> action(z)

This has two issues:

• At times the enumerator/rewriter is unable to deal with such constructions (especially in the presence of other sums)
• Not all datatypes are enumerable, functions are not enumerable, and by extension all user-defined data types using functions are also not enumerable.

It would be convenient to have a construction similar to whr z = x + y end for process expressions. Since process expressions can be rather large a scope might also be handy: begin .... whr z = x + y end

[tneele]

When exactly do the issues with the sum construction arise? Is that during linearisation (mcrl22lps) or during state-space generation (lps2lts)? In the latter case, you might be able to circumvent them by first applying lpssumelm to eliminate the sum variable and its equality.

By the way, if we do decide to add a whr process expression, I don't think we need a 'begin' keyword, since the desired scope can always be achieved with some parentheses.

[mlaveaux]

We have decided that this language extension is not desirable enough to implement.