Runs in actions work but are not model-checkable

[bugarela]

As the effect system still doesn't implement runs (related to #450), it is possible to define things like:

action init = initialize.then(setup).then(confirm)

action step = sendMessage.then(receiveMessage)

These work fine in the simulator, but won't be model-checkable as neither Apalache nor TLC support the cdot operator for action composition.

However, it turns out these are useful and we should probably not disallow them completely. Perhaps we should show some sort of warning + info on how to convert it into separate actions. Perhaps we can "inline" action composition with auxiliary state vars to make this work with the model checkers without extra action from the user - afterall, TLA+ does define the cdot and we'd have formal semantics for it.