specification Features-service

// Some constants to avoid magical numbers and ease maintenance
def SUCCESS = 200
def CREATED = 201
def NO_CONTENT = 204
def BAD_REQUEST = 400
def NOT_FOUND = 404
def CONFLICT = 409


// Resources
resource ProductR
resource ProductConfigurationR
resource FeatureR
resource FeatureConfigurationR
resource ConstraintR

// Types
type Feature = {
   id: integer,
   name: string,
   description: string
}

type Constraint = (x: { //ADDED commented out stuff that was generating an Any type
   id: integer,
   type: string,
   sourceFeatureName: string,			//estes 3 nao constam do swagger
   ?requiredFeatureName: string,			
   ?excludedFeatureName: string
} where isdefined(x.excludedFeatureName) || isdefined(x.requiredFeatureName)) //supondo q o isdefined nao impede q seja null

type ProductConfiguration = {
   name: string,
   valid: boolean,
   activatedFeatures: Feature[]
}

type Product = {
   id: integer,
   name: string,
   features: Feature[],
   constraints: Constraint[]
}

type URIString = (x: string where length(x) > 0 && matches(/^[a-zA-Z_-]{1,15}$/, x))

// Variables

var productR: ProductR
var featureR: FeatureR
var configurationR: ProductConfigurationR
var featureconfigurationR: FeatureConfigurationR

// Assertions

//***********************  PRODUCTS  ***************************

// get products
// > to request a list with the names of all available products
{
	true
}
    GET /products [alias GetAllProducts]
{
    response.code == SUCCESS &&
    response in {body: string[]} &&& (
    (forall i: (x: integer where x >= 0 && x < length(response.body)).
    		(exists productR: ProductR.  
    			(exists product: Product. product representationof productR &&
    				product.name == response.body[i]) 	
    		)
    ) &&
    (forall productR: ProductR. 
   	 	(exists product: Product. product representationof productR &&
    			(exists i: (x: integer where x >= 0 && x < length(response.body)). 
    				product.name == response.body[i])     			
    		)
    )
    ) 
}

// get product
// > to request the features and constraints of a product
{
   request in {template: {productName: URIString}} &&
   (exists productR:ProductR .
   	request.location uriof productR		
   )   
}
	GET /products/{productName} [alias getProductByName]
{
  response.code == SUCCESS &&
  response in {body: Product} &&& (
  response.body representationof productR &&
  response.body.name == request.template.productName &&
  request.location uriof productR //to simulate the lock from the var
  )
}


// >add a new product  
{
   request in {template: {productName: URIString}}
}
	POST /products/{productName} [alias addProduct, creates ProductR]
{
  response.code == CREATED &&
  response in {header: {Location: URI}} &&& 
  (exists productR: ProductR . 
     response.header.Location uriof productR &&						
     (exists product: Product . product representationof productR &&
     	product.name == request.template.productName && product.features == [] && product.constraints == [])
  ) 
}

// delete product
// > to remove an existing product and all its configurations
{
   request in {template: {productName: URIString}} &&
   (exists productR: ProductR . request.location uriof productR)		   
}
	DELETE /products/{productName} [alias deleteProductByName]
{
  response.code == NO_CONTENT &&       
  (forall productR: ProductR . !(request.location uriof productR) &&
  (forall product : Product . product representationof productR => product.name != request.template.productName)) &&
  (forall configuration: ProductConfigurationR . 
  		(forall configurationName: URIString .  
    			!(/*root ++*/ expand(/products/{productName}/configurations/{configurationName} , {
    						productName: request.template.productName,
    						configurationName: configurationName })
    			uriof configurationR) 
    		)  
  )
}


//***********************  FEATURES  ***************************

