Max. cuddmaxem and javamaxem
26 views
Skip to first unread message
Muhammad Usama Sardar
Jul 11, 2016, 3:04:49 PM7/11/16
to PRISM model checker
Hi.
1) PC with 4 GB RAM
2) Server with 32 GB RAM
such that PRISM does not crash.
Joachim Klein
Jul 13, 2016, 3:19:01 AM7/13/16
to prismmod...@googlegroups.com
Hi Muhammad,
In the following, I'm assuming that you are using 64bit versions of
PRISM and are running on Linux or OS X. On Windows, the situation is a
bit more complicated.
First, if you are using the explicit engine, you can keep the cuddmaxmem
as-is, as then the symbolic engine is not used at all. In that
situation, you can set javamaxmem near the full amount of RAM that you
have, keeping a bit for the operating system, etc. So, for 1) something
like 3500m and for 2) something like 31g should work for javamaxmem.
If you are using one of the symbolic engines, you can increase the size
of cuddmaxmem. Note that the maxmem values do not lead to the memory
actually being used at once, so in this situation it is generally fine
to have larger cuddmaxmem and a big javamaxmem at the same time.
So, for 1) you could try cuddmaxmem of 2g and javamaxmem of 3500m and
for 2) you could try cuddmaxmem of 10g and javamaxmem of 31g. In my
experience, if the symbolic engine needs that much memory, the symbolic
operations tend to slow down so much that running time and not memory
becomes the bottle neck.
Cheers,
Joachim
PRISM and are running on Linux or OS X. On Windows, the situation is a
bit more complicated.
First, if you are using the explicit engine, you can keep the cuddmaxmem
as-is, as then the symbolic engine is not used at all. In that
situation, you can set javamaxmem near the full amount of RAM that you
have, keeping a bit for the operating system, etc. So, for 1) something
like 3500m and for 2) something like 31g should work for javamaxmem.
If you are using one of the symbolic engines, you can increase the size
of cuddmaxmem. Note that the maxmem values do not lead to the memory
actually being used at once, so in this situation it is generally fine
to have larger cuddmaxmem and a big javamaxmem at the same time.
So, for 1) you could try cuddmaxmem of 2g and javamaxmem of 3500m and
for 2) you could try cuddmaxmem of 10g and javamaxmem of 31g. In my
experience, if the symbolic engine needs that much memory, the symbolic
operations tend to slow down so much that running time and not memory
becomes the bottle neck.
Cheers,
Joachim
Muhammad Usama Sardar
Jul 13, 2016, 11:24:31 AM7/13/16
to PRISM model checker, kl...@tcs.inf.tu-dresden.de
Hello Joachim,
Thanks very much for the nice and clear explanation. It was really very helpful otherwise I had been lost. May I ask one more thing? If the model is very large, which engine is the most suitable (assuming 64-bit linux version on a 32 GB RAM server)?From the PRISM website:
Hybrid and MTBDD are mentioned to handle up to 10^8 and 10^11 respectively. While it is not mentioned for other engines. So could you please elaborate on this point?
I will be grateful to you.
--
You received this message because you are subscribed to a topic in the Google Groups "PRISM model checker" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/prismmodelchecker/0LS263MOLEY/unsubscribe.
To unsubscribe from this group and all its topics, send an email to prismmodelchec...@googlegroups.com.
To post to this group, send an 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.
Joachim Klein
Jul 14, 2016, 4:10:51 AM7/14/16
to prismmod...@googlegroups.com
Hi,
> Thanks very much for the nice and clear explanation. It was really very
> helpful otherwise I had been lost. May I ask one more thing? If the
> model is very large, which engine is the most suitable (assuming 64-bit
> linux version on a 32 GB RAM server)?
>
> From the PRISM website:
> http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/PRISMModelling#max_model_size
> Hybrid and MTBDD are mentioned to handle up to 10^8 and 10^11
> respectively. While it is not mentioned for other engines. So could you
> please elaborate on this point?
> I will be grateful to you.
Clearly, it's difficult to state that in a general way, as this depends
on particularities of the model and you have to differentiate between
"can build the representation of the model" and "can actually perform
some particular model checking".
With that amount of memory, my guess would be that PRISM with the
explicit engine should handle models with a state space in the tens of
millions states.
For the other engines (MTBDD, Hybrid, Sparse), the first hurdle is to
successfully build the symbolic representation. That heavily depends on
the model structure and the variable ordering (order of modules in the
source file and of the state variables). After building, i.e., for
actual model checking, roughly speaking, the sparse engine needs enough
memory to store an explicit representation of the (relevant parts of
the) model, i.e., the transition matrix, the hybrid engine needs enough
memory to store an explicit representation of a value vector, i.e., not
the full matrix but only a row with one value per state, and the MTBDD
engine stores everything symbolically, which does not really allow a
prediction about the memory requirements.
In the end, the easiest way is to try all 4 variants and pick the one
that works. Hopefully, one of them does :)
Cheers,
Joachim
> Thanks very much for the nice and clear explanation. It was really very
> helpful otherwise I had been lost. May I ask one more thing? If the
> model is very large, which engine is the most suitable (assuming 64-bit
> linux version on a 32 GB RAM server)?
>
> From the PRISM website:
> http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/PRISMModelling#max_model_size
> Hybrid and MTBDD are mentioned to handle up to 10^8 and 10^11
> respectively. While it is not mentioned for other engines. So could you
> please elaborate on this point?
> I will be grateful to you.
on particularities of the model and you have to differentiate between
"can build the representation of the model" and "can actually perform
some particular model checking".
With that amount of memory, my guess would be that PRISM with the
explicit engine should handle models with a state space in the tens of
millions states.
For the other engines (MTBDD, Hybrid, Sparse), the first hurdle is to
successfully build the symbolic representation. That heavily depends on
the model structure and the variable ordering (order of modules in the
source file and of the state variables). After building, i.e., for
actual model checking, roughly speaking, the sparse engine needs enough
memory to store an explicit representation of the (relevant parts of
the) model, i.e., the transition matrix, the hybrid engine needs enough
memory to store an explicit representation of a value vector, i.e., not
the full matrix but only a row with one value per state, and the MTBDD
engine stores everything symbolically, which does not really allow a
prediction about the memory requirements.
In the end, the easiest way is to try all 4 variants and pick the one
that works. Hopefully, one of them does :)
Cheers,
Joachim
Muhammad Usama Sardar
Jul 15, 2016, 12:06:18 PM7/15/16
to PRISM model checker, kl...@tcs.inf.tu-dresden.de
Hi again.
On Thu, Jul 14, 2016 at 1:10 PM, Joachim Klein <kl...@tcs.inf.tu-dresden.de> wrote:
Hi,
Thanks very much for the nice and clear explanation. It was really very
helpful otherwise I had been lost. May I ask one more thing? If the
model is very large, which engine is the most suitable (assuming 64-bit
linux version on a 32 GB RAM server)?
From the PRISM website:
http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/PRISMModelling#max_model_size
Hybrid and MTBDD are mentioned to handle up to 10^8 and 10^11
respectively. While it is not mentioned for other engines. So could you
please elaborate on this point?
I will be grateful to you.
Clearly, it's difficult to state that in a general way, as this depends on particularities of the model and you have to differentiate between "can build the representation of the model" and "can actually perform some particular model checking".
So which one of these is referred by the term "handle" on the PRISM web page I mentioned? I guess it is the later one, right?
With that amount of memory, my guess would be that PRISM with the explicit engine should handle models with a state space in the tens of millions states.
Yes, it seems so. I have been able to build a model with states up to 3.5x10^7 using the explicit engine. But any further addition of functionality does not seem to be working.
For the other engines (MTBDD, Hybrid, Sparse), the first hurdle is to successfully build the symbolic representation. That heavily depends on the model structure and the variable ordering (order of modules in the source file and of the state variables). After building, i.e., for actual model checking, roughly speaking, the sparse engine needs enough memory to store an explicit representation of the (relevant parts of the) model, i.e., the transition matrix, the hybrid engine needs enough memory to store an explicit representation of a value vector, i.e., not the full matrix but only a row with one value per state, and the MTBDD engine stores everything symbolically, which does not really allow a prediction about the memory requirements.
In the end, the easiest way is to try all 4 variants and pick the one that works. Hopefully, one of them does :)
Unfortunately, none of them is working :(
Cheers,
Joachim
--
You received this message because you are subscribed to a topic in the Google Groups "PRISM model checker" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/prismmodelchecker/0LS263MOLEY/unsubscribe.
To unsubscribe from this group and all its topics, send an email to prismmodelchec...@googlegroups.com.
To post to this group, send an 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.
Reply all
Reply to author
Forward
0 new messages