Hi, As part of my PhD research, I am using MRMC for statistical model checkering. For a given model(tra) and a property, I need to know how much time MRMC spends for (i)parsing the model, (ii)generating its simulation, and (iii)the time spend for property verification.
Is it possible to somehow access these informations?
Thank you very much, Best
Mehmet Emin BAKIR University of Sheffield http://www.sheffield.ac.uk/ Department of Computer Science Verification and Testing Group http://www.sheffield.ac.uk/dcs/research/groups/vt
Dear Mehmet,
Op 25 nov. 2015, om 22:17 heeft Mehmet E Bakir mebakir1@sheffield.ac.uk het volgende geschreven:
As part of my PhD research, I am using MRMC for statistical model checkering. For a given model(tra) and a property, I need to know how much time MRMC spends for (i)parsing the model, (ii)generating its simulation, and (iii)the time spend for property verification.
Is it possible to somehow access these informations?
I propose that you instrument the function parseInParamsAndInitialize() in file src/mcc.c to measure the time (i). The time of (ii) and (iii) together is already measured in the function modelCheckFormulaTree() in file src/io/parser/parser_to_core.c. You can change the calls to startTimer() and stopTimer() in this function to split the two steps.
Kind regards, David N. Jansen.
Dear MRMC developer(s), Can we identify how much time spent for simulation trace generation, and the time spent for property verification. Is it possible to separately identify each time when verifying a model with MRMC in statistical model checking mode? Or MRMC does verification on fly(parallel with simulation) which means we can't separate them?
Thanks in advance, Best
Mehmet Emin BAKIR University of Sheffield http://www.sheffield.ac.uk/ Department of Computer Science Verification and Testing Group http://www.sheffield.ac.uk/dcs/research/groups/vt
On 25 November 2015 at 21:17, Mehmet E Bakir mebakir1@sheffield.ac.uk wrote:
Hi, As part of my PhD research, I am using MRMC for statistical model checkering. For a given model(tra) and a property, I need to know how much time MRMC spends for (i)parsing the model, (ii)generating its simulation, and (iii)the time spend for property verification.
Is it possible to somehow access these informations?
Thank you very much, Best
Mehmet Emin BAKIR University of Sheffield http://www.sheffield.ac.uk/ Department of Computer Science Verification and Testing Group http://www.sheffield.ac.uk/dcs/research/groups/vt
mrmc-users@lists.rwth-aachen.de
-
David N. Jansen -
Mehmet E Bakir