import 'http://mast.unican.es/ecoremast/Mast2'

package mast2


context Mast_Model 

-- No_Hard_Local_Deadlines
inv noHardLocalDeadlines:
	Hard_Local_Deadline.allInstances() -> isEmpty()
	
-- Monoprocessor_Only
inv isMonoprocessor:
	self.Element_List -> one(elem | elem.oclIsKindOf(Computing_Resource)) and 
	self.Element_List -> select(elem | elem.oclIsKindOf(Processing_Resource)) -> size() = 1

-- Fixed_Priorities_Only
inv isOnlyFP: 
	Schedulable_Resource.allInstances() -> forAll(sr | sr.Scheduling_Parameters.oclIsKindOf(Priority_Based_Params)) and
	Code_Operation.allInstances() -> forAll(co | not co.Overridden_Sched_Parameters.oclIsUndefined() implies 
		                                             co.Overridden_Sched_Parameters.oclIsTypeOf(Overridden_Fixed_Priority)) and
	Secondary_Scheduler.allInstances() -> isEmpty()


-- Simple_Transations_Only
context End_To_End_Flow inv isSimple:
	self.Flow_Element_List -> select(fe | fe.oclIsTypeOf(Step)) -> forAll(s1, s2 | s1.oclAsType(Step).Step_Schedulable_Resource = s2.oclAsType(Step).Step_Schedulable_Resource)

	                     
-- No_Permanent_OVerridden_Priorities	                     
context Code_Operation inv hasNoPermanentOverridenPriorities: 
	not self.Overridden_Sched_Parameters.oclIsUndefined() implies 
	not self.Overridden_Sched_Parameters.oclIsTypeOf(Overridden_Permanent_FP)

endpackage