A New Look at the Automatic Synthesis of Linear Ranking Functions