% Intermediate IOA for lazy lists proof
% This describes a set of processes acting on a shared set, with operations:
%   add(int key): boolean
%   rem(int key): boolean
%   cont(int key): boolean

% The idea behind this intermediate automaton is to be as close as possible to the abstract
% automaton, while allowing a forward simulation from the concrete automaton for the LazyList
% algorithm to the intermediate one.
%
% Because unsuccessful contains methods only recognise after the fact that the sought-after element
% was absent (present), the intermeditate automaton allows us to "observe" the absence of the 
% sought-after element, either at invocation time, or when the sought-after element is deleted while
% a cont method is searching for it, and to subsequently return false indicating that the value was
% not in the set.

IntAut: 
THEORY BEGIN

	importing basic_types
	importing IOA

	state: TYPE = [#
		pc:       [PROC -> pcval],
		seen_out: [PROC -> bool],
		keys: setof[Key]
	#]

	p,q: VAR PROC
	a: VAR state    %% a was not a great choice for the name of an intermediate state

	int_init: state = (# pc := (lambda p: idle), 
                             seen_out := (lambda p: false), 
		 	     keys := emptyset #)

	int_initial(a): bool = a = int_init


	pre_con(name: int?)(a): bool = 
       	cases name of
       		doAddT(k, p): NOT member(k, a`keys),
       		doAddF(k, p): member(k, a`keys),
       		doRemT(k, p): member(k, a`keys),
       		doRemF(k, p): NOT member(k, a`keys),
       		doContT(k, p): member(k, a`keys),
       		doContF(k, p): a`seen_out(p)
	else true
        endcases

	pcin(name: int?): pcval = 
        cases name of
        	add(k, p): idle,
        	doAddT(k, p): pcDoAdd(k),
        	doAddF(k, p): pcDoAdd(k),
        	addResp(r, p): pcAddResp(r),

        	rem(k, p): idle,
        	doRemT(k, p): pcDoRem(k),
        	doRemF(k, p): pcDoRem(k),
        	remResp(r, p): pcRemResp(r),

        	cont(k, p): idle,
        	doContT(k, p): pcDoCont(k),
        	doContF(k, p): pcDoCont(k),
        	contResp(r, p): pcContResp(r)
        endcases

    	pre(name: int?)(a): bool = pre_con(name)(a) and 
					a`pc(proc(name)) = pcin(name)

    	pcout(name: int?)(a: (pre(name))): pcval = 
        cases name of
        	add(k, p): pcDoAdd(k),
        	doAddT(k, p): pcAddResp(true),
        	doAddF(k, p): pcAddResp(false),
        	addResp(r, p): idle,

        	rem(k, p): pcDoRem(k),
        	doRemT(k, p): pcRemResp(true),
        	doRemF(k, p): pcRemResp(false),
        	remResp(r, p): idle,

        	cont(k, p): pcDoCont(k),
        	doContT(k, p): pcContResp(true),
        	doContF(k, p): pcContResp(false),
        	contResp(r, p): idle
        endcases

	main_eff(name: int?)(a: (pre(name))): state = 
        cases name of
        	doAddT(k, p): a with [keys := add(k, a`keys)],
        	doRemT(k, p): a with [keys := remove(k, a`keys),
                                      seen_out := (lambda q: a`seen_out(q) OR 
								a`pc(q) = pcDoCont(k))],
		cont(k, p): a with [seen_out := a`seen_out with [p := NOT member(k, a`keys)]]
            else a
        endcases


    	INT_IOA: TYPE = IOA[state, int?].IOA

    	eff(name: int?)(a: (pre(name))): state =
                    main_eff(name)(a) with 
			[pc := a`pc with [(proc(name)) := pcout(name)(a)]] 

    	int_ioa_inst: INT_IOA = (#
        	initial := int_initial,
        	pre := pre,
        	eff := eff
    	#)

    	AUTO_REWRITE+ add, doAddT, doAddF, addResp
    	AUTO_REWRITE+ rem, doRemT, doRemF, remResp
    	AUTO_REWRITE+ cont, doContT, doContF, contResp
    	AUTO_REWRITE+ int_ioa_inst
    	AUTO_REWRITE+ ext

END IntAut