Skip to content

Add a support for runtime analysis and ability to guide oneof-decisions #276

@buzden

Description

@buzden

In theory we can have an interface(s) passed to unGen or to its alternative, running in a monad (like existing CanManageLabels) having information about

  • start of generation
  • successful and unsuccessful end of generation (unsuccessful, however, can be managed through MonadError, as now already)
  • most importantly,
    • the current decision point (index of the chosen oneof node of a generator tree, and indices of all previous decisions, thus identifying uniquely full path to the current decision point)
    • possibly, a decision that is going to be made (we'll need to modify pickWeighted for that slightly)
    • possibly, all the labels met in the generator tree before the current point (but, this can be made with existing CanManageLabels in a stateful monad)
    • ability to override the default decision with our own one (based, say, on the statistics or whatever)

Maybe, we can generalise unGen by not requiring MonadRandom, but the default implementation of the proposed interface should require it, thus calls to randomFin and pickWeighted would be inside this default implementation. Then, statistics-based one would be a named implementation requring external similarly typed implementation, just adding the statistics-management functionality. This idea, however, requires changes in RawGen data type, since we will need not MonadRandom, but the proposed decision-making interface there, which whould make us unable to use simple choose unless this decision-making interface is a subinterface of MonadRandom, or at least it implies it somehow. Well, maybe, we can treat empty list of the current decisions as a stuff that can provide MonadRandom?

This all can be used for collecting and analysing current decisions and their influence on, say, SUT's coverage, thus implementing a coverage-guided adjustments. It can, say, find that particular decisions influence positively on, say, SUT's coverage and increase probability of these decisions. Alternatively, it can increase probabilities of never visited choices in order to achieve better diversity of generated samples and increase the model coverage. Finally, it can just analyse the other decision algorithm and print its statistics afterwards. Existing labelling mechanism can be handy for such reports.

Roughtly speaking, this interface (or at least, the decision part) is meant to be something like this:

interface Decision m where
  choicePoint : (path : List Nat) -> (altWeights : List Nat1) -> m $ Fin altWeights.length

Probable problem is that (original) weights of alternatives is a constant for each path, thus it can be remembered inside m. It means that users of the interface must guarantee the same values of weights for each path, or weights should be returned in some other way (maybe, it should be an indexing function by the generator and path?). Maybe, we should use not a list of nats as a path, but a special data structure that is indexed by Gen?

Metadata

Metadata

Assignees

No one assigned

    Labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions