Formal Specification of XFD-DEVS |
Natural Language for XFD-DEVS |
Downloads |
References |
Working with GUI | Example |
XFD-DEVS
Parameter |
DEVS
Specifications |
Comment |
incomingMessageSet |
x
= {(inMsg, Msg):Msg €
incomingMessageSet} |
for
each incoming message, Msg, we construct an input port inMsg and allow
Msg as the only value on it |
outgoingMsgSet |
Y = {(inMsg,Msg): Msg € outgoingMessageSet}b | For
each outgoing message, Msg we construct an output port outMsg and allow
Msg as the only value on it. Bags of such message output are allowed.
They can be constructed by providing rows in the internal transition
table having different output paths for the same transition |
StateSet |
S = {(phase,sigma):phase € StateSet and sigma € R0,∞+ } | States
in XFD-DEVS become phases in DEVS and have an associated time advance
value, sigma |
TimeAdvanceTable: StateSet → R0,∞+ | ta: S→ R0,∞+ ,where ta(phase,sigma) = sigma. | The
TimeAdvanceTable in XFD-DEVS is used to assign initial sigma values in
DEVS as is seen below. |
InternalTransitionTable: StateSet → StateSet |
δint: S→ S ,where δint (phase,sigma) = (phase’, TimeAdvanceTable(phase’)). where phase’ = InternalTransitionTable(phase) |
The InternalTransitionTable in XFD-DEVS determines the phase of the next phase in DEVS while the TimeAdvanceTable determines the initial value of sigma in this phase. |
ExternalTransitionTable: StateSet × incomingMessageSet → StateSet |
δext: Q×X → S ,where δext (phase,sigma,e,(inMsg,Msg)) = (phase’,TimeAdvanceTable(phase’)). where phase’ = ExternalTransitionTable(phase,Msg) provided that ExternalTransitionTable(phase,Msg) is defined. otherwise, δext (phase,sigma,(inMsg,Msg)) = (phase, sigma – e) |
When it is defined, the ExternalTransitionTable in XFD-DEVS determines the phase of the next state in DEVS while the TimeAdvanceTable determines the initial value of sigma in this state. We say that the ExternalTransitionTable is defined for a state and incoming message when there is an entry in the table for that pair. Thus, when you don’t provide a next state for a particular combination of states and inputs in XFD-DEVS, it is interpreted in the DEVS model as an order to ignore the input and continue in the state to the original transition time. |
δcon: Q×X → S is not specified by XFD-DEVS | The confluent function must be specified by the modeler in the DEVS model constructed from XFD-DEVS | |
OutputTable: StateSet → 2outgoingMsgSet |
ŷ:S → Yb where ŷ(phase,sigma) = {(outMsg,Msg): Msg € OutputTable(phase)} |
The output in the DEVS model is obtained by applying the XFD-DEVS output table to the phase component of the DEVS model state. The resulting value could be the empty set, in which case no output is emitted, a single value, or multiple values, in which case, a bag of values is constructed. |
Schedule preserving incoming message, Msg |
δext:
Q×X → S ,where
δext
(phase,sigma,e,(inMsg,Msg)) = where phase’ =
ExternalTransitionTable(phase,Msg) δext
(phase,sigma,(inMsg,Msg)) = |
When
it is defined for a schedule preserving input, the ExternalTransitionTable
in XFD-DEVS determines an immediate transition to the phase of the next state in DEVS with the next transition scheduled at the original transition time. Otherwise, it is interpreted in the DEVS model as an order to ignore the input and continue in the state to the original transition time. |
Natural
Language Phrase |
XFD-DEVS Specification |
Example |
to
start hold in PHASE for time SIGMA! where SIGMA is 0, a positive real, or the symbol Infinity (other variants such as Inf are allowed) |
TimeAdvanceTable(PHASE)
= SIGMA and also set PHASE as initial state |
to
stat hold in waitForJob for time Infinitiy! This can also be expressed as: to start passivate in waitForJob! |
hold
in PHASE for time SIGMA where SIGMA = 0, a positive real, or the symbol Infinity(other variants such as Inf are allowed) |
TimeAdvanceTable(PHASE)=SIGMA |
hold
in sendOut for time 0.1 ! |
after
PHASE then output MSG! |
OutputTable(PHASE)
= MSG |
after
sendOut then output Job ! |
from
PHASE go to PHASE! |
InternalTransitionTable(PHASE)
= PHASE' |
from
sendOut go to waitForJob ! |
when
in PHASE and receive MSG go to PHASE'! |
ExternalTransitionTable(PHASE,MSG)
= PHASE' |
when
in waitForJob and receive Job go to processing! |
when in PHASE and receive MSG go to PHASE’ eventually ! | ExternalTransitionTable(PHASE,
MSG) = PHASE' with a mark to note that this input is schedule-preserving in this state |
when in waitForJob and receive Job go to processing eventually ! |
You can define internal transitions for any of the defined states by hitting the Default Internal State Machine Specifications button, as shown in Figure 3. The drop down menus display such states (that were defined in the Time Advance Table). Enter the transition from passive to passive first since this will make passive the initial state for the model – the state that it starts in. In general, the startin state of the row in the table having the number 1 will be taken as the model’s initial state.
Finally, Figure 4 shows how external input
transitions are
specified. You can enter an incoming message name and select a start
state, an
end state, and optionally, an output message for the end state. Note
that you
can also enter output messages for transitions in the internal
transition table
for any states not covered in the external transition table. For example, when the model is in passive, an
incoming job message will send it to processing where it will stay for
the
prescribed time and then output the job. You will have already prescribed the residence time
the Time Advance table since the latter
table only include states in the drop
down menus that have been entered in that table. The transition out of
processing is prescribed in the internal transition table, e.g.,
processing to
passive, and the output message after processing can be entered there
as well,
but both have to agree.
Figures 5 and 6 show the XML and Java codes that are generated when the Generate FDDevs button is pressed. The XML specification, proc.xml, corresponds to the formal specification of the model and contains all the information you have entered in a form that is easily understood and processed. The Java model, proc.java, is ready to run in package Models.java within DEVSJAVA.