Interaction with Implementation
pfeodrippe opened this issue · 7 comments
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.
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.
Make use of TLC coverage information to better drive which paths will be taken.
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.
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).
For Arrudeia, maybe the process can run and pinpoint points of change so it can help you decide where to put the labels,