init{
    weather := 0
    logger := "not_started"
}

channel CIO1{
    out weather(time:Int, timePasses(nil)) == mod(time + 1,4)
}

channel CIO2{
    out orcs(o:Int, update(weather)) == weather
    out hobbits(h:Int, update(weather)) == weather
}

channel C1{
    in weather(w:Int, update(weather)) == weather
    out orcs(o2:Int, update(weather)) == weather
    out hobbits(h2:Int, update(weather)) == weather
}