// get a list with the features of a product 
{
	request in {template: {productName: URIString}} &&
	request.location uriof productR 
}
    GET /products/{productName}/features [alias getFeaturesForProduct]
{
    response.code == SUCCESS &&
    response in {body: Feature[]} &&& (
    //no swagger tem que o array nao tem elementos repetidos mas no headrest isto eh chato de escrever...
    (forall i: (x: integer where x >= 0 && x < length(response.body)). 
    		(exists featureR: FeatureR .  
    			(exists feature: Feature . 
    					feature representationof featureR &&
    					feature.name == response.body[i].name &&
    					(/*root ++*/ expand(/products/{productName}/features/{featureName} , {
    							productName: request.template.productName,
    							featureName: feature.name })
    					) uriof featureR
    			)
    		)
    ) &&
    (forall featureR: FeatureR .  
    	(exists featureName: URIString .  
    		(/*root ++*/ expand(/products/{productName}/features/{featureName} , {
    					productName: request.template.productName,
    					featureName: featureName })
    		) uriof featureR
    	)  
    	=>
   	 	(exists feature: Feature . 
   	 		feature representationof featureR &&
    			(exists i: (x: integer where x >= 0 && x < length(response.body)). 
    				feature.name == response.body[i])     			
    		)
    ) 
    )
    //para  dizer que todas as features que ele mostra sao do produto dado so indo atraves do resourceid
}

// add a feature to a product 
{
   request in {template: {productName: URIString, featureName: URIString, ?description: string}} &&
   (/*root ++*/ expand(/products/{productName} , {productName: request.template.productName})) uriof productR
}
	POST /products/{productName}/features/{featureName}{?description} [alias addFeatureToProduct, creates FeatureR]
{
  response.code == CREATED &&
  response in {header: {Location: URI}} &&& (
  (exists featureR: FeatureR . 
     response.header.Location uriof featureR &&						
     (exists feature: Feature . 
     	feature representationof featureR &&
     	feature.name == request.template.featureName &&
     	((isdefined(request.template.description) ==> feature.description == request.template.description)) &&
     	((!isdefined(request.template.description) ==> feature.description == null))	
     )
  ) &&
  //ver se queremos eliminar a anterior...
  (forall product: Product. product representationof productR =>
  	(exists i: (x: integer where x >= 0 && x < length(product.features)). 
  		product.features[i].name  == request.template.featureName &&
 		((isdefined(request.template.description) ==> product.features[i].description  == request.template.description)) &&
		((!isdefined(request.template.description) ==> product.features[i].description  == null))
  	) 
  )
  )
}

// delete a product feature 
{
   request in {template: {productName: URIString, featureName: URIString}} &&
   request.location uriof featureR &&		//isto vai possivelmente causar problemas...   
   (/*root ++*/ expand(/products/{productName} , {productName: request.template.productName})) uriof productR  
}
	DELETE /products/{productName}/features/{featureName} [alias deleteFeatureOfProduct]
{
  response.code ==  NO_CONTENT &&
  (forall featureR: FeatureR . !(request.location uriof featureR)) &&
  (forall product: Product. product representationof productR &&
  	(forall i: (x: integer where x >= 0 && x < length(product.features)). 
  		product.features[i].name  != request.template.featureName 
   	) 
  )
 }


// update a feature of a product 
{
   request in {template: {productName: URIString, featureName: URIString, ?description: string}} &&
   (/*root ++*/ expand(/products/{productName} , {productName: request.template.productName})) uriof productR
}
	PUT /products/{productName}/features/{featureName}{?description} [alias updateFeatureOfProduct]
{
  response.code == SUCCESS &&
  response in {body: Feature} &&& (
  response.body.name  == request.template.featureName &&
  ((isdefined(request.template.description) ==> response.body.description  == request.template.description)) &&
  (exists product: Product . product representationof productR &&
  	(exists i: (x: integer where x >= 0 && x < length(product.features)). product.features[i] == response.body) 
  )
  )
}


//***********************  CONSTRAINTS  ***************************


