fmod NAT-TIME is protecting NAT . sorts Time NzTime TimeInf . subsort NzTime < Time < TimeInf . op oo : -> TimeInf [ctor] . --- Infinity value subsort Nat < Time . subsort NzNat < NzTime . vars T T' : Time . --- extend operators to infinity: op _<=_ : Time TimeInf -> Bool [ditto] . eq T <= oo = true . op min : TimeInf TimeInf -> TimeInf [ditto] . eq min(oo, TI:TimeInf) = TI:TimeInf . vars N N' : Nat . op _monus_ : TimeInf Time -> TimeInf . eq N monus N' = if N' <= N then sd(N, N') else 0 fi . eq oo monus N = oo . endfm fmod POSITIVE-RAT is protecting RAT . sort NNegRat . --- non-negative rationals! subsorts Zero PosRat Nat < NNegRat < Rat . endfm fmod POSRAT-TIME is protecting POSITIVE-RAT . protecting NAT-TIME . subsort NNegRat < Time . subsort PosRat < NzTime . vars R R' : NNegRat . eq R monus R' = if R > R' then R - R' else 0 fi . endfm load full-maude (omod OO-TIMED-PRELUDE is including NAT-TIME . sorts GlobalState ClockedState . subsort GlobalState < ClockedState . op `{_`} : Configuration -> GlobalState [format (g o g so)] . op _in`time_ : GlobalState Time -> ClockedState [format (o g g y o)] . eq (CLS:ClockedState in time R:Time) in time R':Time = CLS:ClockedState in time (R:Time + R':Time) . endom) --- Different OO clocks: --- 1. single clock --- 2. multiple clocks --- 3. multiple skewed clocks, with rationals (omod SINGLE-CLOCK is including OO-TIMED-PRELUDE . protecting NAT-TIME . class Clock | state : ClockState, time : Time . sort ClockState . ops running stopped : -> ClockState [ctor] . var C : Oid . var T : Time . --- Tick rules: crl [tickOneRunning] : {< C : Clock | state : running, time : T >} => {< C : Clock | time : T + 1 >} in time 1 if T < 12 . rl [tickOneStopped] : {< C : Clock | state : stopped >} => {< C : Clock | >} in time 1 . --- Instantaneous rules: rl [jumpToZero] : < C : Clock | state : running, time : 12 > => < C : Clock | time : 0 > . rl [batteryDies] : < C : Clock | state : running > => < C : Clock | state : stopped > . op genta : -> Oid [ctor] . endom) (rew [100] {< genta : Clock | state : running, time : 0 >} .) ---(search [1] {< genta : Clock | state : running, time : 0 >} =>* {< genta : Clock | state : stopped >} in time N:Nat .) ---(search [1] {< genta : Clock | state : running, time : 0 >} =>* {< genta : Clock | state : stopped, time : 13 >} in time N:Nat .) --- 2. Multiple standard retrograde clocks. (omod MANY-CLOCKS is including OO-TIMED-PRELUDE . protecting NAT-TIME . class Clock | state : ClockState, time : Time . sort ClockState . ops running stopped : -> ClockState [ctor] . var C : Oid . var T T' : Time . var SYSTEM CONF1 CONF2 : Configuration . --- Tick rules: crl [tickOne] : {SYSTEM} => {timeEffect(SYSTEM, 1)} in time 1 if 1 <= mte(SYSTEM) . --- Instantaneous rules: rl [jumpToZero] : < C : Clock | state : running, time : 12 > => < C : Clock | time : 0 > . rl [batteryDies] : < C : Clock | state : running > => < C : Clock | state : stopped > . op timeEffect : Configuration Time -> Configuration [frozen (1)] . eq timeEffect(none, T) = none . ceq timeEffect(CONF1 CONF2, T) = timeEffect(CONF1, T) timeEffect(CONF2, T) if CONF1 =/= none and CONF2 =/= none . eq timeEffect(< C : Clock | state : running, time : T >, T') = < C : Clock | state : running, time : T + T' > . eq timeEffect(< C : Clock | state : stopped >, T') = < C : Clock | > . op mte : Configuration -> TimeInf [frozen (1)] . eq mte(none) = oo . ceq mte(CONF1 CONF2) = min(mte(CONF1), mte(CONF2)) if CONF1 =/= none and CONF2 =/= none . eq mte(< C : Clock | state : running, time : T >) = 12 monus T . eq mte(< C : Clock | state : stopped >) = oo . ops ap genta dubuis seiko jlc : -> Oid [ctor] . op clocks : -> Configuration . eq clocks = < ap : Clock | state : running, time : 0 > < genta : Clock | state : running, time : 0 > < dubuis : Clock | state : running, time : 0 > < seiko : Clock | state : running, time : 0 > < jlc : Clock | state : running, time : 0 > . endom) (rew [100] {clocks} .) (rew [100] {< ap : Clock | state : running, time : 0 > < dubuis : Clock | state : running, time : 0 > < seiko : Clock | state : running, time : 0 >} .) --- 3. Many skewed clocks: (omod MANY-SKEWED-CLOCKS is including OO-TIMED-PRELUDE . protecting POSRAT-TIME . class Clock | state : ClockState, time : Time, rate : PosRat . sort ClockState . ops running stopped : -> ClockState [ctor] . var C : Oid . var T T' : Time . var SYSTEM CONF1 CONF2 : Configuration . var RATE : PosRat . --- Tick rules: crl [tickOne] : {SYSTEM} => {timeEffect(SYSTEM, min(1000, mte(SYSTEM)))} in time min(1000, mte(SYSTEM)) if mte(SYSTEM) =/= 0 . --- Instantaneous rules: rl [jumpToZero] : < C : Clock | state : running, time : 12 > => < C : Clock | time : 0 > . rl [batteryDies] : < C : Clock | state : running > => < C : Clock | state : stopped > . op timeEffect : Configuration Time -> Configuration [frozen (1)] . eq timeEffect(none, T) = none . ceq timeEffect(CONF1 CONF2, T) = timeEffect(CONF1, T) timeEffect(CONF2, T) if CONF1 =/= none and CONF2 =/= none . eq timeEffect(< C : Clock | state : running, time : T, rate : RATE >, T') = < C : Clock | state : running, time : T + (T' * RATE) > . eq timeEffect(< C : Clock | state : stopped >, T') = < C : Clock | > . op mte : Configuration -> TimeInf [frozen (1)] . eq mte(none) = oo . ceq mte(CONF1 CONF2) = min(mte(CONF1), mte(CONF2)) if CONF1 =/= none and CONF2 =/= none . eq mte(< C : Clock | state : running, time : T, rate : RATE >) = (12 monus T) / RATE . eq mte(< C : Clock | state : stopped >) = oo . ops ap genta dubuis seiko jlc : -> Oid [ctor] . op clocks : -> Configuration . eq clocks = < ap : Clock | state : running, time : 0, rate : 1/2 > < dubuis : Clock | state : running, time : 0, rate : 1 > < seiko : Clock | state : running, time : 0, rate : 1 > < jlc : Clock | state : running, time : 0, rate : 5/6 > . endom) --- seems to work! (rew [100] {clocks} .) *** Exercise 1: many non-skewed clocks, but with minutes, seconds, and hours. *** Can also stop at any time *** Exercise 2: --- In population, assume that everyone has birthday Jan 1, when a new year --- starts. Time unit = year. Define aging for populations, so --- that a. time advance by one year in each step --- b. nobody can get older than 1000 years --- c. everybody must marry (or drop the enganement) --- the same year that they become enganged. *** RTT protocol. Simple protocol. One guy wants to find the RTT to another *** guy. If the RTT is < 10, then fine; else he starts a new round ...: load messages (omod FIND-RTT is including OO-TIMED-PRELUDE . protecting NAT-TIME . including MESSAGE-LOSS . --- message wrapper plus lose messages class Sender | time : Time, rtt : Time, resendTimer : TimeInf, receiver : Oid . class Receiver . ops rttReq rttReply : Time -> MsgContent [ctor] . vars T T' T1 T2 : Time . var TI : TimeInf . vars S R O1 O2 : Oid . vars CONF1 CONF2 SYSTEM : Configuration . var MC : MsgContent . --- Send request with own time, and reset timer to 10: rl [sendRequest] : < S : Sender | time : T, resendTimer : 0, receiver : R > => < S : Sender | resendTimer : 10 > (msg rttReq(T) from S to R) . --- receive rttReply with rtt < 10; then a. record rtt, b. stop timer rl [recReply] : (msg rttReply(T1) from R to S) < S : Sender | time : T2 > => if (T2 monus T1) < 10 then < S : Sender | rtt : T2 monus T1, resendTimer : oo > else < S : Sender | > fi . *** just ignore message --- receiver can get message and then then just replies with the same timestamp --- it received: rl [reply] : (msg rttReq(T) from S to R) < R : Receiver | > => < R : Receiver | > (msg rttReply(T) from R to S) . --- standard OO tick rule: crl [tick] : {SYSTEM} => {timeEffect(SYSTEM, 1)} in time 1 if 1 <= mte(SYSTEM) . op timeEffect : Configuration Time -> Configuration [frozen (1)] . eq timeEffect(none, T) = none . ceq timeEffect(CONF1 CONF2, T) = timeEffect(CONF1, T) timeEffect(CONF2, T) if CONF1 =/= none and CONF2 =/= none . eq timeEffect(< S : Sender | time : T1, resendTimer : TI >, T2) = < S : Sender | time : T1 + T2, resendTimer : TI monus T2 > . eq timeEffect(< R : Receiver | >, T) = < R : Receiver | > . eq timeEffect(msg MC from O1 to O2, T) = (msg MC from O1 to O2) . op mte : Configuration -> TimeInf [frozen (1)] . eq mte(none) = oo . ceq mte(CONF1 CONF2) = min(mte(CONF1), mte(CONF2)) if CONF1 =/= none and CONF2 =/= none . eq mte(< S : Sender | resendTimer : TI >) = TI . eq mte(< R : Receiver | >) = oo . eq mte(msg MC from O1 to O2)= oo . ops snd rec : -> Oid [ctor] . op init : -> Configuration . eq init = < snd : Sender | time : 0, rtt : 0, resendTimer : 0, receiver : rec > < rec : Receiver | > . endom) (rew [200] {init} .) (search [1] {init} =>* {< snd : Sender | rtt : 7 > REST:Configuration} in time N:Nat .) (omod SINGLE-CLOCK-NO-GLOBAL-CLOCK is including SINGLE-CLOCK . var GS : GlobalState . var T : Time . eq GS in time T = GS . endom) (rew [1000] {< genta : Clock | state : running, time : 0 >} .) (search [1] {< genta : Clock | state : running, time : 0 >} =>* {< genta : Clock | time : T:Time >} such that T:Time > 12 .) ***( *** REST of SECTION: msg delay frameworks: op delay : Msg Time -> DlyMsg [right id: 0] . subsort Msg < DlyMsg . --- SEND message delay(msg ... from X to Y, delay) --- READ message (msg ... from X to Y) --- eq timeEffect(delay(MSG, T), T2) = delay(MSG, T monus T2) . *** is all, no equation needed for the undelayed message case; why not --- mte --- version 1: must read the message exactly when its delay has expired: mte(delay(MSG, T)) = T . --- again: no def needed for the undelayed msg case --- version 2: delay is the minumum message delay: mte(delay(MSG, T)) = oo . *** Exercise: how would you model communication *** in which the messaging delay could be any value *** in the interval [minDelay, maxDelay]??? *** Exercise: do the timed version of 2PC. That is, now also *** the prepare message and the OK/notOK message could get lost *** (but maybe for simplicity of analysis can not get lost abort/commit *** cannot get lost). When the coordintaor sends the prepare messages, *** it also sets a timer, to, say, 10. If some messages have not arrived *** when the timer expires, the cordinator assumes not OK *** and immediately sends out the decision; ASAP. *** Exercise 2b: analyze the solution. Hoever, this system is *** nonterminating (why?), and infinite reachable state space *** (why?). Therefore search for states reachable in time *** 10 or more, such that the states there are "consistent" *** (maybe you need take the abort/commit messages into account ...) *** Then: --- redefine _in time_ so that it does not carry the clock ... --- explain advantages ... *** Then: --- timed temporal logic; just standard version ... *** Then: Real-Time Maude: --- builds in a lot of infrastructre and different time domains. --- supports both "clocked" and "unclocked" systems --- both constant-ticks and event-based simulation --- Analysis: (trew {init} in time <= 1000 .) (tsearch {init} =>* pattern such that in time <= 100 .) - can also search for states reachable AFTER a certain time, - and states reachable in a time interval [lower, upper] (utsearch ... ) --- unclocked --- clocked and unclocked model checking --- metric CTL model checking ... and timed LTLR model checker --- under development (?) --- mention incompleteness of analysis: for RAT, cannot reach a clock --- with value 11/17, I think, even though this should be reachable --- discrete time: no problem --- dense time: can often have sound and complete analysis WRLA 06 --- Apps: large IETF, wireless sensor networks, cloud storage systems, etc. --- real-time modeling languages such as ... --- useful also for performance estimation, eg WSN (omod SINGLE-CLOCK-NO-GLOBAL-CLOCK is including SINGLE-CLOCK . var GS : GlobalState . var T : Time . eq GS in time T = GS . endom) (rew [1000] {< genta : Clock | state : running, time : 0 >} .) (search [1] {< genta : Clock | state : running, time : 0 >} =>* {< genta : Clock | time : T:Time >} such that T:Time > 12 .)