'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.