MACHINE
  Generic
SEES
  GenericCtx
VARIABLES
  t
  x_p
  x_s
INVARIANTS
  inv1: t : RRealPlus
  inv2: x_p : RReal +-> S
  inv3: Closed2Closed(Rzero,t) <: dom(x_p)
  inv4: x_s : STATES
EVENTS
  INITIALISATION
  THEN
    act1: t := Rzero
    act2: x_p :: { Rzero } --> S
    act3: x_s :: STATES
  END

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

  Sense
  ANY
    s
    p
  WHERE
    grd1: s : POW1(STATES)
    grd2: p : POW(STATES*RReal*S)
    grd3: (x_s |-> t |-> x_p(t)) : p
  THEN
    act1: x_s :: s
  END

  Behave
  ANY
    tp
    e
    Inv
  WHERE
    grd0: tp : RRealPlus & t |-> tp : lt
    grd1: e : DE(S)
    grd2: Solvable(Closed2Closed(t,tp),e)
    grd3: Inv <: S
  THEN
    act1: t,x_p :| x_p' : RReal +-> S & t' = tp & Closed2Closed(Rzero,t') <: dom(x_p') & CBAPsolutionOf(t,t',x_p,x_p',e,Inv)
  END

  Actuate
  ANY
    tp
    e
    s
    Inv
  WHERE
    grd0: tp : RRealPlus & t |-> tp : lt
    grd1: e : DE(S)
    grd2: Solvable(Closed2Closed(t,tp),e)
    grd3: s <: STATES
    grd4: x_s : s
    grd5: Inv <: S
  THEN
    act1: t,x_p :| x_p' : RReal +-> S & t' = tp & Closed2Closed(Rzero,t') <: dom(x_p') & CBAPsolutionOf(t,t',x_p,x_p',e,Inv)
  END

END