Unifying Reactive Languages. NSRD healthy predicates encompass a number of existing languages, notably Circus and CML, and thus acts as a unifying layer for stateful reactive contracts. We will show that these UTP theories are all subsets of NSRD, and thus all the laws we have proved so far are applicable. This section thus serves to demonstrate the breadth of application of our UTP theory. We first consider CSP and Circus. In addition to the reactive design healthiness condi- tions, CSP1 and CSP2, the UTP CSP semantics adds CSP3 and CSP4. Definition A.4 (CSP Healthiness Conditions). CSP3(P) ¾ SKIP ; P CSP4(P) ¾ P ; SKIP The operator SKIP is equivalent to the Skip operator, but without state variables as CSP does not have these. CSP can be obtained by simply setting the state-space type Σ to a xxxxxxxxx set, which effectively removes state. In this case, R3h degenerates to R3, and thus Rs degenerates to X. Xxxxxxxxxx and Xxxxxxxx [9] proved that SKIP is equivalent to the reactive design R(true € trj = tr ∧ waitj), which in turn is equivalent to [ truer |- false | tt = () ]. We can then prove the following theorem. Theorem A.11 (CSP processes are NSRD healthy). If P is R and CSP1-CSP4 healthy, then P is NSRD healthy − − Proof. Since SRD is equivalent to R CSP1 CSP2 is suffices to show that P is RD3 healthy. From CSP4 we know that P = P ; SKIP. Moreover, we know that SKIP is RD3 since it satisfies the form given in Theorem A.3.2: the precondition is clearly RC1, and the pericondition does not mention stj. Consequently, SKIP ; IIR = SKIP, and thus by associativity of ; it follows that P is NSRD. Circus actions are similar to CSP processes, but have slightly different healthiness condi- tions that do account for state variables. Effectively, they require that the Circus action Skip is a left and right unit. Then, following a similar proof to Theorem A.11, we can show that Circus actions are indeed NSRD healthy. Circus additionally has the healthi- ness condition C3 [40] that mandates that the precondition of a reactive design can only contain undashed variables. Though true for Circus processes, this is over-restrictive and prevents assumptions with trace behaviour in reactive contracts. Thus our model is both unifying and more general, in that we only mandate the the precondition is RC1. We next show that our model also encompasses CML, a formal discrete time modelling language for systems of systems. Sequential CML actions are characterised by six health- iness conditions that we enum...
