Base definitions Clause Samples

Base definitions. Time Delays. The processing of asynchronous co-simulation steps involves time delays. A MA waits for the FMU to finish some step up to a certain duration of time. To support this, we need to provide a model, which is based on the event tock that represents a unit of passing time; delays are based on a certain number of tock events that are issued. We also introduce an event timeout to represent the fact a certain time delay has elapsed. This is formalised in CSP by the following channels: ⨾ e : evsT ! e → SKIP Q ☐ e : evsB ! e → SKIP t == 0 & timeout → SKIP ◻ t > 0 & tock →Timer(t-1) Figure 5: Process WaitUntilOrTrigger Figure 5 presents process WaitUntilOrTrigger with its constituent processes, which underpins the processing of asynchronous FMU co-simulation steps. WaitUntilOrTrigger waits for a certain time delay for some event to hap- pen, if it doesn’t happen and the time delay elapses, then some event is triggered. The next process, used by WaitUntilOrTrigger , defines a Timer . If the current time is greater than 0 (there is still some time left) and a tock is issued (an instant of time has passed), then we decrease the timer by one unit. We consider that a time duration has elapsed, when the current time reaches 0, at which point Timer issues the timeout event. Timer (t ) = t = 0 & timeout → SKIP 2 t > 0 & tock → Timer (t — 1) Process WaitUntil , also used by WaitUntilOrTrigger , waits a certain amount of time until some event, of a given set, happens: WaitUntil (t, evs) = if t == 0 then Timer (t ) else Timer (t ) Δ (2 e : evs • e → SKIP ) Above, we say that the occurrence of one of the events interrupts the timer. Process WaitUntilOrTrigger (depicted in Fig. 5) executes WaitUntil with the given set of break events (evsB ), but if the timeout event is received then it triggers the events of the set of timeout trigger events (evsT ). WaitUntilOrTrigger (t, evsB, evsT ) = let WaitUntilOrTrigger0 = WaitUntil (t, evsB ) within Θ (; e : evsT • e → SKIP ) WaitUntilOrTrigger0 \ {|timeout |} Above, event timeout is hidden because it is part of WaitUntilOrTrigger only, remaining, this way, invisible to the environment. Asynchronous steps. Next process describes how a MA responds to the asynchronous execution of a FMU step. It takes an FMU index i and the number of tocks to wait for the FMU response. Then it does process WaitUntilOrTrigger , which means that it waits until event stepFinished oc- curs; if it does not occur within the given time bound, and time...