specification PetStoreAPI

/**
 * Resource definition
 */
resource Pet {
	pred hasid(integer)
}

resource Store

resource User {
	pred hasNameAndPassword(string, string)
}


/**
 * Types definition
 */
type PetRep = {
	?id: integer,
	?category: Category,
	name: string,
	photoUrls: URI[],
	tags: Tag[],
    ?status: (x: string where x == "available" || x == "pending" || x == "sold")    
}

type Category = {
	?id: integer,
	?name: string
}

type Tag = {
	id: integer,
	name: string
} 

type ModelApiResponse = {
    code: integer,
    type: string,
    message: string
}

type InlineModel = {
    model: InlineModelAux[]
}

// aparentemente uma repeticao do PetRep
type InlineModelAux = {
    ?id: integer,
    ?category: Category,
    name: string,
    photoUrls: URI[],
    ?tags: Tag[],
    ?status: ["available"] | ["pending"] | ["sold"]
}

type UserRep = {
    ?id: integer, //long ???
    ?username: string,
    ?firstName: string,
    ?lastName: string,
    ?email: string,
    ?password: string,
    ?phone: string,
    ?userStatus: integer
}

type StatusType = (x:string where x == "available" || x == "pending" || x == "sold")[]

/**
 * Represents definition
 */
 
petRep:PetRep represents Pet {
	hasid(id) => isdefined(petRep.id) && petRep.id == id
}

userRep:UserRep represents User {
	hasNameAndPassword(username, password) => userRep.username == username && userRep.password == password
}

/**
 * CODES
 */
def SUCCESS = 200
def CREATED = 201
def BAD_REQUEST = 400
def NOT_FOUND = 404
def INVALID_INPUT = 405
def DUPLICATE = 409

// addPet 200, If pet doesn't exist
{	
	request in {body: PetRep} &&
	(isdefined(request.body.id) ==>
		(forall pet:Pet .
			!pet.hasid(request.body.id)
		)
	)	
}
	POST /pet
{
	response.code == SUCCESS &&
	response in {body: PetRep} &&
	(isdefined(request.body.id) => response.body == request.body) &&
	(exists pet:Pet .
		response.body representationof pet && expand(/pet/{petid} , {petid: response.body.id}) uriof pet
	)
}

// addPet 200, If pet exists
var pet: Pet  
{
	request in {body: PetRep} &&
	(isdefined(request.body.id) ?
		(exists pet: Pet .
			expand(/pet/{id} , {id: request.body.id}) uriof pet && pet.hasid(request.body.id)
		)
		: false
	)
}
	POST /pet
{
	
	response.code == SUCCESS &&
	response in {body: PetRep} &&
	response.body == request.body &&
	response.body representationof pet
}

// addPet 405, Invalid input
{
	!(request in {body: PetRep})
}
	POST /pet
{
	response.code == INVALID_INPUT &&
	response in {body: ModelApiResponse} &&
	response.body.type == "unknown" &&
    response.body.message == "bad input"
}

// updatePet 200
// hardcopies request.body on a pet representation
{
	request in {body: PetRep} &&
	(exists pet: Pet .
		expand(/pet/{id} , {id: request.body.id}) uriof pet &&
		pet.hasid(request.body.id)
	)
}
	PUT /pet
{
	response.code == SUCCESS &&
	response in {body: PetRep} &&
	response.body == request.body &&
	response.body representationof pet
}

// updatePet 400
{
	!(request in {body: PetRep})
}
	PUT /pet
{
	response.code == BAD_REQUEST &&
	response in {body: ModelApiResponse} &&
	response.body.type == "unknown" &&
	response.body.message == "bad input"
}

// updatePet 404, 405
// 404 impossivel pois o PUT deles cria se nao existe ...
// tentativas de 405 acabaram em erro 500 (meter string em vez de int, int overflow, etc)

// uploadFile 200
// fileuploading is still complex for RSpec language

// findPetsByStatus 200
{
	request in {template: {status: StatusType}}
}
	GET /pet/findByStatus{?status}
{
	response.code == SUCCESS &&
	response in {body: InlineModel} &&
	(forall i: (x: integer where 0 <= x && x < length(response.body.model)) . //here
		(exists j: (y: integer where 0 <= y && y < length(response.body.model)) .
			response.body.model[i].status == request.template.status[j]
		)
	)
}

// findPetsByStatus 400
{
	!(request in {template: {status: StatusType}})
}
    GET /pet/findByStatus{?status}
{
    response.code == BAD_REQUEST
}

// createUser 200
{
    request in {body: UserRep}
}
    POST /user
{
	response.code == SUCCESS 
}

// loginUser 200 & 400, if invalid it creates as new account
{
	request in {template: {username: string, password: string}} &&
	(exists user:User .
		user.hasNameAndPassword(request.template.username, request.template.password)
	)
}
	GET /user/login{?username,password}
{
	response.code == SUCCESS 
}