Shorthand notation for observation variables

[markuzzz]

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.