Circus. Circus is a process algebra similar to CSP [19], but with additional support for defining data operations and state. Circus inherits many of its process operators from CSP, including sequential and parallel composition, input and output communications on a channel c, synchronisation, external choice, interrupt, guard and recursion. A summary of Circus constructs relevant to our models in this deliverable is given in Table 1. To define a process state, a Circus process declares a record in its state paragraph, whose fields define a data model. Data operations can either be written as Z operation schemas [28] or constructs from Xxxxxx’x refinement calculus [23], such as specification statements, assignments, conditionals and iteration. Circus has a rich set of laws that can be used for verification and refinement [7]; it is thus an ideal language for developing state-rich imple- mentations from abstract specifications of reactive systems. A notable trade-off in Circus is that the language enforces non-interference of Name Syntax Description Sequence A ; B Execute A and B in sequence. Parallel Comp. A cs B ¢ ¢ Execute A and B in parallel, synchronising on the channels in the channel set cs. External Choice A B Q The environment decides whether to execute A or B ; communication resolves the choice. Synchronisation c −→ A Synchronisation on a (typeless) channel c. Input Prefix c?x −→ A(x ) Input a value x on a typed channel c. Output Prefix c!e −→ A Output a value e on a typed channel c. Guarded Action g A g Proceed with A only if g is true. Interrupt A O c −→ B A is interrupted by synchornisation on channel c. Recursion µ X • F (X ) Execution recursive action F . Assignment x := e Assignment to a state component x . Table 1: Overview of relevant Circus action operators. parallel computations; this endows it with a monotonic parallel composition operator that facilitates piecewise and compositional development.
Circus. Circus shall as its Initial Capital Contribution contribute to the Company Circus interest in the Preference Rights, for which Circus shall receive a credit to its Capital Account as follows: (i) $5 million upon full execution and delivery of this Agreement and satisfaction of the conditions set forth in Section 4.05(e)(i); and (ii) $8 million payable upon Initial Licensing and satisfaction of the conditions set forth in Section 4.05(e)(ii). 5.02
Circus. The main construct of Circus is a process, used to specify a system and its components. Processes communicate with each other via channels. Com- munications are instantaneous and synchronous events. A process can have a state, defined using a Z schema, and a behaviour, defined using an ac- tion. The specification of an action can combine Z schemas that specify data operations over the state and CSP constructs. To illustrate Circus, Fig. 1 presents the model of a Timer from a valid master algorithm. Timer takes as parameters the current time ct , the step size hc, and the end time tN of the simulation. Although it is possible to set up experiments without an end time, we restrict ourselves to experiments channel : setT : TIME ; updateSS : NZTIME ; × step : TIME NZTIME ; end ^ • process Timer = ct, hc, tN : TIME begin state State == [currentTime, stepSize : TIME ] Step = setT ?t : t ≤ tN −→ currentTime := t ; Step Q −→ QupdateSS ?ss −→ stepSize := ss; Step step!currentTime!stepSize Q g currentTime := currentTime + stepSize; Step −→ currentTime = tN end Stop • currentTime, stepSize := ct, hc; Step end
