mCRL2org/mCRL2

'Don't care' values in mu-calculus formulas

Opened this issue · 0 comments

It is quite often that in mu-calculus formulas that you don't care about some of the data parameters.

Example snippet:
<exists hr: Pos. schrijfDigitaleOutput(HSBx_SCHAK_OP_SUBRy(hr, 1), false)>true
&& [!(exists hr: Pos. schrijfDigitaleOutput(HSBx_SCHAK_OP_SUBRy(hr, 1), false))]false

Here I do not care what the value of hr is. It would be nice if the formula could be made more concise and readable in the following way:
<schrijfDigitaleOutput(HSBx_SCHAK_OP_SUBRy(, 1), false)>true
&& [!schrijfDigitaleOutput(HSBx_SCHAK_OP_SUBRy(
, 1), false)]false
The _ would indicate that the value can be antyhing in the data domain. This is similar syntax to that in some other languages where you can indicate that you do not care about a particular value, such as in destructuring Rust values.

It could be syntactic sugar that is eliminated by introducing an existential quantifier with a fresh variable name. I assume the type checker should be able to figure out what the data domain should be.