// add a excluded constraint to a product 
{
   request in {template: {productName: URIString, ?sourceFeature: string, ?excludedFeature: string}} &&
   (/*root ++*/ expand(/products/{productName} , {productName: request.template.productName})) uriof productR
   //nao exige que os nomes sejam de features que existem e vai juntando sempre
}
	POST /products/{productName}/constraints/excludes{?sourceFeature,excludedFeature} [alias addExcludesConstrainToProduct, creates ConstraintR]
{
  response.code == CREATED &&
  response in {header: {Location: URI}} &&& (  //usa o id do contraint para criar o uri
  (exists constraintR: ConstraintR. 
     response.header.Location uriof constraintR &&						
     (exists constraint: Constraint . 
     	constraint representationof constraintR &&
  		constraint.type  == "excludes" &&
  		isdefined(constraint.excludedFeatureName) &&& (		
 		((isdefined(request.template.sourceFeature) ==> constraint.sourceFeatureName  == request.template.sourceFeature)) &&
		((!isdefined(request.template.sourceFeature) ==> constraint.sourceFeatureName  == null)) &&
		((isdefined(request.template.excludedFeature) ==> constraint.excludedFeatureName  == request.template.excludedFeature)) &&
		((!isdefined(request.template.excludedFeature) ==> constraint.excludedFeatureName  == null)) 
		)
     )
  ) &&
  (exists product: Product. product representationof productR &&
  	(exists i: (x: integer where x >= 0 && x < length(product.constraints)). 
  			product.constraints[i].type  == "excludes" &&
 			((isdefined(request.template.sourceFeature) ==> product.constraints[i].sourceFeatureName  == request.template.sourceFeature)) &&
			((!isdefined(request.template.sourceFeature) ==> product.constraints[i].sourceFeatureName  == null)) &&
			((isdefined(request.template.excludedFeature) ==> product.constraints[i].excludedFeatureName  == request.template.excludedFeature)) &&
			((!isdefined(request.template.excludedFeature) ==> product.constraints[i].excludedFeatureName  == null)) 
	)
  ) 
  )
}

// add a required constraint to a product 
{
   request in {template: {productName: URIString, ?sourceFeature: string, ?requiredFeature: string}} &&
   (/*root ++*/ expand(/products/{productName} , {productName: request.template.productName})) uriof productR
   //nao exige que os nomes sejam de features que existem e vai juntando sempre
}
	POST /products/{productName}/constraints/requires{?sourceFeature,requiredFeature} [alias addRequiresConstrainToProduct, creates ConstraintR]
{
  response.code == CREATED &&
  response in {header: {Location: URI}} &&& ( //o uri eh /products/{productName}/constraints/{id}
   (exists constraintR: ConstraintR. 
     response.header.Location uriof constraintR &&						
     (exists constraint: Constraint . 
     	constraint representationof constraintR &&
   		constraint.type  == "requires" && 
   		isdefined(constraint.requiredFeatureName) &&& (
 		((isdefined(request.template.sourceFeature) ==> constraint.sourceFeatureName  == request.template.sourceFeature)) &&
		((!isdefined(request.template.sourceFeature) ==> constraint.sourceFeatureName  == null)) &&
		((isdefined(request.template.requiredFeature) ==> constraint.requiredFeatureName  == request.template.requiredFeature)) &&
		((!isdefined(request.template.requiredFeature) ==> constraint.requiredFeatureName  == null)) 
		)
     )
  ) &&
  (exists product: Product. product representationof productR &&
  	(exists i: (x: integer where x >= 0 && x < length(product.features)).  
   			product.constraints[i].type  == "requires" &&
 			((isdefined(request.template.sourceFeature) ==> product.constraints[i].sourceFeatureName  == request.template.sourceFeature)) &&
			((!isdefined(request.template.sourceFeature) ==> product.constraints[i].sourceFeatureName  == null)) &&
			((isdefined(request.template.requiredFeature) ==> product.constraints[i].requiredFeatureName  == request.template.requiredFeature)) &&
			((!isdefined(request.template.requiredFeature) ==> product.constraints[i].requiredFeatureName  == null)) 
			// nao sei como dizer que ultimo pedaco de response.header.Location eh igual a product.features[i].id
		)
  )
  )
}

// delete a constraint to a product 
{
   request in {template: {productName: URIString, constraintId: integer}} &&
   request.location uriof featureR &&		//isto vai possivelmente causar problemas...   
   (/*root ++*/ expand(/products/{productName} , {productName: request.template.productName})) uriof productR  
}
	DELETE /products/{productName}/constraints/{constraintId} [alias deleteConstraint]
{
  response.code ==  NO_CONTENT &&
  (forall constraintR: ConstraintR. !(request.location uriof featureR)) &&
  (forall product: Product. product representationof productR &&
  	(forall i: (x: integer where x >= 0 && x < length(product.constraints)). 
  		product.constraints[i].id  != request.template.constraintId 
   	) 
  )
 }


