|
|
||||||
|
sp_plpexecutor.h
Go to the documentation of this file.
39 * enabled, the ProposingExecutor actually proposes either one particular transition for execution or
41 * parametrised by data from SimEventAttribute. The decision procedure is organized in four stages,
52 * an event with stochastic timing is scheduled to occur, the earliest of such events form the candidate set.
58 * - if the EnabledInterval is of infinite duration, let all clock time pass and stop the simulation
67 * invariant and guard conditions. In this sense, the above procedure is compliant with Alur semantics
70 * If the above procedure fails to indicate a transition to execute or clock time to let pass, the
72 * either life locked (no enabled events) or just unwilling/unable to execute a negative priority event.
82 * when it matched the current clock time, regardless whether the event is executed or not. When the
86 * point. By "effective guard interval" we refer to the interval of time in which the guard is satisfied
89 * interval. In order to guarantee that the scheduled occurence lies within the guard, the density function
90 * is shaped accordingly. The schedule expires when either the event is actually executed or when the
94 * enabled. A sample is taken when the executor is reset to determine the initial amount of delay.
95 * During the execution sequence the executor accumulates the durations for which the event is enabled. The event
100 * potentially leads to blocking behaviour even if the timed automata is non-blocking by Alur semantics.
102 * synchronized with the timed automata, and it is perferctly reasonable that this synchronisation
104 * In contrast, events of type Trigger are not affected by the blocking issue provided that guards lie
157 * Technical detail: since the trace buffer only covers the dynamic state of the parallel executor,
158 * the RevertToStep method cannot recover the stochastic event states. Including stochastic states
429 virtual void DoWrite(TokenWriter& rTw, const std::string& rLabel="", const Type* pContext=0) const;
#define FAUDES_TYPE_DECLARATION(ftype, ctype, cbase) faudes type declaration macro Definition: cfl_types.h:867 Synchronized parallel execution of TimedGenerators. Definition: sp_pexecutor.h:64 Executer that proposes which transition to execute. Definition: sp_plpexecutor.h:165 const sEventSet & Alphabet(void) const Access alphabet (incl simulation event attributes) Definition: sp_plpexecutor.h:245 sEventSet mSimEvents Simulation event attributes, incl stochastic and priority data. Definition: sp_plpexecutor.h:364 Attribute for an event in the context of simulation. Definition: sp_simeventset.h:149 A TokenReader reads sequential tokens from a file or string. Definition: cfl_tokenreader.h:63 A TokenWriter writes sequential tokens to a file, a string or stdout. Definition: cfl_tokenwriter.h:51 Base class of all libFAUDES objects that participate in the run-time interface. Definition: cfl_types.h:239 Includes all libFAUDES headers, no plugins. TaNameSet< AttributeCFlags > Alphabet Convenience typedef for event sets with controllability attributes. Definition: cfl_cgenerator.h:240 Executor with logging facilities Evaluating random variables. Eventsets with execution data for simulation. Include timed plugin headers. libFAUDES 2.32b --- 2024.03.01 --- c++ api documentaion by doxygen |