5. Perspicuity, Divergence, and Internal Operations

In going from the relational semantics of CSMATs in Chap. 3 to the abstract data types of Chap. 4 we made a number of radical changes. We labelled individual transitions with the name of an operation, much as we had been doing in LTS and automata in Chaps. 1 and 2, and removed transitivity from the transition relation as we were now able to observe individual steps. We also created a separation between local (abstract) state and global (concrete) state that extended the idea of state abstraction in Chap. 3. One aspect of CSMATs that has not been fully reflected in the relational data types yet is reflexivity of the transition relation, or “stuttering”: an unchanged state could be the outcome of a labelled transition, but not every occurrence of “nothing has changed” is worth recording explicitly as a transition. This chapter will look more closely at this – leading to the concept of “perspicuous” operations in refinement. CSMATs allowed us to remain agnostic about having potentially infinite traces in the model; uncovering perspicuous operations forces us to worry about invisible things happening infinitely often (“livelock”). Thus, divergence needs to be addressed now.