Executing simulator many times and outputting all traces at the end.

[Mehmet Emin BAKIR]

Hi everyone,

I need to get simulation traces of a prism model from commandline. I am facing two difficulties, first one is I need to exclude the action column from produced traces. 

And the second one is I need define the simulation sample size, that is I mean, the simulator needs to repeat to produce traces a more than one time, e.g, 1000. 10.000,  times. 

Currently am calling the prism simulator from commandline in a loop (i.e., 1000 times), and  for each turn, I modify the outputted traces file by removing the action column. 

Which makes the process too slow. Is there a better way you can advice?

Thank you.

[Marcin Copik]

Hi Mehmet,

I'm not sure whether it is possible right now to generate multiple outputs in one run. It shouldn't be hard for me to provide a fix with such option, but you can try another thing: if the traces are not very long, then you may be spending a lot of time on initialization of JVM on every run of PRISM. This problem was mentioned on mailing list few weeks ago:

https://groups.google.com/forum/#!topic/prismmodelchecker/OErvM7wBYgQ

If the initialization time of JVM is not the bottleneck in your case, then we may look for another solution.

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.

[Mehmet Emin BAKIR]

Hi Marcin,

Thank you for your prompt reply. Since I need many traces, reducing the JVM initialization times is quite important, but in my case it still not enough. Because my ultimate aim is to produce many simulation samples to a single file (to reduce I/O time as well), and also the the action column should be discarded. I have double checked options, unfortunately it seems, I need to modify the source code. I hope I can import and run the code in windows and eclipse environment:)

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

--

Mehmet Emin BAKIR

[Dave Parker]

Hi Mehmet,

As suggested by Marcin, it should not be a big job to update PRISM's
-simpath functionality so that it (a) outputs multiple paths and (b)
omits the action labels when printing. One of us should be able to
provide some pointers or patches to do this. Are you compiling your
version of PRISM from from source code?

Best wishes,

Dave.

> <memin...@gmail.com <mailto:memin...@gmail.com>> napisał:

>
> Hi everyone,
> I need to get simulation traces of a prism model from
> commandline. I am facing two difficulties, first one is I need
> to exclude the action column from produced traces.
> And the second one is I need define the simulation sample size,
> that is I mean, the simulator needs to repeat to produce traces
> a more than one time, e.g, 1000. 10.000, times.
> Currently am calling the prism simulator from commandline in a
> loop (i.e., 1000 times), and for each turn, I modify the
> outputted traces file by removing the action column.
> Which makes the process too slow. Is there a better way you can
> advice?
>
> Thank you.
>
> --
> 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.
>
> --
> 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/oUH5_6DAHvQ/unsubscribe.
> To unsubscribe from this group and all its topics, 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.
>
>
>
>
> --
> Mehmet Emin BAKIR
>

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

[Mehmet Emin BAKIR]

Dear Dave,
Yes I had modified the code which outputs multiple paths and ignores action. The results I presented belongs to the modified code which is still slow.

Dear Marcin
Thank you for explanation. If you somehow improved the performance, I will really appreciate if I can have the code. 

Thank you,
Best

Mehmet Emin BAKIR