fmod TRAFFIC is
    protecting INT .
    
    sort Light .
    
    op Red : -> Light .
    op Green : -> Light .
    op Yellow : -> Light .
    op RedYellow : -> Light .
    
    op TRAFFIC : Int Light -> Light .
    op next : Light -> Light .
    
    var t : Int .
    var l : Light .
    
    eq TRAFFIC(0, l) = l .
    ceq TRAFFIC(t, l) = next(TRAFFIC(t - 1, l)) if t > 0 .
    
    eq next(Green) = Yellow .
    eq next(Yellow) = Red .
    eq next(Red) = RedYellow .
    eq next(RedYellow) = Green .
endfm