Question about Modelling a synchronous system with large number of nodes using DTMC

[Negin]

Hi all,

I am currently working with PRSIM to model leader election in a synchronous systems of up to 6 nodes using DTMC. My ultimate goal is to model my algorithms for large systems (for example for 100 nodes), but with the current settings I am using ( using global variables, formulas, etc) it can be too complex to continue with the same approach for much bigger systems although I am using one process module and several instances of this module for the rest of the processes.

This can be problematic for both defining the model and verification properties. So, my question is that whether there is a better way to model large synchronous systems in PRISM. 

I appreciate if anyone can provide me with some information and possibly some examples of large  systems modeled in PRISM.

Best,

Negin

[Dave Parker]

Hi Negin,

There are two separate issues here. One is the ease with which you can
model the system, the other is the size of the resulting model during
verification. It is most likely the latter that will limit how large the
system can be (i.e. how many nodes in your case). But it seems like you
are more concerned here about the former, i.e. how easy it is to write
the model down. If you are already using module renaming to create
multiple processes, there is not too much more you can do in this
regard. But you could also look at the PRISM preprocessor, which is a
way of generating large model descriptions more easily.

Best wishes,

Dave.

> --
> 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
> <mailto:prismmodelchec...@googlegroups.com>.
> To post to this group, send email to prismmod...@googlegroups.com
> <mailto:prismmod...@googlegroups.com>.
> Visit this group at http://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.

[Negin]

Hi Dave,

Thanks for introducing me the Preprocessor idea. I am currently using PRISM under Windows. I changed the prism.bat file as you discussed in previous posts but still PRISM cannot recognize #..# command. Am I missing something?

Thanks in advance for your help.

Best,

Negin

> <mailto:prismmodelchecker+unsub...@googlegroups.com>.