fwd_sim_rel: THEORY
BEGIN

% The forward simulation says that keys and seen_out in the intermediate IOA are
% the same as in the concrete IOA (where they are kept as auxiliary variables).
% It also says that the pc values in the two IOA "correspond".  
% The definition of action_corr shows which steps in concaut correspond to
% actions in intaut.

  IMPORTING proc

  IMPORTING IntAut, ConcreteAut

  p, q: VAR PROC
  k: VAR Key
  i0, i1, i: VAR IntAut.state
  c0, c1, c: VAR ConcreteAut.state
  ca: VAR cc?
  actlist: VAR list[int?]
  n: VAR nat
  l0, l1, l2: VAR Node
  l: VAR ConcreteAut.pcval

  action_corr(ca, c0, c1, i1): list[int?] =
    LET p = proc(ca), k = c0`v(p) IN
      COND
        ext(ca) -> (: ca :),
        cont4F?(ca) -> (: doContF(k, p) :),
        cont5F?(ca) -> (: doContF(k, p) :),
        cont5T?(ca) -> (: doContT(k, p) :),
        add6?(ca) -> (: doAddT(k, p) :),
        add8?(ca) -> (: doAddF(k, p) :),
        rem3?(ca) -> (: doRemT(k, p) :),
        rem7?(ca) -> (: doRemF(k, p) :),
        ELSE -> (: :)
      ENDCOND

  fwd_sim_rel_data(c,i): bool =
    i`keys = c`aux_keys AND		% aux variables in conc aut accurately track
    i`seen_out = c`aux_seen_out		% corresponding ones in int aut

  fwd_sim_rel_step_corr(c, i): bool =
    forall p: i`pc(p) = CASES c`pc(p) OF

                          idle: idle,

                          pcCont1: pcDoCont(c`v(p)),
                          pcCont2: pcDoCont(c`v(p)),
                          pcCont3: pcDoCont(c`v(p)),
                          pcCont4: pcDoCont(c`v(p)),
                          pcCont5: pcDoCont(c`v(p)),
                          pcContResp(r): pcContResp(r),

                          pcAdd1: pcDoAdd(c`v(p)),
                          pcAdd2: pcDoAdd(c`v(p)),
                          pcAdd3: pcDoAdd(c`v(p)),
                          pcAdd4: pcDoAdd(c`v(p)),
                          pcAdd5: pcDoAdd(c`v(p)),
                          pcAdd6: pcDoAdd(c`v(p)),
                          pcAdd7: pcAddResp(true),
                          pcAdd8: pcDoAdd(c`v(p)),
                          pcAdd9: pcAddResp(c`res(p)),
                          pcAdd10: pcAddResp(c`res(p)),
                          pcAddResp(r): pcAddResp(r),

                          pcRem1: pcDoRem(c`v(p)),
                          pcRem2: pcDoRem(c`v(p)),
                          pcRem3: pcDoRem(c`v(p)),
                          pcRem4: pcRemResp(true),
                          pcRem5: pcRemResp(true),
                          pcRem6: pcRemResp(true),
                          pcRem7: pcDoRem(c`v(p)),
                          pcRem8: pcRemResp(c`res(p)),
                          pcRem9: pcRemResp(c`res(p)),
                          pcRemResp(r): pcRemResp(r)

                          % Pcloc#
                          ELSE IF c`ret_addr(p) = pcAdd2 THEN pcDoAdd(c`v(p)) 
                                                         ELSE pcDoRem(c`v(p)) ENDIF

                        ENDCASES

  fwd_sim_rel(c, i): bool =
    fwd_sim_rel_data(c, i) AND fwd_sim_rel_step_corr(c, i)

END fwd_sim_rel