Example: Many OO Clocks III
op mte : NEConfiguration -> TimeInf [frozen (1)] .
eq mte(C C’) = min(mte(C), mte(C’)) .
eq mte(< O : Clock | state : running,
value : R >) = EXERCISE!! .
eq mte(< O : Clock | state : stopped,
value : R >) = EXERCISE!! .
June 2, 2004
UFF
25
