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
	                     
-- EDF_Only
inv isOnlyEDF: 
	Schedulable_Resource.allInstances() -> forAll(sr | sr.Scheduling_Parameters.oclIsKindOf(EDF_Based_Params) or
		                                               sr.Scheduling_Parameters.oclIsKindOf(Interrupt_Based_Params)) and
	Code_Operation.allInstances() -> forAll(co | co.Overridden_Sched_Parameters.oclIsUndefined()) and
	Secondary_Scheduler.allInstances() -> isEmpty()
	
-- SRP_Only	         
inv isOnlySRP: 
	Mutual_Exclusion_Resource.allInstances()-> forAll(m | m.oclIsTypeOf(SRP_Mutex))


-- 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)
	
    
endpackage