// update a feature of a product 
{
   request in {template: {productName: URIString, featureName: URIString, ?description: string}} &&&
   (/*root ++*/ expand(/products/{productName} , {productName: request.template.productName})) uriof productR
}
	PUT /products/{productName}/features/{featureName}{?description} [alias updateFeatureOfProduct]
{
  response.code == SUCCESS &&
  response in {body: Feature} &&& (
  response.body.name  == request.template.featureName &&
  ((isdefined(request.template.description) ==> response.body.description  == request.template.description)) &&
  ((!isdefined(request.template.description) ==> response.body.description  == null)) &&
  (exists product: Product. product representationof productR &&
  	(exists i: (x: integer where x >= 0 && x < length(product.features)). 
  		product.features[i] == response.body) 
  )
  )
}

//***********************  PRODUCT CONFIGURATIONS  ***************************

// get a list with the names of the configurations of a product 
{
	request in {template: {productName: URIString}} &&
    (/*root ++*/ expand(/products/{productName} , {productName: request.template.productName})) uriof productR
 }
    GET /products/{productName}/configurations [alias getConfigurationsForProduct]
{
    response.code == SUCCESS &&
    response in {body: string[]} &&& (
    (forall i: (x: integer where x >= 0 && x < length(response.body)). 
    		(exists configurationR: ProductConfigurationR .  
    			(exists configuration: ProductConfiguration . 
    					configuration representationof configurationR &&
    					configuration.name == response.body[i] &&
    					(/*root ++*/ expand(/products/{productName}/configurations/{configurationName} , {
    							productName: request.template.productName,
    							configurationName: configuration.name })
    					) uriof configurationR
    			)
    		)
    ) &&
    (forall configurationR: ProductConfigurationR .  
    		(exists configurationName: URIString .  
    			(/*root ++*/ expand(/products/{productName}/configurations/{configurationName} , {
    						productName: request.template.productName,
    						configurationName: configurationName })
    			) uriof configurationR
    		)  
    		=>
   	 	(exists configuration: ProductConfiguration . 
   	 		configuration representationof configurationR &&
    			(exists i: (x: integer where x >= 0 && x < length(response.body)).
    			 configuration.name == response.body[i])     			
    		)
    ) 
    )
    //para  dizer que todas as configurations cujo nome ele mostra sao do produto dado so indo atraves do resourceid
}

// get a product configuration 
{
   request in {template: {productName: URIString, configurationName: URIString}} &&
   request.location uriof configurationR 		   
}
	GET /products/{productName}/configurations/{configurationName} [alias getConfigurationWithNameForProduct]
{
  response.code == SUCCESS /*&& //ADDED Commented out incompatible response types
  response in {body: ProductConfiguration} &&& (
  response.body representationof configurationR &&
  response.body.name == request.template.configurationName
  )*/
}

// add a product configuration 
{
   request in {template: {productName: URIString, configurationName: URIString}} &&
   request.location uriof configurationR 		   
}
	POST /products/{productName}/configurations/{configurationName} [alias addConfiguration, creates ProductConfigurationR]
{
  response.code == CREATED &&
  response in {header: {Location: URI}} &&&
  (exists configurationR: ProductConfigurationR . 
     response.header.Location uriof configurationR &&						
     (exists configuration: ProductConfiguration . 
     	configuration representationof configurationR &&
     	configuration.name == request.template.configurationName &&
     	configuration.valid == true &&										//nao diz na spec mas na wiki
     	configuration.activatedFeatures == []
     )
  ) 
}

// delete a product configuration 
{
   request in {template: {productName: URIString, configurationName: URIString}} &&
   request.location uriof configurationR 		   
}
	DELETE /products/{productName}/configurations/{configurationName} [alias deleteConfiguration]
{
  response.code ==  NO_CONTENT &&
  (forall configurationR: ProductConfigurationR . !(request.location uriof configurationR))
  //fica por dizer que nao ha nenhuma config daquele produto com aquele nome...
 }
 
 
 
//***********************  FEATURES OF PRODUCCONFIGURATIONS  ***************************

