The simulator plug-in provides a hierarchically organized stack of executor classes to run a synchronous composition of timed automata.
The ParallelExecutor implements basic timed automata behaviour, the LoggingExecutor adds so called simulation conditions, the ProposingExecutor adds a scheduling mechanism to resolve remaining ambiguities, and the DeviceExecutor adds synchronisation with physical events.
Basic simulation of synchronized timed automata.
The ParallelExecutor implements simulation behaviour for synchronised timed automata according to semantics by R. Alur and D.L. Dill. The formalism is based on clocks, invariants, guards and resets.
A timed automata refers to set of clocks that track the progress of physical time. In libFAUDES, clocks are implemented as integral typed variables that count faudes-time units (ftu). Each state has an invariant attached to impose a condition of the clock values. The system can only remain within a particular state as long as the invariant is satisfied. Each transition has an attached guard, again imposing a condition on the clock values. A transition may only be executed, when the guard is satisfied. When executing a transition, specified clocks are reset to zero.
A future revision of the timed plug-in will provide more detailed documentation.
The token format is illustrated an example.
<Executor> % Configuration "exectest.sim" <Generators> "machinea.gen" "machineb.gen" "bufferab.gen" "superab.gen" </Generators> </Executor>
Note that the specification of file-names for generators is relative to the directory of the overall configuration file. Alternatively, generators can be added inline as token sequence.
Timed automata features are read as generator attributes. The below version of the simple machine takes between 50 and 100 ftu to process a workpiece.
<Generator> % timed automata tsimplechine.gen "times simple machine" <Alphabet> "alpha" "beta" "mue" "lambda" </Alphabet> <States> "idle" "busy" <Invariant> "cBusy" "LT" 100 </Invariant> "down" </States> <TransRel> %%% I-(alpha)->B "idle" "alpha" "busy" <Timing> <Resets> "cBusy" </Resets> </Timing> %%% B-(beta)->I "busy" "beta" "idle" <Timing> <Guard> "cBusy" "GT" 50 "cBusy" "LT" 100 </Guard> </Timing> %%% B-(mue)->D "busy" "mue" "down" %%% D-(lambda)->I "down" "lambda" "idle" </TransRel> <InitStates> "idle" </InitStates> <MarkedStates> "idle" </MarkedStates> <Clocks> "cBusy" </Clocks> </Generator>
Notes. Invariant- and guard-conditions are represented as a set of inequalities; supported relations are less than "LT", less than or equal "LE", greater than "GT" and greater than or equal "GE"; all clocks must be specified in the Clocks section; clocks are meant to be unique over all generators.
Simulation of synchronized timed automata, incl logging.
The LoggingExecutor is an extension to the ParallelExecutor in that it defines so called simulation conditions and logs their occurrence for later analysis. There are two types of simulation conditions, one based on events and one based on states.
An event condition is defined by a set of start events and a set of stop events. The condition becomes satisfied when a start event occurs and it becomes dissatisfied when a stop event occurs. Thus, when start or stop events fail to alternate, the first event of the respective type is relevant.
A state condition is satisfied while the executor current state is within a specified set of discrete states. The latter set of states is to be given per component generator either as a disjunction (at least one component must match) or conjunction (all components must match). For convenience, the empty set in the conjunction is re-interpreted as the entire state set of the respective component.
While symbolic names are optional for states, it is advisable to have symbolic names for those states that are referenced by a simulation condition.
Simulations conditions can be configured by the section Condition within the executor token stream. Example:
<Conditions> % Event condition: Operation cycle "Performance" <EventCondition> <StartEvents> "alpha_a" </StartEvents> <StopEvents> "beta_b" </StopEvents> </EventCondition> % State Condition: MA is idle because the buffer is full "Bottleneck" <StateCondition> +Conjunction+ <StateSet> "idle" </StateSet> % machine a <StateSet> </StateSet> % machine b (dont care) <StateSet> "full" </StateSet> % buffer <StateSet> </StateSet> % supervisor (dont care) </StateCondition> </Conditions>
Notes. State- and event-conditions can be mixed freely with the Conditions section; conditions must have a symbolic name; disjunctive state conditions are flagged by the key +Disjunction+, conjunctive state conditions are flagged +Conjunction+.
Simulation of synchronized timed automata, incl. stochastic execution.
The ProposingGenerator is an extension to the LoggingExecutor. At each instance of time, the ProposingExecutor provides a proposal either of a specific event to be executed instantly or of how much time to let elapse. The proposal is guaranteed to comply to the underlying ParallelExecutor and the corresponding timed automata semantics.
Generating the proposal
The generation of the proposal is parametrised by so called simulation event attributes that define either a priority or a stochastic timing behaviour on a per event basis. The implementation is organized as a procedure with four stages.
Stage 1: Events with a positive priority parameter.
Stage 2: Events with a stochastic timing attribute.
Stage 3: Let time elapse.
Stage 4: Events with a negative priority parameter.
If the above stages fail to indicate an event to execute or time to let elapse, the system is deadlocked. If the procedure sticks with case 3) and infinite duration, it the system is either life locked (no enabled events) or it refuses to execute a negative priority event. The latter case is utilised for input events in a hardware-in-the-loop simulation.
Scheduling stochastic events
Events with stochastic timing attribute sample a random variable with a certain distribution in order to schedule their occurrence. The scheduling comes in three flavors, Extern, Trigger and Delay.
Note that type Extern or Delay schedules can disable the respective event in a way that potentially leads to blocking behaviour even if the timed automata is non-blocking by Alur semantics. This is a consequence of the fact that both types model additional phenomena that are synchronised with the timed automata, and it is perfectly reasonable that this synchronisation may introduce blocking situations. In contrast, events of type Trigger are not affected by the blocking issue provided that guards lie within the respective invariant.
Simulation event attributes can be configured by the section SimEvents within the executor token stream.
<SimEvents> % priority events "alpha_a" <Priority> 10 </Priority> "alpha_b" <Priority> 10 </Priority> "lambda_a" <Priority> 10 </Priority> "lambda_b" <Priority> 10 </Priority> % stochastic events "beta_a" <Stochastic> +Trigger+ +Gauss+ <Parameter> 50 20 </Parameter> </Stochastic> "beta_b" <Stochastic> +Trigger+ +Gauss+ <Parameter> 100 20 </Parameter> </Stochastic> "mue_a" <Stochastic> +Delay+ +Exponential+ <Parameter> 500 </Parameter> </Stochastic> "mue_b" <Stochastic> +Delay+ +Exponential+ <Parameter> 500 </Parameter> </Stochastic> </SimEvents>
Notes. Keys for stochastic types are +Extern+, +Trigger+, +Delay+; Supported distributions include +Gauss+ with parameters min, max, mue and sigma; +Exponential+ with parameter min, max and lambda; +Uniform+ with parameters min and max.
Simulation of synchronized timed automata, incl. physical events and time.
The DeviceExecutor is an extension to the ProposingExecutor in that it synchronises both simulation time and events with physical time and physical events provided by digital IO hardware or network messages. The actual mapping from executor events to physical events is done via an abstract interface provided by the iodevice plug-in.
We give an outline of the synchronisation procedure: