search

dreal / dreal2

Please check dreal4 instead.
https://github.com/dreal/dreal4
GNU General Public License v3.0
13 stars 15 forks source link

meaning of -k flag in dReach #82

Open shmarovfedor opened 9 years ago

shmarovfedor commented 9 years ago

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 commented 9 years ago

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

shmarovfedor commented 9 years ago

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 commented 9 years ago

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 commented 9 years ago

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 notifications@github.com 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 https://github.com/dreal/dreal/issues/82#issuecomment-74546411.

soonhokong commented 9 years ago

@scungao, I got you here!!

scungao commented 9 years ago

haha

On Mon, Feb 16, 2015 at 12:47 PM, Soonho Kong notifications@github.com wrote:

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

— Reply to this email directly or view it on GitHub https://github.com/dreal/dreal/issues/82#issuecomment-74546904.

shmarovfedor commented 9 years ago

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.