[FEATURE] Seed the randomness for deterministic model based test generation

[ebuchman]

Is your feature request related to a problem? Please describe.

Currently every time we regenerate tests we get new ones.

Describe the solution you'd like

A way to regenerate the same set of tests, typically in a case where we've changed some data structure on the Rust side but otherwise want to be testing the same scenario.

[andrey-kuprianov]

To do the testing in the proper way, we need to have it both ways:

• allow Z3 to choose it's random seed, and then provide it to the user in the output (for exploratory testing)
• accept the seed in the user input, and pass it to Z3 (for test reproducibility)

[konnov]

I am reading the z3 docs, and the developers say that z3 should be deterministic. The default seed is 0. Are we sure that we get non-determinism from z3? @andrey-kuprianov, you can produce the smt log with --debug, run it with z3 several times and see, whether the results are different.

I will add an option to set the seed. But it may happen that non-determinism is also on our side.

[andrey-kuprianov]

well, the outcome is that smt logging seems to be broken. first, it's log0.smt that's being produced. Second, after some initial valid SMT commands, it contains some printout, which is not an SMT-LIB:

(error "line 44536 column 1: invalid command, '(' expected")
(error "line 44538 column 7: unexpected character")
(error "line 44538 column 19: unexpected character")
(error "line 44550 column 8: unexpected character")

(assert (= $C$1994 (>= $C$1776 $C$1993)))
; } IntCmpRule returns $C$1994 [1995 arena cells])
;; assert $C$1994
(assert $C$1994)
(check-sat)
;; sat = true
$C$0 = FALSE
$C$1 = TRUE
$C$2 = {FALSE, TRUE}
$C$3 = Nat

[konnov]

That's weird. It used to work pretty well. Are you feeding this back to z3?

[konnov]

log0.smt is fine. There are multiple solver instances in the parallel version.

[konnov]

Oh wait. The last four lines are the output of the sat model. Just delete all these things.

[konnov]

I have added #320 on that issue. But if you remove the model output at the end of the log, it should work.

[konnov]

That command seems to produce stable results:

z3 -smt2 smt.random_seed=1 sat.random_seed=1  log0.smt

However, setting random_seed in the Java API does not help, and Solver complains about smt.random_seed.

[konnov]

The code in this branch sets all random seeds to 0 by default, or to the value passed as smt.randomSeed in the tuning properties, with --tuning=tuning.properties.

When I run Apalache in Intellij Idea on test/tla/Rand.tla, the produced counterexample is always the same. When I run Apalache in the command line, two different results are produced. The file log0.smt only differs in the values of the produced model. It might be something about pointers having different values, not really sure about what is going on.

@andrey-kuprianov can you try this branch and see, whether you also get different results on test/tla/Rand.tla?

[konnov]

Related discussion on stackoverflow: https://stackoverflow.com/questions/47839976/z3-producing-different-models-when-run-multiple-times

[konnov]

The observation that it worked with Intellij Idea led me to try different versions on java.

Java(TM) SE Runtime Environment (build 1.8.0_172-b11)

z3 behaves non-deterministcally

Java(TM) SE Runtime Environment (build 9.0.4+11)

z3 behaves deterministically (on Rand.tla)

We need JDK8 to compile scala, but the compiled code should work in later JREs too. So I guess the current solution will be to run MBT in JRE9 or later.

[konnov]

It should work unless you are using Java 8