String (String name) { String result = mySlotNames.get(name); if (result == null) { result = name.replace("/", "."); final int idx = result.indexOf("$"); if (idx >= 0) { result = result.substring(0, idx); } mySlotNames.put(name, result); } return result; }