[nrf1]

> 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].

[0] https://en.wikipedia.org/wiki/Dynamic_logic_(modal_logic)

[guiraldelli]

I think a set of two equations is enough:

    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.

[nrf1]

> 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).