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
}