Newer
Older
AlgebraicDataflowArchitectureModel / AlgebraicDataflowArchitectureModel / models / OnlineBattleGame.model
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
}