module checkFixedSize [Addr, Data]
open fixedSizeMemory [Addr, Data] as memory
open fixedSizeMemory_H [Addr, Data] as fmemory
open abstractMemory [Addr, Data] as amemory


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

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

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

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

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