If the rule is applicable and its application results in a new state, the function should return non-zero and PX will add the new state to its tables for later evaluation. When applying a rule with repeat count N to a state, PX will call the associated function N times with arguments from 0 to N-1. Once the data structures, variables, and transition rules are defined, we have a protocol. Invariants are functional descriptions of properties that should always be true regardless of what transitions. For example, if your protocol is supposed to provide a mutual exclusion property, you might provide an invariant to check whether more than one node is in a critical section.
Goals are functional descriptions of what a protocol is intended to achieve.
Every state transition from every state must lead to a goal state. If any transition leads to a state which is terminal but not a goal state,or to an infinite loop, the protocol is considered incorrect. For example, if the protocol is intended to guarantee that a message gets from A to B despite N dropped packets, a goal state would be one in which B has received the message. The significance of repeat counts is the same as for rules, and the associated C functions are of the same type also. For a goal, the function should return non-zero to indicate that the state meets the requirements for a goal state.