Maximum value of a variable in PRISM

[Muhammad Usama Sardar]

Hi everybody. 

I was wondering if there is any restriction on the maximum value of the variable in PRISM, e.g. 65536 or so. 

Secondly, I could not find a concatenation operator to form a packet, which is common in Communication Systems. Is it possible somehow? 

Thank you. 

[Joachim Klein]

Hi,

> I was wondering if there is any restriction on the maximum value of the
> variable in PRISM, e.g. 65536 or so.

Generally, my guess would be that if you stick to values that can be
stored in a Java int (i.e., roughly speaking above -2^31 and below 2^31)
you should be fine, provided that all intermediate values during
expression calculations (guards, assignments, ...) are also in that
range... However, if you have variables with such huge ranges,
performance might be quite bad. In general, you should try to abstract
from concrete values in your application as far as possible, while still
allowing you to express the property you want to check, naturally.


Cheers,
Joachim