import 'ARINC'.'metamodel';

@incremental
machine ModelsConstraints{ 
	
	 //allocate a job to a partition
	 @LabelingLiteral(executionmode='choose', priority='4')
	 gtrule allocateJobInstance(out JInstance) =
	 	{	  
	 		precondition pattern lhs(Job,P1,M1,M2,JInstance) =
	 		{  
			'Partition'(P1) below 'ARINC'.'model';   
			'JobInstance'(JInstance) below 'ARINC'.'model';
			'JobInstance'.'ins'(JI1,JInstance,Job);
	 		'Memory'(M1) below 'ARINC'.'model';
			'Memory'(M2) below 'ARINC'.'model';
	 		'Partition'.'freeMemory'(PM,P1,M1);
	 		'Job'(Job) below 'ARINC'.'model';
	 		'Application'.'memoryNeeded'(JM,Job,M2); 
		 	
		 	neg find PartitionJob(P2,JInstance);
            
           /*	neg pattern noJob(JInstance) = 
		 		{ 
		 			'Partition'(P11) below 'ARINC'.'model';   
					'JobInstance'(JInstance);
					'Partition'.'jobs'(PB3,P11,JInstance);     
		 		}*/
	        check( toInteger(value(M2)) <= toInteger(value(M1)) );
		 	}  
		 	action
		 	{ 
		 		let PJ = undef in seq
			 		{
			 		new('Partition'.'jobs'(PJ,P1,JInstance));	
			 		setValue(M1,toInteger(value(M1))-toInteger(value(M2)));  
			 		}   
		 	}
	    } 
	    
	 @LabelingLiteral(executionmode='choose', priority='4')
	 gtrule allocatePartition(out Partition) =
	 	{	  
	 		precondition pattern lhs(Partition,CPIOM) =
	 		{  
			'Partition'(Partition) below 'ARINC'.'model';
			'CPIOM'(CPIOM) below 'ARINC'.'model';
			
			neg find CPIOMPartition(OtherCPIOM,Partition); 
		 	/*neg pattern nopartition(Partition) = 
		 		{ 
		 			'Partition'(Partition) below 'ARINC'.'model';
					'CPIOM'(CPIOM1) below 'ARINC'.'model';
		 			'CPIOM'.'partitions'(CP1,CPIOM1,Partition);
		 		}*/
	 	 	}  
		 	action
		 	{ 
		 		let CJ = undef in seq
			 		{
			 		new('CPIOM'.'partitions'(CJ,CPIOM,Partition));	
			 		}   
		 	}
	    }
	    
	 @LabelingLiteral(executionmode='choose', priority='4')
	 gtrule allocateCPIOM(out CPIOM) =
	 	{	  
	 		precondition pattern lhs(CPIOM,Cabinet) =
	 		{  
			'Cabinet'(Cabinet) below 'ARINC'.'model';
			'CPIOM'(CPIOM) below 'ARINC'.'model';
			
		 	neg find CabinetCPIOM(OtherCabinet,CPIOM);
		 	/*neg pattern nopartition(CPIOM) = 
		 		{ 
		 			'Cabinet'(Cabinet) below 'ARINC'.'model';
					'CPIOM'(CPIOM) below 'ARINC'.'model';
		 			'Cabinet'.'cpioms'(CP1,Cabinet,CPIOM);
		 		}*/
	 	 	}  
		 	action
		 	{ 
		 		let CJ = undef in seq
			 		{
			 		new('Cabinet'.'cpioms'(CJ,Cabinet,CPIOM));	
			 		}   
		 	}
	    }
	 
	 /*@LabelingLiteral(executionmode='choose', priority='6')
	 gtrule createPartition(out ID) =
	 	{	  
	 		precondition pattern lhs(ID) =
	 		{  
				'IDPartition'(ID) below 'ARINC'.'model';
			}  
		 	action
		 	{ 
		 		let Memory = undef, PM = undef, Par = undef in seq
			 		{
			 		new('Partition'(Par) in 'ARINC'.'model');
			 		new('Memory'(Memory) in 'ARINC'.'model');
			 		setValue(Memory,100);
			 		rename(Par,"partition_"+value(ID));
			 		setValue(ID,toInteger(value(ID))+1);
			 		new('Partition'.'freeMemory'(PM,Par,Memory));	
			 		}   
		 	}
	    }   
	  */
	    
	 @LabelingLiteral(executionmode='choose', priority='exception')
	 gtrule createCPIOM(out ID) =
	 	{	  
	 		precondition pattern lhs(ID) =
	 		{  
				'IDCPIOM'(ID) below 'ARINC'.'model'; 
			}  
		 	action
		 	{ 	let CP = undef in seq{
		 			new('CPIOM'(CP)in 'ARINC'.'model');
			 		rename(CP,"CPIOM_"+value(ID));
			 		setValue(ID,toInteger(value(ID))+1);
		 	}  
		 	}
	    }      
	        
	
	 //all jobInstancess are scheduled to a partition 
	 @goal 
	 pattern JobInsatncewithoutPartition(Job) =    
	 {
	 		'JobInstance'(Job) below 'ARINC'.'model';
			neg find PartitionJob(Par,Job);
			/*neg pattern negpattern(Job) ={
	 			'JobInstance'(Job);
	 			'Partition'.'jobs'(PJ,P1,Job); 
	 			'Partition'(P1); 
	 		}*/ 
	 } 
 
	 //all CPIOMS are scheduled to a Cabinet
	 @goal 
	 pattern CPIOMwithoutCabinet(CPIOM) =    
	 {
	 		'CPIOM'(CPIOM) below 'ARINC'.'model';
			neg find CabinetCPIOM(Cabinet,CPIOM);
			/*neg pattern negpattern(CPIOM) ={
	 			'CPIOM'(CPIOM);
	 			'Cabinet'.'cpioms'(PJ,P1,CPIOM); 
	 			'Cabinet'(P1); 
	 		} */
	 } 
	 
	 //all Partitions are scheduled to a Cabinet
	 @goal 
	 pattern PartitionwithoutCPIOM(Par) =    
	 {
	 		'Partition'(Par) below 'ARINC'.'model';
			neg find CPIOMPartition(CPIOM,Par);
			/*neg pattern negpattern(Par) ={
	 			'Partition'(Par);
	 			'CPIOM'.'partitions'(PJ,P1,Par); 
	 			'CPIOM'(P1); 
	 		} */
	 } 
	 
	 //all partitions has more than 0 memory
	 //@globalconstraint
	 //pattern partitionsMemoryHigherThanZero(P1) =
	 //{
	 //	'Partition'(P1) below 'ARINC'.'model';    
	//	'Memory'(M1);
	//	'Partition'.'freeMemory'(PM,P1,M1);
	// 	check(toInteger(value(M1)) < 0);
	 //}
	 
	 @globalconstraint
	 pattern CriticalInstancesonSamePartition(Job) = 
	 {
	 	'JobInstance'(JobI1) below 'ARINC'.'model';
	 	'JobInstance'(JobI2) below 'ARINC'.'model';
		'CriticalJob'(Job) below 'ARINC'.'model';
		'JobInstance'.'ins'(JI1,JobI1,Job);
		'JobInstance'.'ins'(JI2,JobI2,Job);
		find PartitionJob(Par,JobI1);
        find PartitionJob(Par,JobI2);
        /*'Partition'(P1); 
		'Partition'.'jobs'(JS1,P1,JobI1);
		'Partition'.'jobs'(JS2,P1,JobI2);*/
	 }
	 
	 @globalconstraint 
	 pattern CriticalInstancesonSameCIOP(Job) = 
	 {
	 	'JobInstance'(JobI1) below 'ARINC'.'model';
	 	'JobInstance'(JobI2) below 'ARINC'.'model';
		'CriticalJob'(Job) below 'ARINC'.'model';
		'JobInstance'.'ins'(JI1,JobI1,Job);
		'JobInstance'.'ins'(JI2,JobI2,Job);
		find PartitionJob(Par1,JobI1);
        find PartitionJob(Par2,JobI2);
        /*'Partition'(P1); 
		'Partition'(P2);
		'Partition'.'jobs'(JS1,P1,JobI1);
		'Partition'.'jobs'(JS2,P2,JobI2);*/
		find CPIOMPartition(CPIOM,Par1);
        find CPIOMPartition(CPIOM,Par2);
        /*'CPIOM'(CPIOM) below 'ARINC'.'model';
		'CPIOM'.'partitions'(CPP1,CPIOM,P1);
		'CPIOM'.'partitions'(CPP2,CPIOM,P2);*/
	 }
	 
	 @globalconstraint
	 pattern PartitionCanHoldOnlyOneCriticalityLevel(P) = 
	 {
	 	'JobInstance'(JobI1) below 'ARINC'.'model';
	 	'JobInstance'(JobI2) below 'ARINC'.'model';
		'SimpleJob'(Job1) below 'ARINC'.'model';
		'CriticalJob'(Job2) below 'ARINC'.'model';
		'JobInstance'.'ins'(JI1,JobI1,Job1);
		'JobInstance'.'ins'(JI2,JobI2,Job2);
		find PartitionJob(P,JobI1);
        find PartitionJob(P,JobI2);
        /*'Partition'(P);
		'Partition'.'jobs'(JS1,P,JobI1);
		'Partition'.'jobs'(JS2,P,JobI2);*/
	 }
    @globalconstraint
     pattern TooManyUnusedCPIOM() = {
        'CPIOM'(C);
        'CPIOM'(C2);        
        neg find CPIOMPartition(C,Par);
        neg find CPIOMPartition(C2,Par);
     }
    //TODO: no constrain on the CIOPM arrangement
	/*@localsearch
	pattern lhs(ID) =
	 		{  
				'IDPartition'(ID) ;
			}
			
	pattern lhs2(ID) =
	 		{  
				'IDCPIOM'(ID) ;
			}
			
	pattern isEntity(E) = 
	{
		entity(E);
	}		  
	 
	 pattern isRelation(E) =
	 {
	 	entity(B);
	 	entity(A);
	 	relation(E,A,B);
	 }
	 
	 asmfunction model/1;
	 rule main() = seq{
	      println("DIANA constraint set");
	    update model("Relation") = 0;
	    update model("Entity") = 0;  
	   /* forall E below'ARINC'.'solution' with find isEntity(E) do
	    	  update model("Entity") = toInteger(model("Entity")) + 1; 
	    	  
	     forall E below'ARINC'.'solution' with find isRelation(E) do
	    	  update model("Relation") = toInteger(model("Relation")) + 1; 	  
	      
	      println("E: "+model("Entity") + " R:"+ model("Relation"));
	   */   
	   //   forall Id with find lhs(Id) do println(fqn(Id));
	      
	   //   forall Id with find lhs2(Id) do println(fqn(Id));
	      
		/*forall Job with apply allocateJobInstance(Job) do println(fqn(Job));
		
		//forall Job with find JobInsatncewithoutPartition(Job) do println("hej "+fqn(Job));
		
		//choose Par with apply createPartition(Par) do println(fqn(Par));
		
		//choose Par with apply allocateJobInstance(Par) do println(fqn(Par));
		
		
	}*/
    pattern CabinetCPIOM(Cabinet,CPIOM) = { 
        'Cabinet'(Cabinet);
        'CPIOM'(CPIOM);
        'Cabinet'.'cpioms'(CP1,Cabinet,CPIOM);
    }  

    pattern CPIOMPartition(P1,Par) ={
        'Partition'(Par);
        'CPIOM'.'partitions'(PJ,P1,Par); 
        'CPIOM'(P1); 
    } 
    
    pattern PartitionJob(P1,Job) ={
        'JobInstance'(Job);
        'Partition'.'jobs'(PJ,P1,Job); 
        'Partition'(P1); 
    } 
    
    pattern Cabinet(C) = {
        'Cabinet'(C);
    } 
    pattern CPIOM(C) = {
        'CPIOM'(C);
    }
    pattern Partition(P) = {
        'Partition'(P);
    }
}