search

pfeodrippe / recife

A Clojure model checker (using the TLA+/TLC engine)
Other
136 stars 3 forks source link

Interaction with Implementation #4

Closed pfeodrippe closed 2 years ago

pfeodrippe commented 3 years ago

With a lot of states, it may be infeasible to keep everything in memory, we could use https://github.com/lambdaisland/edn-lines to just append edn data line to a file. But let's try first with transit to see if any problem surfaces, the spec says that it has compaction. Yeah, better create checkpoints and use these generated files when reading, if you have a lot of states and you want to test the app, it should be negligible anyway.

For hillel.ch2-recycler-2, we have ~53k distinct states and the EDN file has ~13MB.

There is also https://github.com/replikativ/konserve which is a KV store using EDN semantics (get-in , assoc-in etc). Ouch, but it's painfully slow for our use case, so it's excluded.

Spike with DFS to check if it's usable to call the app in real time or if we will have to do it ad hoc. Let's do the ad hoc way, it's much simpler.

pfeodrippe commented 3 years ago

Maybe we can use some statistics to show that enough coverage was done and we have X% of certain that the implementation is a "refinement" of the model.

pfeodrippe commented 3 years ago

https://github.com/tlaplus/tlaplus/issues/367#issuecomment-532936460

Make use of TLC coverage information to better drive which paths will be taken.

pfeodrippe commented 3 years ago

https://youtu.be/lj31oIaYSj4

pfeodrippe commented 3 years ago

https://twitter.com/hillelogram/status/1395557894565863426?s=19

pfeodrippe commented 3 years ago

Could we use some of the ideas from the LDFI paper (Lineage Driven Fault Injection by Peter Alvaro et al) to drive our implementation testing using the state graph?

We already have all the required provenance, but which data do we have to say if one path is safe? Otherwise TLA+ would just use this to reduce state explosion.

We could favor paths which has the large number of processes changes. How to do that? No idea ATM.

pfeodrippe commented 3 years ago

The user can create a counter example by changing the spec a little bit so it violates an invariant or a temporal property and reusing this failed trace in a impl test (which will have to pass).

pfeodrippe commented 3 years ago

For Arrudeia, maybe the process can run and pinpoint points of change so it can help you decide where to put the labels,