predicate simulated_annealing(float: initTemp, float: coolingRate) = let { var float: temp; } in if status()=START then temp = initTemp else temp = lastval(temp)*(1-coolingRate) /\ % cool down _objective < sol(_objective) - ceil(log(uniform(0.0,1.0)) * temp) endif;