Declaring constant inside a module

[hacha]

Hi,

Is it possible to declare a constant, say k, inside a module, say M1.
my goal is to create a number of these modules (M2, M3, ..Mn) where
each module has a different k (i.e. I would like to define something
like
"module M2 = M1 [ k=4 ] endmodule" ), not sure if this directly or
indirectly
possible to do?

thank you,

Hichem.

[Mark Kattenbelt]

Hi Hichem,

I don't believe you can do it in the way you have described. I suspect
the easiest way to do this is to define some global constants K1, ...,
Kn and use these in renaming as in the following model:

const int K1 = 1;
const int K2 = 2;

module M1
x1 : [0..K1];
[] (x1 < K1) -> (x1' = x1 + 1);
endmodule

module M2 = M1 [x1 = x2, K1 = K2] endmodule

[Muhammad Usama Sardar]

Hi everyone. 

The proposed solution is going to increase the states of the system very much. I was wondering if there is some other possible solution which can reduce the states, possibly such that it is considered as a local constant instead of global. 

Any suggestion will be appreciated. 

[Gethin Norman]

I do not see how it will change the state space as constants do not add to the state space. You will end up with the modules you want and the state space will be the same if you could have done it the other way.

thanks

Gethin

> --
> You received this message because you are subscribed to the Google Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to prismmodelchec...@googlegroups.com.
> To post to this group, send email to prismmod...@googlegroups.com.
> Visit this group at https://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.

[Muhammad Usama Sardar]

I want to assign IDs to each module which are to be used later. So in fact, 

const int K1 = 1; 

const int K2 = 2; 

 
module M1 

  x1 : [0..10]; 

  <Some commands>

endmodule 

module M2 = M1 [x1 = x2, K1 = K2] endmodule 

There are going to be a number of such modules with renaming, such that their IDs are different; and important thing is that the IDs remain fixed throughout. So I want to model it using constant, instead of the state variable that is proposed in this thread. Since constants do not add to state space while variables do, the proposed solution is going to add to the state space in my case. 

Moreover, is there a way to make K1 and K2 local constants instead of global? (so that I have everything inside a model making more explicit that K1 represents ID of module M1 and so on)