Interrupts have strange refusal interaction with gaps

[MattWindsor91]

A follow-up issue from #63: while the gap itself is now allowing the model to refuse actions stated inside the gap set. the interrupt /\ used to connect the gap set to the action it follows doesn't seem to have the right semantics.

Specifically, in the translation of anything in E until event x, the gap apparently cannot refuse x at any time - if x is offered by the environment it always makes the gap resolve. This is unwanted, as the model might want to perform more things in E first.

Some solutions (discussing with Pedro) include:

• replacing /\ with [| |> for arrow actions only, using a construction similar to that in page 141 of Understanding Concurrent Systems to do any binding;
• replacing event x's construction with a wrapper that nondeterministically allows tocks to occur while waiting for event x, thus allowing it to be refused.

At time of typing, I'm heading towards the latter, but am unsure whether that wrapper should be part of the gap or a more general modality on arrow actions.

[MattWindsor91]

Solved (for now) with the temperature modality: by default actions get wrapped in a cold temperature that allows the indefinite refusal of the action.