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
It is a common use case to use 'observation variables' in mu-calculus formulas to track the state of the system. Certain action then change these variables, usually only one at a time. For example:
nu X(
long_variable_name_1: Bool = false,
long_variable_name_2: Bool = false,
long_variable_name_3: Bool = false,
long_variable_name_4: Bool = false
).(
[a]X(true, long_variable_name_2, long_variable_name_3, long_variable_name_4)
&& [b]X(long_variable_name_1, true, long_variable_name_3, long_variable_name_4)
&& [c]X(long_variable_name_1, long_variable_name_2, true, long_variable_name_4)
&& ....
)
The more variables there are, the more annoying it becomes to repeat all the names of unchanged variables. I just wrote a formula with 9 observation variables for Rijkswaterstaat. Moreover, it becomes difficult to read because the variable that is changed is the interesting one but exactly the name of that variable is not given in the update. For recursion in processes there is a shorthand notation that could also be used here:
nu X(
long_variable_name_1: Bool = false,
long_variable_name_2: Bool = false,
long_variable_name_3: Bool = false,
long_variable_name_4: Bool = false
).(
[a]X(long_variable_name_1 = true)
&& [b]X(long_variable_name_2 = true)
&& [c]X(long_variable_name_3 = true)
&& ....
)
It could probably be implemented easily as syntactic sugar that is replaced in a preprocessing step.
The text was updated successfully, but these errors were encountered:
It is a common use case to use 'observation variables' in mu-calculus formulas to track the state of the system. Certain action then change these variables, usually only one at a time. For example:
nu X(
long_variable_name_1: Bool = false,
long_variable_name_2: Bool = false,
long_variable_name_3: Bool = false,
long_variable_name_4: Bool = false
).(
[a]X(true, long_variable_name_2, long_variable_name_3, long_variable_name_4)
&& [b]X(long_variable_name_1, true, long_variable_name_3, long_variable_name_4)
&& [c]X(long_variable_name_1, long_variable_name_2, true, long_variable_name_4)
&& ....
)
The more variables there are, the more annoying it becomes to repeat all the names of unchanged variables. I just wrote a formula with 9 observation variables for Rijkswaterstaat. Moreover, it becomes difficult to read because the variable that is changed is the interesting one but exactly the name of that variable is not given in the update. For recursion in processes there is a shorthand notation that could also be used here:
nu X(
long_variable_name_1: Bool = false,
long_variable_name_2: Bool = false,
long_variable_name_3: Bool = false,
long_variable_name_4: Bool = false
).(
[a]X(long_variable_name_1 = true)
&& [b]X(long_variable_name_2 = true)
&& [c]X(long_variable_name_3 = true)
&& ....
)
It could probably be implemented easily as syntactic sugar that is replaced in a preprocessing step.
The text was updated successfully, but these errors were encountered: