|
> but if we stick to the evaluation order defined by the language Is this true? According to the linked page: "The program will continually pick rules at random from the set of applicable rules, until there are no such rules." In your encoding, we could end up transition from state {3Eve, 1Alice, 1Bob} to state {3Eve, 1AliceBob}. I agree that, in the next time step, we might transition back to {3Eve, 1Alice, 1Bob}. But there are two problems with this formulation: 1. We often (in many domains always) really care about the intermediate behaviors of the model, not just the final state. Which means that an observation of the trace: {3Eve, 1Alice, 1Bob} ~> {3Eve, 1AliceBob} ~> {3Eve, 1Alice, 1Bob}
is often not necessarily equivalent to simply staying in state {3Eve, 1Alice, 1Bob}. This is especially true in physical systems (including chemical reactions).2. We might end up back in the "right" state, but only for those two rules! In particular, we might not actually end up back in state {3Eve, 1Alice, 1Bob} after all if there are other transition rules. For example: Eve + AliceBob → Alice + Bob + Eve
Alice + Bob → AliceBob
AliceBob + Eve → WEIRDNESS
With some probability (which the docs don't specify) we might now observe the following transition: {3Eve, 1Alice, 1Bob} ~> {3Eve, 1AliceBob} ~> {2Eve, WEIRDNESS}
with no way to get back to {3Eve, 1Alice, 1Bob} :-(One additional problem: this encoding is not equivalent to the guarded version if transitions can have side-effects (e.g., if transitions consume a global implicit "fuel" or some other abstract representation of cost). |