How to model non-deterministic decisions in Actors?

[mauricelam]

Hi, thanks for creating this really interesting tool!

I am trying to use this to model check a system in which actors can decide between one of a few possible actions depending on external inputs when a message is received.

Looking at Out, I only see set_timer, send and broadcast, but I don't see how I can use them to model non-determinism in the actors. Is it possible to model that using the Actor framework?

[jeffa5]

As far as I know, @jonnadal feel free to correct me, I think that the actors are supposed to be deterministic. This makes it much easier to debug their behaviour as given an input, there is only one output.

Now, what you're wanting to do with the non-determinism, basing behaviour on external inputs, is pretty standard in practice but for now requires using the lower-level Model rather than an ActorModel. Unfortunately this requires reimplementing some of the nicer bits from the actor model.

I'd imagine that we could create a hybrid of the two models, based around actors with a special function for generating environmental actions that can be non-deterministic. This might even generalise things like the network operations nicely. This would then let you have the main actor model and environmental impacts.

Hope that helps, and I'd be interested to hear if the hybrid thing might work for your case?

[jonnadal]

Yes, @jeffa5 is correct: an actor is essentially a deterministic function from its previous state and an input (like a message delivery or timer firing) to its next state and outputs (like a set of message sends or timer scheduling). Nondeterminism comes from the environment (such as reordering of messages) which manifests in varying inputs.

The framework already introduces additional nondeterminism at runtime by offering time ranges for sleep, with "elapsed time" not visible by design as doing so would increase the state space (since actors could reference it to vary behavior).

To give actors visibility into nondeterminism you also need to account for model checking and would want a design that is sensitive to the state space (favoring a small number of discrete options rather than a large number). I believe a viable solution is to introduce for instance Out::choose_random(Vec<Self::Random>) and Actor::on_random(Self::Random) or similar.

[mauricelam]

Adding Out::choose_random(Vec<Self::Random>) and Actor::on_random(Self::Random) sounds great, I think it would solve my use case perfectly.

I attempted to do this by implementing a Model that contains an ActorModel which delegates as needed, but couldn't find a way to send a message from outside of an actor (which is understandable), and modifying the actor state directly via actor_model.actor_states[id] feels like a violation of the documented requirement that "Stateright must have visibility of every input and output".

---

Using timeouts as a source of nondeterminism is interesting, I haven't though of that — if I understand correctly that means I can set the choices as timers to race against each other, and the first timer to fire will cancel the other timers to achieve the same thing as choose_random. It's not as nice as choose_random in terms of clarity, but sounds like a reasonable workaround in the meantime.

[jonnadal]

@mauricelam you could add support directly to ActorModel rather than creating a wrapping Model. This would be a welcome feature.

Also, I didn't mean to suggest using racing timers to emulate a random choice (certainly a clever idea!). Instead I was mentioning that my own earlier use case for randomness was varying sleep durations, and I just meant to contrast how that works since the random choice of duration within a specified range isn't directly observable by actors (by design).

[mauricelam]

Thanks for the directions! #80 is my attempt to add this functionality to ActorModel, and I would appreciate if you can review that. Especially for the implementation related to spawn — I am not sure if my implementation matches the design intent of that feature.

[jonnadal]

Hi @mauricelam. This is great! I left feedback and wanted to give you an opportunity to review/update before I merge.