/* for now, incorporate basicMemory_H here until bug is fixed */

module checkBasic [Addr, Data]
open fixedSizeMemory [Addr, Data] as fmemory
open abstractMemory [Addr, Data] as amemory

sig Memory_H extends fmemory/Memory {
	unwritten: set Addr
	}

pred init_H (m: Memory_H) {
	fmemory/init (m)
	m.unwritten = Addr
	}

pred read_H (m: Memory_H, a: Addr, d: Data) {
	fmemory/read (m, a, d)
	}

pred write_H (m, m': Memory_H, a: Addr, d: Data) {
	fmemory/write (m, m', a, d)
	m'.unwritten = m.unwritten - a
	}

/* define abstraction function from history-extended concrete state to abstract state */

/* to see how this works, change to
	am.data = fm.data
and not that InitOK now fails
*/


pred alpha (fm: fmemory/Memory, am: amemory/Memory) {
	am.data = fm.data - (fm.unwritten -> Data)
	}

assert initOK {
	all fm: Memory_H, am: amemory/Memory |
		init_H (fm) and alpha (fm, am) =>  amemory/init (am)
	}
check initOK

assert readOK {
	all fm: Memory_H, a: Addr, d: Data, am: amemory/Memory |
		read_H (fm, a, d) and alpha (fm, am) => amemory/read (am, a, d)
	}
check readOK

assert writeOK {
	all fm, fm': Memory_H, a: Addr, d: Data, am, am': amemory/Memory |
		write_H (fm, fm', a, d) and alpha (fm, am) and alpha (fm', am')
 		implies amemory/write (am, am', a, d)
	}
check writeOK