Formalization of the reliability example

[slwu89]

The reliability model is sufficiently complex that it would be nice to show how to formalize it (to avoid bugs, to make it easier to explain, to make it more extensible, to make it more testable, etc) I am not totally sure if such an example of formalization should live in this repository or in another "examples library" but it should be considered regardless.

One way to do this would be with algebraic graph rewriting, implemented for example, in https://github.com/AlgebraicJulia/AlgebraicRewriting.jl. This provides a lot of advantages but also has some overheads in terms of needing to fully "buy in" to the C-Set concept (or typed graphs, for the general concept unrelated to AlgJulia) to formulate the model and dynamics.

Using some light functional techniques from https://thautwarm.github.io/MLStyle.jl/latest/ may be a nice middle ground. As an example, one can do (@as_record makes it possible to deconstruct arbitrary types in patterns, see https://thautwarm.github.io/MLStyle.jl/latest/syntax/pattern.html#deconstruction-of-custom-composite-data):

using MLStyle

@data IndividualState begin
    Ready
    Working
    Broken
end

mutable struct Individual
    # State for the individual
    state::IndividualState
    work_age::Float64 ## How an individual remembers its total work leading to breaks.
    transition_start::Float64  ## This is bookkeeping.
    Individual() = new(Ready, 0.0, 0.0)
    Individual(state, work_date, transition_start) = new(state, work_date, transition_start)
end

@as_record Individual

# If a vehicle is done work, or if they break, then include the time worked
# in their total work age.
accumulate_work_age!(x, when) = begin
    @match x begin
        Individual(Working, _, _) => let
            work_duration = when - x.transition_start
            x.work_age += work_duration
        end
        _ => nothing
    end
end

i = Individual(Working, 1.0, 1.2)
accumulate_work_age!(i, 2.0)

i = Individual(Broken, 1.0, 1.2)
accumulate_work_age!(i, 2.0)

However, there are some interesting questions here. For example, what are transitions? Here we have a type IndividualState, which is a sum type, and a value of it may have type Ready, Working, or Broken (additionally, because there are no fields for those subtypes, those are singleton types). But is a transition a generalized type parameterized by the type of its old and new IndividualState? Or is each transition just an ordinary type and there exists a type for each transition? Graph rewriting systems say that each transition is a span of graphs, but that makes it slightly difficult to have relationships between transitions themselves (i.e. inheritance). For example, in the reliability example, the work transition when the number of workers is equal to the maximum capacity is somehow related to (a subtype?) of the more general work transition.

The transitions are below. Interestingly knowledge of the old and new states, as here, isn't enough to determine the logic that executes when the transition fires...there is a lot of logic in handle_event which depends on other computed values (e.g. how many workers there are, etc).

const IndividualTransitions = Dict(
    :work => (Ready, Working),
    :done => (Working, Ready),
    :break => (Working, Broken),
    :repair => (Broken, Ready)
);

[slwu89]

One thing that makes this example a bit complex is the fact that the logic of the transition depends on the value of a computed quantity on the entire system (not just local state). In DB terms, we'd say it depends on a VIEW.

For this example, the work transition behaves differently if worker_cnt == experiment.workers_max compared to when that does not hold. The same is true of done and break. These aren't really 2 completely different transitions (though one certainly could think of them that way). They are related (I mean the work transition when the VIEW dependency holds vs when it does not), in that they share quite a bit of logic, and also are of the same type.

One thing would be to implement pattern matching for the key type, and the VIEW.