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_Within_Priorities_Only
inv isOnlyEDFwithinPriorities: 
	Primary_Scheduler.allInstances() -> forAll(ps | ps.Policy.oclIsTypeOf(Fixed_Priority_Policy)) and
	Secondary_Scheduler.allInstances() -> forAll(ss | ss.Policy.oclIsTypeOf(EDF_Policy)) and
	Secondary_Scheduler.allInstances() -> forAll(ss | ss.Host.Scheduler.oclIsTypeOf(Primary_Scheduler)) and
	Step.allInstances() -> select(s | s.Step_Operation.oclIsKindOf(Code_Operation)) ->
	                       forAll(s | s.Step_Operation.oclAsType(Code_Operation).Overridden_Sched_Parameters.oclIsTypeOf(Overridden_Fixed_Priority) implies 
	                           	      s.Step_Schedulable_Resource.Scheduling_Parameters.oclIsKindOf(Priority_Based_Params))


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