You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
The text was updated successfully, but these errors were encountered: