back_sim_rel: THEORY
BEGIN

	IMPORTING proc

	IMPORTING AbstractAut, IntAut

	p,q: VAR PROC
	k: VAR Key
	a0, a1, a: VAR AbstractAut.state
	i0, i1, i: VAR IntAut.state
	ia: VAR int?
	actlist: VAR list[ab?]
	n: VAR nat

	%% In the backwards simulation, we always do the same action in the abstract as the
	%% intermediate does, except that we skip the doContF action, which is instead done
        %% at either the cont action or a doRem action of another process.

	betweenDoCont(i,a,k,p): bool =
		i`pc(p) = pcDoCont(k) AND i`seen_out(p) AND a`pc(p) = pcContResp(false)

	remlist(i1, a1, k, n): RECURSIVE list[ab?] = 
		IF n >= NUMPROC THEN null
			ELSE IF betweenDoCont(i1,a1,k,n) 
				THEN cons(doContF(k, n), remlist(i1,a1,k,n+1))
				ELSE remlist(i1,a1,k,n+1)
			ENDIF
		ENDIF
	MEASURE (lambda (i1, a1, k, n): IF n > NUMPROC THEN 0 ELSE NUMPROC - n ENDIF)

	action_corr(ia, i0, i1, a1): list[ab?] =
		cases ia of
			doContF(k, p): null,
                        cont(k, p): (IF a1`pc(p) = pcContResp(false) THEN 
					(: ia, doContF(k, p) :) ELSE (: ia :) ENDIF),
			doRemT(k, p): cons(ia, remlist(i1,a1,k,0))
		else (: ia :)
		endcases			


	% This constructs a state with the right program counter for the first action in 
  	% the list of actions to be applied in the abstract automaton.  For many cases, this is
	% sufficient to construct the right prestate, and it is always necessary

	simple_prestate(a1, actlist): AbstractAut.state =
		IF actlist = null THEN 
			a1 
		ELSE
			a1 WITH [pc := a1`pc WITH [(proc(car(actlist))) := 
				AbstractAut.pcin(car(actlist))]]
		ENDIF

	% In most cases, we just need to update the program counter to be the one required
	% by the first action in the list of actions to be applied in the abstract automaton.
	% For the two actions that modify the set, we need to "undo" the changes they make 
	% in order to make the precondition of the action hold in the prestate

	bk_sim_prestate(ia, i0, i1, a1, actlist): AbstractAut.state = 
		cases ia of
			doAddT(k, p): simple_prestate(a1 WITH [keys := remove(k, a1`keys)], actlist),
			doRemT(k, p): simple_prestate(a1 WITH 
							[keys := add(k, a1`keys),
							 pc := (lambda q: IF betweenDoCont(i1,a1,k,q)
										THEN pcDoCont(k) 
										ELSE a1`pc(q) ENDIF) ], 
							actlist)
		else simple_prestate(a1, actlist)
		endcases			
	
	back_sim_rel_data(i, a): bool = i`keys = a`keys 

	back_sim_rel_step_corr(i, a): bool =
		forall p: (i`pc(p) = a`pc(p) OR
				% (exists k: betweenDoCont(i,a,k,p))
				(pcDoCont?(i`pc(p)) AND a`pc(p) = pcContResp(false) AND i`seen_out(p)))

	back_sim_rel(i, a): bool = 
		back_sim_rel_data(i, a)	AND back_sim_rel_step_corr(i,a)
		
END back_sim_rel