Simulator Speed

[Mehmet Emin BAKIR]

Hi,

I wonder why when we use statistical model checking of Prism, it is quite fast, But when we try to use the simulator of prism to get simulation traces, it is too slow. 

For example when I run statistical model checking for 1000 iteration where each iteration depth is 1000 as well, it roughly checks a property of my model aroun 2-3 seconds.

However when I tried to get traces of simulate same model 1000 times it took around 75-80 seconds.

I assume the statistical model checker  already produces simulation traces and in addition it verifies property as well, It does more work than the simulator, hence I would expect the simulator will produce traces faster since it does not involve any verification process.

So my question is, why simulation is slower than SMC and is there a solution to increase the simulation speed?

Thank you

[Marcin Copik]

Dear Mehmet,

> For example when I run statistical model checking for 1000 iteration where each iteration depth is 1000 as well, it roughly checks a property of my model aroun 2-3 seconds.

The path length is given as a maximum. If the property has been verified, e.g. satisfying state reached, bad prefix generated or an upper time bound reached, then the generation of a path will stop.

Moreover, there is more than one class for path generation, SMC needs to store only previous and current state, but the generation of a trace requires a full storage in memory which may influence the execution time.

> a solution to increase the simulation speed

There's no simple answer to that question. The simulator engine in PRISM is quite heavy, it repeats all evaluations in model many times during path generation and it has too many dependencies to be easily parallelized (although in your case it should be possible to create independent instances of SimulatorEngine and generate traces concurrently). 

During last year's GSoC, I've developed some improvements for simulator, including optimized storage of the model in memory and preprocessing of the model, but I don't know if it has been already merged with trunk. It may be treated as an experimental solution. I am working on a simulator engine based on OpenCL, but it supports only stochastic model checking.

Best regards,

Marcin Copik

--
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 http://groups.google.com/group/prismmodelchecker.
For more options, visit https://groups.google.com/d/optout.

[Dave Parker]

Hi Mehmet,

There are various reasons why statistic model checking could be faster.

Firstly, it is generating paths in order to check whether some property
is true along each path. Therefore, it will stop generating each path as
soon as it can, i.e., as soon as it knows whether the property is true
or false. When generating paths explicitly (e.g. with -simpath), you
often simply specify a length of path to generate. You can look at
information displayed about min/max/average path lengths during
statistical model checking to see if this is having an effect.

Secondly, statistical model checking does not usually store the paths
that it generates - it analyses them on-the-fly to see if a property if
true or false. But when you use -simpath, the full path is stored in
memory for later processing or output. So in your case, there is
additional overhead both to store the path and to export it to a file.

For the second of these, it might be possible to export the path
on-the-fly. But there will still be overhead from writing to a file.

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>.

[Haakan Younes]

I don't know what output you need, but perhaps you could try Ymer to generate simulation traces?  Ymer is a complementary tool to PRISM, aiming to be compatible with the PRISM language, while focusing heavily on statistical model checking.  Ymer has fairly comprehensive support for PRISM models of type DTMC and CTMC.  The Ymer simulator is a lot leaner than the one in PRISM, and compiles a PRISM model into a representation that allows faster path generation.  The source code for Ymer is available on GitHub:

https://github.com/hlsyounes/ymer

Here is an example command line that will generate simulation traces with Ymer:

$ echo 'P=?[true U false]' | GLOG_logtostderr=1 GLOG_v=3 ./ymer src/testdata/poll5.sm /dev/stdin --fixed-sample-size 2 --max-path-length 10 2>/tmp/paths.log >/dev/null

The "echo 'P=?[true U false]'" is just a dummy property to prevent Ymer from terminating traces early.  The "GLOG_logtostderr=1 and GLOG_v=3" enables trace logging to STDERR.  The "--fix-sample-size 2" means you get 2 simulation traces, and "--max-path-length 10" means each trace is 10 states long (9 state transitions).  The "2>/tmp/paths.log >/dev/null" discards STDOUT output and writes STDERR output to the file "/tmp/paths.log".  The contents of this file will contain simulation traces of the form:

I0825 16:31:53.716259 19066 sampling.cc:593] t = 0: s=1 & a=1 & s1=1 & s2=1 & s3=1 & s4=1 & s5=1

I0825 16:31:53.716280 19066 sampling.cc:593] t = 0.355792: s=2 & a=0 & s1=0 & s2=1 & s3=1 & s4=1 & s5=1

I0825 16:31:53.716292 19066 sampling.cc:593] t = 0.359045: s=2 & a=1 & s1=0 & s2=1 & s3=1 & s4=1 & s5=1

I0825 16:31:53.716302 19066 sampling.cc:593] t = 1.81449: s=3 & a=0 & s1=0 & s2=0 & s3=1 & s4=1 & s5=1

