Make LDFI smarter

[symbiont-daniel-gustafsson]

The current implementation of LDFI, isn't as smart as it could probably be. At the moment it uses a sat-solver to pick a fault-set such that the fault-set hasn't been seen before. But we don't have much smarts going in telling what would happen if any particular failure happened. Part of the problem is that we simply doesn't have that information for two reasons:

1) We don't really know which message made the checker happy. 2) We don't know why different reactors chooses to make certain messages.

This assumes that there will be some sort of information being sent to a reactor that will make the checker happy (and continue to be happy). If we knew that information (potentially using some model) we could as a strategy have to try to inject faults so that message can't happen. If we can't drop that message (because it is not a valid move according to the failurespec) we need to make it so that the reactor that sent the message don't want to send it (by which we need 2) and this process might be needed to be repeated if the proposed earlier message(s) is also outside the failurespec.

[symbiont-stevan-andjelkovic]

The following PR #129 made a lot of progress on this issue.

[symbiont-stevan-andjelkovic]

Another possible way of being "smarter" could be to explore the fault state space in a breath-first fashion, so that for example different combinations of two possible faults are explored before introducing a third fault into the mix and so on. This could potentially lead to fault set minimisation (shrinking) being less important.

[symbiont-stevan-andjelkovic]

A nice property to have for a breath-first search: if a test fails with EFF=T and some set of faults F, and if it fails with EFF=T' where T' > T with some set of faults T' then F <= F'.

For this to hold true, we'd need to define some kind of metric on faults and have the SAT solver minimise that metric.