> I am not certain how it'd be best to define a rule that predicates on an absence of a token but that syntax is terrible.
That would be pretty confusing. Instead, transitions can always be allowed to happen if the left hand side is satisfied and then the "don't transition if there's an Eve" semantics -- when necessary/desired -- can be made explicit by adding assertions to each nondeterministic transition.
For example, if you want 1 Adam and 1 Bob to transition to 1 AliceBob regardless of Eves then you write:
Alice + Bob -> AliceBob
but if you want to insist there are no Eves for this rule to hold, then you write:
assert(0Eve);
Alice + Bob -> AliceBob
in which case there must be 0 Evens in order for the Alicebob transition to happen.
These sorts of nondeterministic transitions with optional guards are expressible in dynamic logic; see see A3 + A8 in [0].
Eve + AliceBob → Alice + Bob + Eve
Alice + Bob → AliceBob
I understand with non-deterministic behaviour and 10 Alices, 10 Bobs and 10 Eves I can get in a certain state (Alice, Bob, Eve, AliceBobs) = (1, 1, 10, 9), but if we stick to the evaluation order defined by the language, then the two rules above satisfy the condition.
> 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:
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:
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).
That would be pretty confusing. Instead, transitions can always be allowed to happen if the left hand side is satisfied and then the "don't transition if there's an Eve" semantics -- when necessary/desired -- can be made explicit by adding assertions to each nondeterministic transition.
For example, if you want 1 Adam and 1 Bob to transition to 1 AliceBob regardless of Eves then you write:
but if you want to insist there are no Eves for this rule to hold, then you write: in which case there must be 0 Evens in order for the Alicebob transition to happen.These sorts of nondeterministic transitions with optional guards are expressible in dynamic logic; see see A3 + A8 in [0].
[0] https://en.wikipedia.org/wiki/Dynamic_logic_(modal_logic)