I0825 16:31:53.716313 19066 sampling.cc:593] t = 1.82722: s=3 & a=1 & s1=0 & s2=0 & s3=1 & s4=1 & s5=1

I0825 16:31:53.716323 19066 sampling.cc:593] t = 1.87453: s=3 & a=1 & s1=1 & s2=0 & s3=1 & s4=1 & s5=1

I0825 16:31:53.716333 19066 sampling.cc:593] t = 2.40277: s=4 & a=0 & s1=1 & s2=0 & s3=0 & s4=1 & s5=1

I0825 16:31:53.716343 19066 sampling.cc:593] t = 2.41559: s=4 & a=1 & s1=1 & s2=0 & s3=0 & s4=1 & s5=1

I0825 16:31:53.716353 19066 sampling.cc:593] t = 2.69273: s=5 & a=0 & s1=1 & s2=0 & s3=0 & s4=0 & s5=1

I0825 16:31:53.716364 19066 sampling.cc:725] t = 2.69654: s=5 & a=1 & s1=1 & s2=0 & s3=0 & s4=0 & s5=1

I0825 16:31:53.716369 19066 sampling.cc:727] >>positive sample

I0825 16:31:53.716384 19066 sampling.cc:457] 1  1.00001

I0825 16:31:53.716393 19066 sampling.cc:593] t = 0: s=1 & a=1 & s1=1 & s2=1 & s3=1 & s4=1 & s5=1

I0825 16:31:53.716403 19066 sampling.cc:593] t = 0.163821: s=2 & a=0 & s1=0 & s2=1 & s3=1 & s4=1 & s5=1

I0825 16:31:53.716413 19066 sampling.cc:593] t = 0.164924: s=2 & a=1 & s1=0 & s2=1 & s3=1 & s4=1 & s5=1

I0825 16:31:53.716423 19066 sampling.cc:593] t = 1.1923: s=2 & a=1 & s1=1 & s2=1 & s3=1 & s4=1 & s5=1

I0825 16:31:53.716434 19066 sampling.cc:593] t = 3.29144: s=3 & a=0 & s1=1 & s2=0 & s3=1 & s4=1 & s5=1

I0825 16:31:53.716442 19066 sampling.cc:593] t = 3.30155: s=3 & a=1 & s1=1 & s2=0 & s3=1 & s4=1 & s5=1

I0825 16:31:53.716452 19066 sampling.cc:593] t = 5.10428: s=3 & a=1 & s1=1 & s2=1 & s3=1 & s4=1 & s5=1

I0825 16:31:53.716470 19066 sampling.cc:593] t = 5.30678: s=4 & a=0 & s1=1 & s2=1 & s3=0 & s4=1 & s5=1

I0825 16:31:53.716481 19066 sampling.cc:593] t = 5.30931: s=4 & a=1 & s1=1 & s2=1 & s3=0 & s4=1 & s5=1

I0825 16:31:53.716491 19066 sampling.cc:725] t = 7.0022: s=5 & a=0 & s1=1 & s2=1 & s3=0 & s4=0 & s5=1

I0825 16:31:53.716496 19066 sampling.cc:727] >>positive sample

I0825 16:31:53.716502 19066 sampling.cc:457] 2  2.00002

The relevant information here are the lines like:

t = 5.10428: s=3 & a=1 & s1=1 & s2=1 & s3=1 & s4=1 & s5=1

This shows the time of entry into the state and the values of state variables.  Each trace starts at t = 0.

I can't tell if this would satisfy your needs, but I expect trace generation would be a lot faster.

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

[memin...@gmail.com]

Dear Haakan

Thank you very much for your detailed email. It is really very good to see different model checkers try to unify their modelling language. Since my models are translated into prism language it will be easy to test with Ymer. It is good that it allows get multiple paths, but I will need to modify the output format of the tool for my needs.

I just wondered does the tool runs on windows platform. I want to try and measure some performance values. Also I would like to ask could you share us its binaries(either for windows or Linux OS) of the tool.

 

 

Thank you,

> <mailto:prismmodelchec...@googlegroups.com>.

[Haakan Younes]

Sorry, I have not attempted to compile Ymer on Windows.  I do not have a binary distribution.  Ymer is source code only and you would have to compile it yourself for your target platform.

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

[Mehmet Emin BAKIR]

I have run it on Linux platform my next attempt will be on windows. The simulation speed is good enough for me. I will play with output if I could use the code on windows.
Thank you for your emails.

Best
Mehmet Emin BAKIR

> <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.

 

 

--
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/52YWaqHUam4/unsubscribe.
To unsubscribe from this group and all its topics, send an email to prismmodelchec...@googlegroups.com.
To post to this group, send email to prismmod...@googlegroups.com.