XBT_INFO("Displaying workstation %s", SD_workstation_get_name(ws));
XBT_INFO(" - power: %.0f", SD_workstation_get_power(ws));
XBT_INFO(" - available power: %.2f", SD_workstation_get_available_power(ws));
XBT_INFO("Displaying workstation %s", SD_workstation_get_name(ws));
XBT_INFO(" - power: %.0f", SD_workstation_get_power(ws));
XBT_INFO(" - available power: %.2f", SD_workstation_get_available_power(ws));