// get a list with the names of the features that are active in a configurations of a product 
{
	request in {template: {productName: URIString, configurationName: URIString}} &&&
    (/*root ++*/ expand(/products/{productName}/configurations/{configurationName} , 
    				{productName: request.template.productName,
    				 configurationName: request.template.configurationName
    				}
    )) uriof configurationR
}
    GET /products/{productName}/configurations/{configurationName} [alias getConfigurationActiveFeatures]
{
    response.code == SUCCESS /*&& //ADDED Commented out incompatible response types
    response in {body: string[]} &&& (
    (forall i: (x: integer where x >= 0 && x < length(response.body)).
       	(forall configuration: ProductConfiguration. configuration representationof configurationR =>
  			(exists j: (x: integer where x >= 0 && x < length(configuration.activatedFeatures)).
    					configuration.activatedFeatures[j] == response.body[i] 
  			)
    	)
    ) &&
   	(exists configuration: ProductConfiguration.  configuration representationof configurationR &&
   		(forall j: (x: integer where x >= 0 && x < length(configuration.activatedFeatures)).
    			(exists i: (x: integer where x >= 0 && x < length(response.body)). 
    				configuration.activatedFeatures[j] == response.body[i]
    			)     			
    		)
    ) 
    )*/
}
 
 // add an active feature to a configuration 
{
	request in {template: {productName: URIString, configurationName: URIString, featureName: URIString}} &&& (
	//interagindo com o sistema aprende-se que 
	//1) da 500 e Object with id XXX has not been found se feature com nome dado nao existe no produto
    (/*root ++*/ expand(/products/{productName} , {productName: request.template.productName})) uriof productR &&
    (forall product: Product. product representationof productR =>
  		(exists i: (x: integer where x >= 0 && x < length(product.features)). 
  			product.features[i].name  == request.template.featureName  	
  		)
  	) &&
  	//substitui eventualmente a anterior
  	(/*root ++*/ expand(/products/{productName}/features/{featureName} , 
    				{productName: request.template.productName,
    				 configurationName: request.template.featureName
    				}
    )) uriof featureR  &&
    (/*root ++*/ expand(/products/{productName}/configurations/{configurationName} , 
    				{productName: request.template.productName,
    				 configurationName: request.template.configurationName
    				}
    )) uriof configurationR 
    )
    	//2)da 500 e excepção com duplicado se ja existe
	//incluir???	
	//3) da 500 se os contraints sao violados 
	//Wrong product configuration: Feauture COURSE_SELLING can not be active when feature IN_TRIAL_PERIOD is active
	//mas mesmo assim coloca no produto
}
    POST /products/{productName}/configurations/{configurationName}/features/{featureName} [alias addActiveFeature, creates FeatureConfigurationR]
{
  response.code == CREATED &&
  response in {header: {Location: URI}} &&& (
  (exists featureconfigurationR: FeatureConfigurationR. 
     response.header.Location uriof featureconfigurationR) &&						
  (forall configuration: ProductConfiguration. configuration representationof configurationR =>
	     (exists feature: Feature. feature representationof featureR &&
     		feature.name == request.template.featureName &&
 			(exists j: (x: integer where x >= 0 && x < length(configuration.activatedFeatures)).
 				configuration.activatedFeatures[j] == feature
 			)
     	)
  )
  )
  //falta dizer que fica invalida se for invalidado com a adicao algum constraint to produto 
}
 
  // delete an active feature to a configuration 
{
	request in {template: {productName: URIString, configurationName: URIString, featureName: URIString}} &&& (
    (/*root ++*/ expand(/products/{productName} , {productName: request.template.productName})) uriof productR &&
  	(/*root ++*/ expand(/products/{productName}/features/{featureName} , 
    				{productName: request.template.productName,
    				 configurationName: request.template.featureName
    				}
    )) uriof featureR  &&
    (/*root ++*/ expand(/products/{productName}/configurations/{configurationName} , 
    				{productName: request.template.productName,
    				 configurationName: request.template.configurationName
    				}
    )) uriof configurationR
    )
}
    DELETE /products/{productName}/configurations/{configurationName}/features/{featureName} [alias deleteFeature]
{
 	response.code ==  NO_CONTENT &&
	(forall featureconfigurationR: FeatureConfigurationR. !(request.location uriof featureconfigurationR)) &&
	(forall configuration: ProductConfiguration. configuration representationof configurationR =>
  		(forall j: (x: integer where x >= 0 && x < length(configuration.activatedFeatures)).
 			configuration.activatedFeatures[j].name != request.template.featureName
     	)
  	)
  	 //falta dizer que fica invalida se for invalidado com o delete algum constraint to produto 
}