Executer that proposes which transition to execute.
Priority and Stochastic Semantics
Whilst the LoggingExecutor (and all lower level executors) is aware of which transitions are enabled, the ProposingExecutor actually proposes either one particular transition for execution or a particular amount of time to let pass. The proposal refers to additional semantics parametrised by data from SimEventAttribute. The decision procedure is organized in four stages, were the first stage that yields a proposal wins:
1.) SimPriorityEventAttribute, positive priority
- if one or more events with positive priority are enabled, those with maximum priority form the candidate set
- if the candidate set is non-emty propose one event by random (uniformly distributed) to be executed immediately
2.) SimStochasticEventAttribute, stochastic timing
- if within the interval at which the set of enabled events remains constant (EnabledInterval) an event with stochastic timing is scheduled to occur, the earliest of such events form the candidate set.
- if the candidate set is non-emty propose one event by random (uniformly distributed) to be executed at the scheduled clock time.
3.) passing by clock time
- if the EnabledInterval is of positive duration, let this duration pass by.
- if the EnabledInterval is of infinite duration, let all clock time pass and stop the simulation
4.) SimPriorityEventAttribute, negative priority
- if one or more events with negative priority are enabled, those with maximum priority form the candidate set
- if the candidate set is non-emty propose one event by random (uniformly distributed) to be executed immediately
Note that the above procedure will never come up with a proposal that fails to satisfy invariant and guard conditions. In this sense, the above procedure is compliant with Alur semantics of timed automata.
If the above procedure fails to indicate a transition to execute or clock time to let pass, the system is deadlocked. If the procedure sticks with case 3) and infinite duration, it might be either life locked (no enabled events) or just unwilling/unable to execute a negative priority event. The latter case can be used for sensor events in a hardware-in-the-loop simulation.
Scheduling Stochastic Events
The mechnism to schedule events with stochastic timing comes in three flavors.
- SimStochasticEventAttribute::Extern The random variable models an external stochastic process. A sample is taken when the executor is reset to determine the first scheduled occurence. The schedule expires when it matched 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 occurence.
- SimStochasticEventAttribute::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 timed state with a non-empty the effective guard interval. In order to guarantee that the scheduled occurence 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.
- SimStochasticEventAttribute::Delay The random variable models a delay relative to the clock time when the event is 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 synchronized with the timed automata, and it is perferctly reasonable that this synchronisation introduces blocking situations. In contrast, events of type Trigger are not affected by the blocking issue provided that guards lie within the respective invariant.
File IO
For token IO, the ProposingExecutor reads and writes a section with default label "Executor". It contains a ParallelExecutor section to define a vector of generators, a SimConditionSet section to define relevant conditions, and a SimEventSet section to define the above event attributes. Example:
<Executor>
<Generators>
"./some_generator.gen"
"./other_generator.gen"
</Generators>
"IdleCond"
<EventCondition>
<StartEvents> "beta" "mue" </StartEvents>
<StopEvents> "alpha" </StopEvents>
</EventCondition>
"DownCond"
<StateCondition>
</StateCondition>
<SimEvents>
"alpha"
<Priority> 100 </Priority>
"beta"
<Stochastic> +Trigger+ +Gauss+ <Parameter> 10 5 </Parameter> </Stochastic>
"mue"
<Stochastic> +Delay+ +Gauss+ <Parameter> 20 5 </Parameter> </Stochastic>
"lambda"
<Priority> 100 </Priority>
</SimEvents>
</Executor>
const SimConditionSet & Conditions(void) const
Read-only access to simulation conditions.
Technical detail: since the trace buffer only covers the dynamic state of the parallel executor, the RevertToStep method cannot recover the stochastic event states. Including stochastic states with the trace buffer is considered to expensive.
Definition at line 165 of file sp_plpexecutor.h.
|
|
| | ProposingExecutor () |
| | Creates an emtpy ProposingExecutor. More...
|
| |
| | ProposingExecutor (const ProposingExecutor &) |
| | Copy constrcutor. More...
|
| |
|
| const SimEventAttribute & | EventAttribute (Idx index) const |
| | Simulation event attribute lookup. More...
|
| |
| void | EventAttribute (Idx index, const SimEventAttribute &rAttr) |
| | Set simulation event attribute. More...
|
| |
| void | Alphabet (const sEventSet &rAlphabet) |
| | Set all simulation event attributes. More...
|
| |
| const sEventSet & | Alphabet (void) const |
| | Access alphabet (incl simulation event attributes) More...
|
| |
|
| TimedEvent | ExecuteNextTransition () |
| | Execute next transition. More...
|
| |
| const TimedEvent & | ProposeNextTransition () |
| | Propose next transition. More...
|
| |
| std::string | EventStatesToString (void) const |
| | Inspect stochastic event states (debugging) More...
|
| |
|
| virtual void | Reset (long int seed) |
| | Reset the ProposingExecutor. More...
|
| |
| virtual void | Reset (void) |
| | Reset the ProposingExecutor. More...
|
| |
| virtual void | Clear (void) |
| | Clear all data (generators, simulation attributes etc) More...
|
| |
| bool | ExecuteTime (Time::Type duration) |
| | Execute time duration. More...
|
| |
| bool | ExecuteEvent (Idx event) |
| | Execute event. More...
|
| |
| bool | ExecuteTransition (const TimedEvent &tevent) |
| | Execute event by transition. More...
|
| |
| bool | RevertToStep (Idx step) |
| | Revert executor to past step. More...
|
| |
| | LoggingExecutor (void) |
| | Construct an emtpy LoggingExecuter. More...
|
| |
| | LoggingExecutor (const LoggingExecutor &rOther) |
| | Copy constructor. More...
|
| |
| | LoggingExecutor (const std::string &rFileName) |
| | Construct from file. More...
|
| |
| virtual | ~LoggingExecutor (void) |
| | Explicit destructor. More...
|
| |
| virtual bool | Valid (void) const |
| | Check validity of executors. More...
|
| |
| Time::Type | CurrentTime (void) const |
| | Get clock time. More...
|
| |
| void | CurrentTime (Time::Type time) |
| | Set clock time. More...
|
| |
| int | CurrentStep (void) const |
| | Get logical time, ie number of transitions so far,. More...
|
| |
| void | CurrentStep (int step) |
| | Set logical time (# of steps) More...
|
| |
| bool | CurrentParallelTimedState (const ParallelTimedState &ptstate) |
| | Set current state of the ParallelExecutor. More...
|
| |
| const ParallelTimedState & | CurrentParallelTimedState (void) const |
| | Get current state of the ParallelExecutor. More...
|
| |
| void | LogOpen (TokenWriter &rTw, int mode) |
| | Start logging to TokenWriter. More...
|
| |
| void | LogOpen (const std::string &rFileName, int logmode, std::ios::openmode openmode=std::ios::out|std::ios::trunc) |
| | Start logging to file. More...
|
| |
| void | LogClose (void) |
| | Stop logging. More...
|
| |
| const SimConditionSet & | Conditions (void) const |
| | Read-only access to simulation conditions. More...
|
| |
| void | Conditions (const SimConditionSet &) |
| | Set all simulation conditions. More...
|
| |
| const AttributeSimCondition & | Condition (const std::string &rName) const |
| | Read-only access to a simulation condition by name. More...
|
| |
| const AttributeSimCondition & | Condition (Idx cond) const |
| | Read-only access to a simulation condition by index. More...
|
| |
| Idx | SetCondition (const std::string &rName, const AttributeSimCondition &rCondition) |
| | Set (or add) a condition by name. More...
|
| |
| void | SetCondition (Idx cond, const AttributeSimCondition &rCondition) |
| | Set a condition by index
More...
|
| |
| void | ClrCondition (const std::string &rName) |
| | Remove a condition by name
More...
|
| |
| void | ClrCondition (Idx cond) |
| | Remove a condition by index
More...
|
| |
| void | ConditionsWrite (TokenWriter &rTw, const std::string &rLabel="SimConditions") const |
| | Write conditions so labled section
More...
|
| |
| void | ConditionsRead (TokenReader &rTr, const std::string &rLabel="SimConditions") |
| | Read conditions from labled section
More...
|
| |
| ConditionIterator | ConditionsBegin (void) const |
| | Condition iterator: begin. More...
|
| |
| ConditionIterator | ConditionsEnd (void) const |
| | Condition iterator: end
More...
|
| |
| bool | BreakCondition (void) const |
| | Simulation state: true if some break condition is currently satisfied. More...
|
| |
| void | TraceClear (int length=-2) |
| | Clear buffer and set max buffer. More...
|
| |
| int | TraceLength (void) const |
| | Access buffer: current length. More...
|
| |
| TraceIterator | TraceBegin (void) const |
| | Condition iterator: begin. More...
|
| |
| TraceIterator | TraceEnd (void) const |
| | Condition iterator: end
More...
|
| |
| const TraceSample * | TraceAtTime (Time::Type time) const |
| | Access buffer: sample by faudes time (returns first sample) More...
|
| |
| const TraceSample * | TraceAtStep (int step) const |
| | Access buffer: sample by step. More...
|
| |
| const TraceSample * | TraceFirst (void) const |
| | Access buffer: first sample. More...
|
| |
| const TraceSample * | TraceRecent (void) const |
| | Access buffer: recent sample. More...
|
| |
| const TraceSample * | TraceCurrent (void) const |
| | Access buffer: current sample. More...
|
| |
| void | TraceWrite (TokenWriter &rTw, const TraceSample &sample) const |
| | Access buffer: tokenwriter output. More...
|
| |
| void | TraceWrite (const TraceSample &sample) const |
| | Access buffer: console output. More...
|
| |
| std::string | TraceToString (const TraceSample &sample) const |
| | Access buffer: convert to string. More...
|
| |
| void | TraceWrite (void) const |
| | Access buffer: console output (list all) More...
|
| |
| | ParallelExecutor (void) |
| | Construct an emtpy ParallelExecuter. More...
|
| |
| | ParallelExecutor (const ParallelExecutor &rOther) |
| | Copy constructor. More...
|
| |
| | ParallelExecutor (const std::string &rFileName) |
| | Construct from file. More...
|
| |
| virtual | ~ParallelExecutor (void) |
| | Explicit destructor. More...
|
| |
| Idx | Size (void) const |
| | Number of TimedGenerators. More...
|
| |
| void | Insert (const std::string &rFileName) |
| | Add a TimedGenerator from file. More...
|
| |
| void | Insert (const TimedGenerator &rGen) |
| | Add a TimedGenerator. More...
|
| |
| const EventSet & | Alphabet (void) const |
| | Overall alphabet. More...
|
| |
| Iterator | Begin (void) const |
| |
| Iterator | End (void) const |
| |
| const Executor & | At (int i) const |
| |
| Idx | EventIndex (const std::string &rName) const |
| | Event index lookup. More...
|
| |
| std::string | EventName (Idx index) const |
| | Event name lookup. More...
|
| |
| Time::Type | CurrentTime (void) const |
| | Get clock time. More...
|
| |
| int | CurrentStep (void) const |
| | Get logical time, ie number of transitions so far,. More...
|
| |
| bool | IsDeadlocked () const |
| | Test for deadlocked. More...
|
| |
| const ParallelTimedState & | CurrentParallelTimedState (void) const |
| | Get current state of the ParallelExecutor. More...
|
| |
| const ParallelState & | CurrentParallelState (void) const |
| | Get current discrete state vector of the ParallelExecutor. More...
|
| |
| const TimeInterval & | EnabledTime () const |
| | Get maximal duration that can pass without executing an event. More...
|
| |
| const EventSet & | EnabledEvents () const |
| | Get events that are enabled at current (timed) state. More...
|
| |
| const EventSet & | DisabledEvents () const |
| | Get events that are disabled at current (timed) state. More...
|
| |
| const TimeInterval & | EnabledInterval () const |
| | Get an interval on which the set of enabled events is constant. More...
|
| |
| TimeInterval | EnabledEventTime (Idx event) const |
| | Get interval on which the specified event is enabled. More...
|
| |
| TimeInterval | EnabledGuardTime (Idx event) const |
| | Get interval on which the respective guard is satisfied. More...
|
| |
| EventSet | ActiveEventSet (const ParallelState &stateVec) const |
| | Get events that are active in all TimedGenerators. More...
|
| |
| bool | Active (Idx ev, const ParallelState &stateVec) const |
| | Test whether an event is active in a given discrete state. More...
|
| |
| bool | Active (Idx ev) const |
| | Test whether an event is active at current (discrete) state. More...
|
| |
| std::string | PTSStr (const ParallelTimedState &ptstate) const |
| | Pretty printable string of timed parallel state. More...
|
| |
| std::string | PSStr (const ParallelState &pstate) const |
| | Pretty printable string of parallel state. More...
|
| |
| std::string | TEStr (const TimedEvent &tevent) const |
| | Pretty printable string of timed event. More...
|
| |
| std::string | CStr (Idx clock) const |
| | Pretty printable string of clock name. More...
|
| |
| std::string | EStr (Idx event) const |
| | Pretty printable string of event. More...
|
| |
| std::string | CurrentParallelTimedStateStr (void) const |
| | Pretty printable string of current state. More...
|
| |
| std::string | CurrentParallelStateStr (void) const |
| | Pretty printable string of parallel state
More...
|
| |
| void | ComputeEnabled (void) const |
| | Compute enabled events and enabled interval (fake const) More...
|
| |
| void | ComputeEnabledNonConst (void) |
| | Compute enabled core routine (non const) More...
|
| |
| | Type (void) |
| | Constructor. More...
|
| |
| | Type (const Type &rType) |
| | Copy constructor. More...
|
| |
| virtual | ~Type (void) |
| | Destructor. More...
|
| |
| virtual Type * | New (void) const |
| | Construct on heap. More...
|
| |
| virtual Type * | Copy (void) const |
| | Construct on heap. More...
|
| |
| virtual const Type * | Cast (const Type *pOther) const |
| | Cast other object to this type. More...
|
| |
| virtual Type & | Assign (const Type &rSrc) |
| | Assign configuration data from other object. More...
|
| |
| Type & | operator= (const Type &rSrc) |
| | Assign configurationdata from other object. More...
|
| |
| virtual bool | Equal (const Type &rOther) const |
| | Test equality of configuration data. More...
|
| |
| bool | operator== (const Type &rOther) const |
| | Test equality of configuration data. More...
|
| |
| bool | operator!= (const Type &rOther) const |
| | Test equality of configuration data. More...
|
| |
| virtual void | Name (const std::string &rName) |
| | Set the objects's name. More...
|
| |
| virtual const std::string & | Name (void) const |
| | Get objects's name. More...
|
| |
| virtual const std::string & | TypeName (void) const |
| | Get objects's type name. More...
|
| |
| void | Write (const Type *pContext=0) const |
| | Write configuration data to console. More...
|
| |
| void | Write (const std::string &pFileName, const std::string &rLabel="", const Type *pContext=0, std::ios::openmode openmode=std::ios::out|std::ios::trunc) const |
| | Write configuration data to a file. More...
|
| |
| void | Write (const std::string &pFileName, std::ios::openmode openmode) const |
| | Write configuration data to a file. More...
|
| |
| void | Write (TokenWriter &rTw, const std::string &rLabel="", const Type *pContext=0) const |
| | Write configuration data to TokenWriter. More...
|
| |
| virtual void | XWrite (const std::string &pFileName, const std::string &rLabel="", const Type *pContext=0) const |
| | Write configuration data to an XML file. More...
|
| |
| void | XWrite (const Type *pContext=0) const |
| | Write configuration data in XML format to concole Note: this write function uses the virtual function DoXWrite(), to be reimplemented by derived classes. More...
|
| |
| void | XWrite (TokenWriter &rTw, const std::string &rLabel="", const Type *pContext=0) const |
| | Write configuration data in XML format to TokenWriter. More...
|
| |
| std::string | ToString (const std::string &rLabel="", const Type *pContext=0) const |
| | Write configuration data to a string. More...
|
| |
| std::string | ToText (const std::string &rLabel="", const Type *pContext=0) const |
| | Write configuration data to a formated string. More...
|
| |
| void | DWrite (const Type *pContext=0) const |
| | Write configuration data to console, debugging format. More...
|
| |
| void | DWrite (const std::string &pFileName, const std::string &rLabel="", const Type *pContext=0, std::ios::openmode openmode=std::ios::out|std::ios::trunc) const |
| | Write configuration data to a file, debugging format. More...
|
| |
| void | DWrite (TokenWriter &rTw, const std::string &rLabel="", const Type *pContext=0) const |
| | Write configuration data in debug format to TokenWriter. More...
|
| |
| void | SWrite (TokenWriter &rTw) const |
| | Write statistics comment to TokenWriter. More...
|
| |
| void | SWrite (void) const |
| | Write statistics comment to console. More...
|
| |
| std::string | ToSText (void) const |
| | Write statistics to a string. More...
|
| |
| void | Read (const std::string &rFileName, const std::string &rLabel="", const Type *pContext=0) |
| | Read configuration data from file with label specified. More...
|
| |
| void | FromString (const std::string &rString, const std::string &rLabel="", const Type *pContext=0) |
| | Read configuration data from a string. More...
|
| |
| void | Read (TokenReader &rTr, const std::string &rLabel="", const Type *pContext=0) |
| | Read configuration data from TokenReader with label sepcified. More...
|
| |
Public Member Functions inherited from