Assume message-structure: A: bool and consider this send over the broadcast channel:
{A & true} *! (true) (A := false) []
This should raise a validation error: message variables in the predicate are only allowed on receives.
Similarly:
- Message variables should never appear as the left-hand side of an update
- Message variables should never appear anywhere in an update after a send
We should add a simple validator to check these.