Range definition

[sohaib...@gmail.com]

Hello . I want help from you people. Can anyone tell me that how will I define range of a variable outside the module. Example I declare variable 

const double Hosp1;

I want that user enter the value of Hosp1 within range 0 to 25. How will I do that?

Secondly i define guard [alpha] d = 0 -> 0.4 : (d'=1) + 0.6 : (d'=2); I want to run another command at [alpha +1] but it is giving me syntax error in prism

Kindly help 

[Dave Parker]

Hi,

> Hello . I want help from you people. Can anyone tell me that how will I
> define range of a variable outside the module. Example I declare variable
>
> const double Hosp1;
> I want that user enter the value of Hosp1 within range 0 to 25. How will
> I do that?

That is not a variable, it is a constant, i.e. its value will be the
same in any state of the model. If you want to run multiple instances of
verification, each with a different value for the constant, then use an
experiment:

http://www.prismmodelchecker.org/manual/RunningPRISM/Experiments

If you wanted a global variable, i.e. one that can be accessed from any
module, see here:

http://www.prismmodelchecker.org/manual/ThePRISMLanguage/GlobalVariables

> Secondly i define guard [alpha] d = 0 -> 0.4 : (d'=1) + 0.6 : (d'=2); I
> want to run another command at [alpha +1] but it is giving me syntax
> error in prism

The action label (the bit between the []) needs to be alphanumeric - the
+ symbolic is not allowed. So just rename "alpha+1" to something else.

Best wishes,

Dave.