Is there support or any way to simulate constant sized array variables and uniformly distributed integer generation?

[kpjo...@illinois.edu]

I would like to use both constructs.

Currently, for constant sized array variables, I must create a separate variable for each index:

foo[3] => foo1 foo2 foo3

though I use a script to automatically generate these correctly, I was wondering if there is inbuilt support for these yet.

I have also taken a look at the preprocessor at http://www.prismmodelchecker.org/prismpp/ which would do the same as my script.

Second, I would like to generate random integers in [a,b] where a,b are parameters.
For this I have no clue what to do. A much older thread https://groups.google.com/forum/#!topic/prismmodelchecker/OlA1aYiZrS4 discussed this when a,b are known. But in my case, I would like to keep them parametric.

[Joachim Klein]

Hi,

> Currently, for constant sized array variables, I must create a separate
> variable for each index:
> foo[3] => foo1 foo2 foo3
> though I use a script to automatically generate these correctly, I was
> wondering if there is inbuilt support for these yet.
> I have also taken a look at the preprocessor
> at http://www.prismmodelchecker.org/prismpp/ which would do the same as
> my script.

Yeah, that would currently be the way to go, as there is no built-in
support in PRISM. When we had to model something like this, we also
generated the PRISM models via some template / macro preprocessing.

> Second, I would like to generate random integers in [a,b] where a,b are
> parameters.
> For this I have no clue what to do. A much older
> thread https://groups.google.com/forum/#!topic/prismmodelchecker/OlA1aYiZrS4
> discussed this when a,b are known. But in my case, I would like to keep
> them parametric.

There is currently no elegant support for that, but this is something we
are currently looking into as that would be useful for some of our
modelling as well. So, there might be support for that in the future.

Out of interest, what do you mean by "parametric"? Do you want to be
able to set the range boundaries via constant expressions (where the
constatns can then be specified via command-line, GUI, or experiments)
or do you need the boundary expressions to depend on the state variables
as well?


Cheers,
Joachim Klein