Search with one more trace? #7
Description
Hi! Firstly, thank you for a wonderfully efficient tool!
I was curious about adaptations of Bolt such that an iterative search could be conducted - i.e. after mining a specification from a set of traces, to then add one (or a few) more traces without having to do the entire mining process again.
Reading your paper, I noted that effectively, the Bolt algorithm conducts a bounded enumerative search of candidate LTL formulas, before then considering boolean combinations with boolean subset cover. Could it be possible to start this bounded search not from say T, but from some formula? I recognize that the addition of a trace may mean that the specification at the end is not explicitly larger than the current one, so maybe this is not the direction?
Conversely, could there be any way to record a trace of the conducted search? Such that if a trace was then added, to avoid recomputation say of characteristic tables or their interactions with candidate formulas?
Would love to hear your thoughts on this! This could introduce some nice extensions to more active processes with mining in the loop.