Circus Processes Clause Samples

Circus Processes. ‌ A mechanised version of the Timer process (Fig. 2 on page 12) is provided in Fig. 10. Its state is given by the HOL type time state and introduced by the following alphabet declaration. The alphabet command is part of Isabelle/UTP and an extension of Isabelle’s record command for introducing record types. An additional behaviour of alphabetis to define lenses for the state components, so that they can be ref- erenced within Isabelle/UTP predicates and relations; details of this are tech- nical and can be found in INTO-CPS Deliverable D2.3b, as well as [15]. Two state components are introduced: currentTime and stepSize. An added feature of the mechanised model is that we represent time abstractly by virtue of an arbitrary type ’τ that fulfils certain type-class membership constraints. The constructs TIME( ) and NZTIME( ) above impose those constraints on ’τ . They guarantee, for instance, that there exists a linear order on the elements of the time domain. They also require the existence of various arithmetic operators like +, , , and so on, with common algebraic properties. Natural, rational and real numbers are valid time domains, for instance. We observe that the Isabelle encoding of the Timer process is a nearly di- rect image of the respective Circus process. There are only a few technical artefacts that we have to remember. Firstly, when referring state components in Circus operators, it is usually nec- ▇▇▇▇▇▇ to decorate them, depending whether the underlying term is a plain predicate or relation. For instance, the occurrence of currentTime within output synchronisations requires an & prefix since the expression is over unprimed variables only. The same applies to the right-hand side of an as- signment. Secondly, where HOL values and terms are referenced, we require the double-angular brackets « ». This emphasises the difference between HOL terms and UTP terms, as the brackets here act as a coercion from the former to the latter. As can be seen, events are prefixed by ‘tm:’, which, as explained in the previous section, is necessary to facilitate later extension of the action event type when additional channels have to be declared. Circus constructs are Figure 11: Encoded InstantiationMode action of the Interaction process. subscripted to delineate to what UTP theory they belong. For instance, equality t1 =u t2 is subscripted with a ‘u’ since this operator is valid in all theories. Fixed-point and assignment, on the other hand, are subscripted with ...