Can UPPAAL offer a special variable for Guard-statements?

[denizcaygoz]

Hi,

I've been modelling my system in UPPAAL and I encountered a problem which is sometimes Guard-statements are too long in Models. And that leads to complicated view of the model. Which could be visually hard to unterstand.

As can be seen in the image. statements marked with red are too long.

So can UPPAAL offer a special variable for Guard-statements which is defined in Declarations (or maybe in an another file you can offer), so that we define the variable in that file and we write to the Guard only the name of the variable.

For example:
instead of writing to the Guard this statement:
isSystemOn == true && (isOccupied == false || temperature > INC_FULLINC && temperature < DEC_FULLDEC)

We define the Statement-Variable in Declarations or in another file like this:
var ifStatement = isSystemOn == true && (isOccupied == false || temperature > INC_FULLINC && temperature < DEC_FULLDEC)

And then we write only the variable name to the Guard:
ifStatement

[mikucionisaau]

Yes, the proper abstraction is a function call: define a function computing the value of the expression and then call that function in the guards instead.

For example, in declarations (either in global or local):

bool isAllowed() {
  return isSystemOn == true && (isOccupied == false || temperature > INC_FULLINC && temperature < DEC_FULLDEC);
}

Then call it on the guard: isAllowed()
(functions can also have parameters)

Functions work only over boolean and integer variables (the clock constraints must still be written on the guard).

Note that boolean variables can be used directly in expressions. For example isSystemOn == true can be written as isSystemOn, isOccupied==false can be written !isOccupied or not isOccupied (same with boolean operations: && can be written as and -- sometimes it can be more readable).

Also UPPAAL uses C rules for converting between boolean and integer expressions so even integer expressions can be shortened. For example, given declaration:

int i = 5;

Guard expression i is true if i!=0, and false when i==0.