MACHINE
  StateSystem
REFINES
  System
SEES
  StateSystemCtx
VARIABLES
  t
  x_p
  x_s
INVARIANTS
  inv1: x_s : STATES
EVENTS
  INITIALISATION
  THEN
    act1: t := Rzero
    act2: x_p :: RRealPlus --> S
    act3: x_s :: STATES
  END

  Progress
  REFINES Progress
  THEN
    act1: t :| t' : RRealPlus & (t |-> t' : lt)
  END

  Behave
  REFINES Behave
  ANY
    e
  WHERE
    grd1: e : DE(S)
    grd2: Solvable(Closed2Infinity(t),e)
  THEN
    act1: x_p :| x_p' : RRealPlus --> S & AppendSolutionBAP(e,RRealPlus,Closed2Open(Rzero,t),Closed2Infinity(t),x_p,x_p')
  END

  Transition
  ANY
    s
  WHERE
    grd1: s : POW1(STATES)
  THEN
    act1: x_s :: s
  END

END