Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
markuzzz opened this issue Dec 19, 2024 · 0 comments
Open

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

markuzzz opened this issue Dec 19, 2024 · 0 comments

Comments

@markuzzz
Copy link

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant