Formal controller synthesis for wastewater systems with signal temporal logic constraints: The Barcelona case study. (September 2018)