// Signature: Buffer with a relation
// contains that identifies 
// the set of locations that are contained in the buffer
sig Buffer {
	start: one StartLocation,
	end: one EndLocation,
	contains: set Location,
	//allocatedTo: one MemoryArea
}

//abstract sig MemoryArea {}

//sig Stack, Heap, Static extends MemoryArea {}


sig Location { 
	partof: set Buffer,
	previousLocation: lone Location,
	nextLocation: lone Location,
	position: lone Int
}

// There exists a start
one sig StartLocation extends Location { } 
{ 	no previousLocation 
	position = 1
}

// There exists a end
one sig EndLocation extends Location { } { no nextLocation }

// A Location pointed to by nextLocation from a Location has a previousLocation relationship with the latter 
fact { all l1: Location, l2: l1.nextLocation | l2.previousLocation = l1 }

// A Location pointed to by nextLocation from a Location has a position value that is greater that one 
fact { all l1: Location, l2: l1.nextLocation | l2.position = l1.position.plus[1] }

// A Location allways has a positive position
fact { all l: Location | l.position > 0 }

// No two Locations have the same position
fact { all l,l': Location | disj[l,l'] implies disj [l.position, l'.position] }


fact { 
	all l: Location, b: Buffer | 
				l in b.start.*nextLocation iff l in b.contains
						

		all l: Location, b: Buffer | 
				l in b.start implies 
						l in b.contains

		all l: Location, b: Buffer | 
				l in b.end implies 
						l in b.contains
}

fact {
	//partof relation is the inverse of contains
	partof = ~contains
}

// Signature: Software with a relation
// performsOperation that captures a 
// software operation on a buffer at a set of locations
sig Software{
	performsOperation: Buffer set -> set Location
}

// Predicate: Operate that captures a 
// software operation on a stack-based buffer at a location
// This predicate also allows us to confirm that the model produces valid instances
pred operate [s: Software, b: Buffer, l: Location] {
	//b.allocatedTo = m
	b->l in s.performsOperation
}

// Run predicate operate for one Buffer, five Locations and one Software
run operate for 1 Buffer, 5 Location, 1 Software

// Assertion: All software operations on a buffer
// are restricted within the bounds of the buffer 
assert noBufferOverflow{

		all s: Software, b:Buffer, l:Location| 
			//operate[s,b,l] implies l in b.start.*nextLocation
				operate[s,b,l] implies l in b.contains
}
check noBufferOverflow for 1 Buffer, 5 Location, 1 Software

// Fact: Software operations on a Buffer are 
// restricted to the bounds of that Buffer
fact limitBufferOverflow {

	all s: Software, b:Buffer| 
		s.performsOperation[b] in b.contains

}