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 .)