M:Marking
〖dFT〗_s : enabled transitions set 〖FT〗_s ∪ 〖FT〗_stcp
〖FT〗_s :enabled Temporel Transition set
〖VT〗_s : Vald temporal transition set
Hl:clocks set
〖FT〗_stcp : enabled Coompound transition set
Initialize Marking(M)
Set clock(Hl)
State Construction (M)
Procedure dPFM (var 〖dFT〗_s , var M, var M_I,Var Hl)
〖dFT〗_s = ∅ 〖FT〗_stcp
if M ≥ B or M ≥B_tcp then
Firability (〖dFT〗_s)
〖FT〗_s ← Temporal Transition (〖dFT〗_s)
← CompoudTransition(〖dFT〗_s)
If 〖FT〗_s≠ ∅ then
〖VT〗_s← Validity (〖FT〗_s)
If 〖VT〗_s ≠∅ then
Firing (〖VT〗_s, M)
Sub (M_I, M)
ResetTimer(Hl(〖VT〗_s))
Else If 〖FT〗_stcp = ∅ then
setIncrementTimer(Hl(〖FT〗_s))
end if
Else If 〖FT〗_stcp ≠∅ then
StepSelection(〖FT〗_stcp)
Firing(〖dFT〗_(s ),M)
Sub(M_I,M)
End if
End if
End dPFM
Begin
initializeMarking(M)
Sub(M_I,M)
setTimer(Hl)
S_c0←StateConstruction(M_I)
IndexState ←0 IndexEdge ←0
Repeat
S_c← S_c∪ {S_cindexState}
T_indexEdge ←∅,W ←MI
Repeat
dPFM(〖dFT〗_s,M,M_I,Hl)
T_(indexEdge )= T_(indexEdge )∪{〖dFT〗_(s )}
until W ≠ M_I or T_indexEdge= ∅
if W ≠ M_I then
succ ←StateConstruction(M_I )
T←∪{T_(indexEdge )}
Rho (S_(cindexEdge ),T_indexEdge } ←succ
If (CheckDeadline(Succ)=True then
FinalState ←succ
〖 S〗_c← S_c∪ {FinalState}
endif
else
FinalState ←S_cindexState
Endif
indexState ← indexState+1
index Edge ← index Edge+1
until succ ∈ 〖 S〗_c or FinalState≠∅
end
Partager