module cacheMemory [Addr, Data]

sig CacheSystem {
	main, cache: Addr -> lone Data
	}

pred init (c: CacheSystem) {
	no c.main + c.cache
	}

pred write (c, c': CacheSystem, a: Addr, d: Data) {
	c'.main = c.main
	c'.cache = c.cache ++ a -> d
	}

pred read (c: CacheSystem, a: Addr, d: Data) {
	some d
	d = c.cache [a]
	}

pred load (c, c': CacheSystem) {
	some addrs: set c.main.Data - c.cache.Data |
		c'.cache = c.cache ++ addrs <: c.main
	c'.main = c.main
	}

pred flush  (c, c': CacheSystem) {
	some addrs: some c.cache.Data {
		c'.main = c.main ++ addrs <: c.cache
		c'.cache = c.cache - addrs -> Data
		}
	}

assert LoadNotObservable {
	all c, c', c": CacheSystem, a1, a2: Addr, d1, d2, d3: Data |
		{
		read (c, a2, d2)
		write (c, c', a1, d1)
		load (c', c")
		read (c", a2, d3)
		} implies d3 = (if a1 = a2 then d1 else d2)
	}
check LoadNotObservable

assert FlushNotObservable {
	all c, c', c": CacheSystem, a1, a2: Addr, d1, d2, d3: Data |
		{
		read (c, a2, d2)
		write (c, c', a1, d1)
		flush (c', c")
		read (c", a2, d3)
		} implies d3 = (if a1 = a2 then d1 else d2)
	}
check FlushNotObservable

assert WriteFlushRead {
	all c, c', c": CacheSystem, a: Addr, d1, d2: Data |
		write (c, c', a, d1) and flush (c', c") and  read (c", a, d2) => d1 = d2
	}
check WriteFlushRead