MACHINE TrainMovement1
  // use new CLP(FD) solver of ProB to solve non-linear equations over reals
CONSTANTS
  a /*@desc acceleration */,
  t /*@desc time */,
  v /*@desc speed */,
  s /*@desc distance travelled */
PROPERTIES
   v = a*t &
   s = 0.5 * a * t * t &
   a = 2.0 &
   t >= 0.0 & t <= 100.0 &
   v <= 10.0 & s>=25.0 // maximum s is 25.0 given v <= 10.0
DEFINITIONS
   SET_PREF_REAL_SOLVER == "precise_float_solver";
END