channel CIO_Signup{ out accounts(adb:Map, signUp(aid:Str, name:Str)) = insert(adb, aid, {"name": name}) } channel CIO_ChangeName(aid:Str) { out accounts.{aid}.name(prev_name:Str, changeName(name)) = name } channel CIO_CreateRoom { out rooms(rdb:Map, createRoom(rid:Str, blue_id:Str, red_id:Str)) = insert(rdb, rid, {"blue_id": blue_id, "red_id": red_id}) } channel CIO_ChangeRed_id(rid:Str) { out rooms.{rid}.red_id(prev_red_id:Str, changeRed_id(red_id)) = red_id } channel CIO_ChangeBlue_id(rid:Str) { out rooms.{rid}.blue_id(prev_blue_id:Str, changeBlue_id(blue_id)) = blue_id } channel C_red(rid:Str) { in rooms.{rid}.red_id(prev_aid:Str, sync(aid, name)) = aid in accounts.{aid}.name(prev_name:Str, sync(aid, name)) = name out rooms.{rid}.red_name(prev_name:Str, sync(aid, name)) = name } channel C_blue(rid:Str) { in rooms.{rid}.blue_id(prev_aid:Str, sync(aid, name)) = aid in accounts.{aid}.name(prev_name:Str, sync(aid, name)) = name out rooms.{rid}.blue_name(prev_name:Str, sync(aid, name)) = name }