Specification suffer from re-entrancy bugs

[shaunazzopardi]

Consider how during a call to a transfer function, satisfying the required pre-condition (and thus transitioning from state Before to state After), the transfer function may call transfer function again (remaining in state After) and ending in a way that satisfies the required post-condition (transitioning back to Before). But this leaves the end of the original call unmonitored.

Proposed Solution: Augment DEA language to allow specifications to be replicated per function call.

[shaunazzopardi]

ce3008a prevents these bugs, but not an ideal solution since it prevents re-entrancy instead of managing it.