Executor Classes

ParallelExecutor

Basic simulation of synchronized timed automata.

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.

Token IO

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.

LoggingExecutor

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.

Event conditions

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.

State conditions

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.

Token IO

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+.

ProposingExecutor

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.
If one or more events with positive priority are enabled, those with maximum priority form the candidate set. If the candidate set is non-empty propose one event by random (uniformly distributed) for immediate execution.

Stage 2: Events with a stochastic timing attribute.
If within the interval at which the set of enabled events remains constant an event with stochastic timing is scheduled to occur, the earliest of such events form the candidate set. If the candidate set is non-empty, propose one event by random (uniformly distributed) for execution at the scheduled time.

Stage 3: Let time elapse.
If the interval at which the set of enabled events remains constant represents a finite positive duration, propose that amount of time to elapse. If the latter interval represents an infinite duration, propose to let all time pass and stop the simulation.

Stage 4: Events with a negative priority parameter.
If one or more events with negative priority are enabled, those with maximum priority form the candidate set. If the candidate set is non-empty, propose one event by random (uniformly distributed) for immediate execution.

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.

Extern.
The random variable models an external stochastic process which is not constraint by the timed automata dynamics. A sample is taken when the executor is reset to determine the first scheduled occurrence. The schedule expires when it matches the current clock time, regardless whether the event is executed or not. When the schedule expires, a new sample is taken to determine the next scheduled occurrence.

Trigger.
The random variable is used to narrow down the effective guard interval to a point. By "effective guard interval" we refer to the interval of time in which the guard is satisfied w.r.t. the current timed state. A sample is taken when the executor enters a state with a non-empty effective guard interval. In order to guarantee that the scheduled occurrence lies within the guard, the density function is shaped accordingly. The schedule expires when either the event is actually executed or when the effective guard interval changes due to a transition.

Delay.
The random variable models a delay relative to the clock time when the event is first enabled. A sample is taken when the executor is reset to determine the initial amount of delay. During the execution sequence the executor accumulates the durations for which the event is enabled. The event is scheduled when the accumulated durations matches the delay. When the event is executed the, schedule expires and the random variable is sampled to re-initialised the 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.

Token IO

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.

DeviceExecutor

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:

1. get a proposal from ProposingEcexutor

2. if physical time is ahead of the generators current clock time, formally execute the missing time (i.e. adjust clock variables); in the case that this is not consistent with the proposal, an error is reported;

3. if the generators current clock time is ahead of physical time, an error is reported

4. if an input event has been reported that can be executed at the generators current time, execute it and continue with 1.

5. if the proposal schedules an event for the generators current time, execute it and continue with 1.

6. if an input event has been reported, execute it now; if this event is not accepted by the generator, report an error; continue with 1.

7. if the proposals time is not yet executed, wait until that amount of time elapsed or for an input event to be delivered; continue with 1.