meaning of -k flag in dReach

[shmarovfedor]

I noticed that in the new version of dReach -k and -u are used to specify an upper bound of unrolling. Is it possible to change -k option to define the exact number of unrolling steps (as it was used before)?

[soonhokong]

We've added -l option to specify the lower-bound of unrolling depth. Sorry for breaking the backward compatibility..

[shmarovfedor]

Thanks Soonho. I was just thinking that you have already specified -u to define an upper bound so you could probably leave -k option without any changes. It causes some difficulties for me as I will have to identify dReach version to choose appropriate command line arguments (which is not very easy as dReach does not have a --version option). However, if you need -k to be the upper bound I will deal with this problem on my end.

[soonhokong]

Again, sorry for the confusion.

@scungao and I talked about the issue. Our conclusion is to respect the original meaning of -k in BMC, which is an upper-bound of unrolling depth.

which is not very easy as dReach does not have a --version option

I understand. If you want, we can add --version option to dReach of course. At the same time, however, I'm wondering why you keep multiple versions of dReach.

[scungao]

Hi Fedor, the change on the -k option is to follow the standard meaning of
this parameter in model checkers. Do you need to use previous versions of
dReach -- in other words, are there cases where some old version
significant outperforms the new version?

On Mon, Feb 16, 2015 at 12:44 PM, Fedor Shmarov [email protected]
wrote:

Thanks Soonho. I was just thinking that you have already specified -u to
define an upper bound so you could probably leave -k option without any
changes. It causes some difficulties for me as I will have to identify
dReach version to choose appropriate command line arguments (which is not
very easy as dReach does not have a --version option). However, if you
need -k to be the upper bound I will deal with this problem on my end.

—
Reply to this email directly or view it on GitHub
#82 (comment).

[soonhokong]

@scungao, I got you here!!

[scungao]

haha

On Mon, Feb 16, 2015 at 12:47 PM, Soonho Kong [email protected]
wrote:

@scungao https://github.com/scungao, I got you here!!

—
Reply to this email directly or view it on GitHub
#82 (comment).

[shmarovfedor]

I was just checking if ProbReach works with all released versions of dReach. It is not a big problem. I will handle it. Thank you.