Problem
The most trivial data type in Uppaal is the integer. Unlike in most programming languages, the int data type is a 16-bit signed number with a range of [-32768, 32767], unless specified otherwise.
In general, it is considered bad practice not to explicitly specify the bounds of data variables (e.g. by using data types):
It indicates that the modeler may not have thought about the possible values a integer may hold.
Specifying the bounds of an integer decreases the size of a state.
Unnecessarily unbounded integers can drastically increase the state space of a model.
Integer variables going outside of their intended (but not specified) range remain undetected.
Detecting overflows require the integers to go outside the default range, which may require a very large state space to be explored
Proposed solutions
The most basic solution would be a warning when using unbounded integers, which can be achieved with simple static analysis using the Ecore utils.
The more elegant solution would be to deduct what the bounds of integer variables should be based on some type of data flow analysis. E.g. based on an edge guard x < 10 with a update x = 0, one could conclude that x should have an range of [0, 10]. An variable x whose only assignment is y = x * x should have bounds [0, 100].
Bachelor project?
Problem
The most trivial data type in Uppaal is the integer. Unlike in most programming languages, the
intdata type is a 16-bit signed number with a range of [-32768, 32767], unless specified otherwise.In general, it is considered bad practice not to explicitly specify the bounds of data variables (e.g. by using data types):
Proposed solutions The most basic solution would be a warning when using unbounded integers, which can be achieved with simple static analysis using the Ecore utils.
The more elegant solution would be to deduct what the bounds of integer variables should be based on some type of data flow analysis. E.g. based on an edge guard
x < 10with a updatex = 0, one could conclude thatxshould have an range of[0, 10]. An variablexwhose only assignment isy = x * xshould have bounds[0, 100].