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

package mast2

-- ------------------------------------------
-- Regarding the attributes of a single class
-- ------------------------------------------

context Timer
	inv i_1_1_a:
		Max_Overhead >= Avg_Overhead and Max_Overhead >= Min_Overhead 
		                             and Avg_Overhead >= Min_Overhead

context Processing_Resource
	inv i_1_2_a: 
		Speed_Factor > 0.0

context Regular_Processor
	inv i_1_3_a: 
		Max_Interrupt_Priority >= Min_Interrupt_Priority
		
context Regular_Processor
	inv i_1_3_b:
		Worst_ISR_Switch >= Avg_ISR_Switch and 
		Worst_ISR_Switch >= Best_ISR_Switch and 
		Avg_ISR_Switch >= Best_ISR_Switch
		
context Network
	inv i_1_4_a: 
		self.Throughput > 0.0
		
context Packet_Based_Network
	inv i_1_5_a:
		Max_Packet_Size >= Min_Packet_Size
		
context AFDX_Link
	inv i_1_6_a:
		Max_Packet_Size >= Min_Packet_Size
		
context AFDX_Link
	inv i_1_6_b:
		Max_HW_Tx_Latency >= Avg_HW_Tx_Latency and 
		Max_HW_Tx_Latency >= Min_HW_Tx_Latency and 
		Avg_HW_Tx_Latency >= Min_HW_Tx_Latency

context AFDX_Link
	inv i_1_6_c:
		Max_HW_Rx_Latency >= Avg_HW_Rx_Latency and 
		Max_HW_Rx_Latency >= Min_HW_Rx_Latency and 
		Avg_HW_Rx_Latency >= Min_HW_Rx_Latency
		
context Network_Switch
	inv i_1_7_a:
		Max_Fixed_Fork_Latency >= Avg_Fixed_Fork_Latency and 
		Max_Fixed_Fork_Latency >= Min_Fixed_Fork_Latency and 
		Avg_Fixed_Fork_Latency >= Min_Fixed_Fork_Latency

context Network_Switch
	inv i_1_7_b:
		Max_Variable_Fork_Latency >= Avg_Variable_Fork_Latency and 
		Max_Variable_Fork_Latency >= Min_Variable_Fork_Latency and 
		Avg_Variable_Fork_Latency >= Min_Variable_Fork_Latency

context Network_Switch
	inv i_1_7_c:
		Max_Delivery_Latency >= Avg_Delivery_Latency and 
		Max_Delivery_Latency >= Min_Delivery_Latency and 
		Avg_Delivery_Latency >= Min_Delivery_Latency

context Network_Router
	inv i_1_8_a:
		Max_Fixed_Branch_Latency >= Avg_Fixed_Branch_Latency and 
		Max_Fixed_Branch_Latency >= Min_Fixed_Branch_Latency and 
		Avg_Fixed_Branch_Latency >= Min_Fixed_Branch_Latency

context Network_Router
	inv i_1_8_b:
		Max_Variable_Branch_Latency >= Avg_Variable_Branch_Latency and 
		Max_Variable_Branch_Latency >= Min_Variable_Branch_Latency and 
		Avg_Variable_Branch_Latency >= Min_Variable_Branch_Latency

context Fixed_Priority_Policy
	inv i_1_9_a:
		Max_Priority >= Min_Priority
		
context Fixed_Priority_Policy
	inv i_1_9_b:		
		Worst_Context_Switch >= Avg_Context_Switch and 
		Worst_Context_Switch >= Best_Context_Switch and 
		Avg_Context_Switch >= Best_Context_Switch

context EDF_Policy
	inv i_1_10_a:		
		Worst_Context_Switch >= Avg_Context_Switch and 
		Worst_Context_Switch >= Best_Context_Switch and 
		Avg_Context_Switch >= Best_Context_Switch

context FP_Packet_Based_Policy
	inv i_1_11_a:
		Max_Priority >= Min_Priority

context FP_Packet_Based_Policy
	inv i_1_11_b:
		Packet_Overhead_Max_Size >= Packet_Overhead_Avg_Size and 
		Packet_Overhead_Max_Size >= Packet_Overhead_Min_Size and 
		Packet_Overhead_Avg_Size >= Packet_Overhead_Min_Size

context Polling_Params
	inv i_1_12_a:
		Polling_Worst_Overhead >= Polling_Avg_Overhead and 
		Polling_Worst_Overhead >= Polling_Best_Overhead and 
		Polling_Avg_Overhead >= Polling_Best_Overhead

context Simple_Operation
	inv i_1_13_a:
		Worst_Case_Execution_Time >= Avg_Case_Execution_Time and 
		Worst_Case_Execution_Time >= Best_Case_Execution_Time and
		Avg_Case_Execution_Time >= Best_Case_Execution_Time

context Enclosing_Operation
	inv i_1_14_a:
		Worst_Case_Execution_Time >= Avg_Case_Execution_Time and 
		Worst_Case_Execution_Time >= Best_Case_Execution_Time and 
		Avg_Case_Execution_Time >= Best_Case_Execution_Time

context Message
	inv i_1_15_a:
		Max_Message_Size >= Avg_Message_Size and 
		Max_Message_Size >= Min_Message_Size and 
		Avg_Message_Size >= Min_Message_Size

context Sporadic_Event
	inv i_1_16_a:
		Avg_Interarrival >= Min_Interarrival
		
context Delay
	inv i_1_17_a:
		Delay_Max_Interval >= Delay_Avg_Interval and 
		Delay_Max_Interval >= Delay_Best_Interval and 
		Delay_Avg_Interval >= Delay_Best_Interval


-- -----------------------------
-- Regarding single associations
-- -----------------------------

context Clock_Synchronization_Object
	inv i_2_1_a: 
		Model.Element_List -> select(e | e.oclIsTypeOf(Clock_Synchronization_Object))
		                   -> forAll(c | c <> self implies c.name <> self.name)

context Timer
	inv i_2_1_b: 
		Model.Element_List -> select(e | e.oclIsKindOf(Timer))
		                   -> forAll(t | t <> self implies t.name <> self.name)

context Processing_Resource
	inv i_2_1_c: 
		Model.Element_List -> select(e | e.oclIsKindOf(Processing_Resource)) 
	                       -> forAll(pr | pr <> self implies pr.name <> self.name)

context Scheduler
	inv i_2_1_d: 
		Model.Element_List -> select(e | e.oclIsKindOf(Scheduler))
	                       -> forAll(s | s <> self implies s.name <> self.name)

context Schedulable_Resource
	inv i_2_1_e: 
		Model.Element_List -> select(e | e.oclIsKindOf(Schedulable_Resource))
	                       -> forAll(sr | sr <> self implies sr.name <> self.name)

context Mutual_Exclusion_Resource
	inv i_2_1_f: 
		Model.Element_List -> select(e | e.oclIsKindOf(Mutual_Exclusion_Resource))
	                       -> forAll(m | m <> self implies m.name <> self.name)

context Operation
	inv i_2_1_g: 
		Model.Element_List -> select(e | e.oclIsKindOf(Operation))
	                       -> forAll(o | o <> self implies o.name <> self.name)

context End_To_End_Flow
	inv i_2_1_h: 
		Model.Element_List -> select(e | e.oclIsKindOf(End_To_End_Flow))
	                       -> forAll(e2ef | e2ef <> self implies e2ef.name <> self.name)

context Workload_Event
	inv i_2_2_a:
		Owner.Flow_Element_List -> select(fe | fe.oclIsKindOf(Workload_Event))
		                        -> forAll(we | we <> self implies we.oclAsType(Workload_Event).name <> self.name)

context Internal_Event
	inv i_2_3_a:
		Owner.Flow_Element_List -> select(fe | fe.oclIsTypeOf(Internal_Event))
		                        -> forAll(ie | ie <> self implies ie.oclAsType(Internal_Event).name <> self.name)

context End_To_End_Flow
	inv i_2_4_a: 
		Flow_Element_List -> exists(fe | fe.oclIsTypeOf(Step))

context Thread
	inv i_2_5_a_I: 
		self.Scheduling_Parameters.oclIsKindOf(Interrupt_Based_Params) or 
		self.Scheduling_Parameters.oclIsTypeOf(Non_Preemptible_FP_Params) or
		self.Scheduling_Parameters.oclIsTypeOf(Fixed_Priority_Params) or
		self.Scheduling_Parameters.oclIsTypeOf(Polling_Params) or 
		self.Scheduling_Parameters.oclIsKindOf(Periodic_Server_Params) or
		self.Scheduling_Parameters.oclIsKindOf(EDF_Based_Params) or 
		self.Scheduling_Parameters.oclIsKindOf(Timetable_Driven_Params)

context Communication_Channel
	inv i_2_5_a_II: 
		self.Scheduling_Parameters.oclIsTypeOf(Non_Preemptible_FP_Params) or
		self.Scheduling_Parameters.oclIsTypeOf(Fixed_Priority_Params) or
		self.Scheduling_Parameters.oclIsTypeOf(Polling_Params) or
		self.Scheduling_Parameters.oclIsKindOf(Periodic_Server_Comm_Params) or 
		self.Scheduling_Parameters.oclIsKindOf(EDF_Based_Params) or 
		self.Scheduling_Parameters.oclIsKindOf(Timetable_Driven_Params) or
		self.Scheduling_Parameters.oclIsTypeOf(AFDX_Virtual_Link) 

context Composite_Operation
	inv i_2_6_a:
		not Operation_List -> includes(self)

context Composite_Message
	inv i_2_7_a:
		not Message_List -> includes(self)
				
context Mutual_Exclusion_Resource
	inv i_2_8_a: 
		Simple_Operation.allInstances() -> exists(so | so.Mutex_List -> includes(self) or 
		                                               so.Mutex_To_Lock_List -> includes(self) or 
		                                               so.Mutex_To_Unlock_List -> includes(self))
		                                               
--context Join
--	inv i_2_9_a:
		
		
--context Hard_Global_Deadline
--	inv i_2_10_a:
		

--context Soft_Global_Deadline
--	inv i_2_11_a:
		

--context Max_Output_Jitter_Req
--	inv i_2_12_a:
		

--context Global_Max_Miss_Ratio
--	inv i_2_13_a:
		

context Step
	inv i_2_14_a_Step:
		Owner.Flow_Element_List -> includes(Input_Event) 

context Delay
	inv i_2_14_a_Delay:
		Owner.Flow_Element_List -> includes(Input_Event) 
		
context Rate_Divisor
	inv i_2_14_a_Rate_Divisor:
		Owner.Flow_Element_List -> includes(Input_Event)
		
context Fork
	inv i_2_14_a_Fork:
		Owner.Flow_Element_List -> includes(Input_Event)
		
context Branch
	inv i_2_14_a_Branch:
		Owner.Flow_Element_List -> includes(Input_Event)
		
context Queried_Branch
	inv i_2_14_a_Queried_Branch:
		Owner.Flow_Element_List -> includes(Input_Event)
		
context Message_Delivery
	inv i_2_14_a_Message_Delivery:
		Owner.Flow_Element_List -> includes(Input_Event)
		
context Message_Fork
	inv i_2_14_a_Message_Fork:
		Owner.Flow_Element_List -> includes(Input_Event)
		
context Message_Branch
	inv i_2_14_a_Message_Branch:
		Owner.Flow_Element_List -> includes(Input_Event)

context Join
	inv i_2_14_a_Join:
		Input_Event_List -> forAll(ev | Owner.Flow_Element_List -> includes(ev)) 

context Merge
	inv i_2_14_a_Merge:
		Input_Event_List -> forAll(ev | Owner.Flow_Element_List -> includes(ev)) 

context Workload_Event
	inv i_2_14_b:
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Step)) -> 
		                           exists(st | st.oclAsType(Step).Input_Event = self) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsKindOf(Delay)) -> 
		                           exists(de | de.oclAsType(Delay).Input_Event = self) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Rate_Divisor)) -> 
		                           exists(rd | rd.oclAsType(Rate_Divisor).Input_Event = self) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Fork)) -> 
		                           exists(fo | fo.oclAsType(Fork).Input_Event = self) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Branch)) -> 
		                           exists(br | br.oclAsType(Branch).Input_Event = self) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Queried_Branch)) -> 
		                           exists(qb | qb.oclAsType(Queried_Branch).Input_Event = self) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Join)) -> 
		                           exists(jo | jo.oclAsType(Join).Input_Event_List -> includes(self)) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Merge)) -> 
		                           exists(me | me.oclAsType(Merge).Input_Event_List -> includes(self)) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Message_Delivery)) -> 
		                           exists(md | md.oclAsType(Message_Delivery).Input_Event = self) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Message_Fork)) -> 
		                           exists(mf | mf.oclAsType(Message_Fork).Input_Event = self) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Message_Branch)) -> 
		                           exists(mb | mb.oclAsType(Message_Branch).Input_Event = self)

context Workload_Event
	inv i_2_14_c:
	   (Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Step)) -> 
	   		                       select(st | st.oclAsType(Step).Input_Event = self) -> size() + 
		Owner.Flow_Element_List -> select(eh | eh.oclIsKindOf(Delay)) -> 
		                           select(de | de.oclAsType(Delay).Input_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Rate_Divisor)) -> 
		                           select(rd | rd.oclAsType(Rate_Divisor).Input_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Fork)) -> 
		                           select(fo | fo.oclAsType(Fork).Input_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Branch)) -> 
		                           select(br | br.oclAsType(Branch).Input_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Queried_Branch)) -> 
		                           select(qb | qb.oclAsType(Queried_Branch).Input_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Join)) -> 
		                           select(jo | jo.oclAsType(Join).Input_Event_List -> includes(self)) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Merge)) -> 
		                           select(me | me.oclAsType(Merge).Input_Event_List -> includes(self)) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Message_Delivery)) -> 
		                           select(md | md.oclAsType(Message_Delivery).Input_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Message_Fork)) -> 
		                           select(mf | mf.oclAsType(Message_Fork).Input_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Message_Branch)) -> 
		                           select(mb | mb.oclAsType(Message_Branch).Input_Event = self) -> size()
		) < 2
		
context Internal_Event
	inv i_2_14_d:
	   (Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Step)) -> 
	   		                       select(st | st.oclAsType(Step).Input_Event = self) -> size() + 
		Owner.Flow_Element_List -> select(eh | eh.oclIsKindOf(Delay)) -> 
		                           select(de | de.oclAsType(Delay).Input_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Rate_Divisor)) -> 
		                           select(rd | rd.oclAsType(Rate_Divisor).Input_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Fork)) -> 
		                           select(fo | fo.oclAsType(Fork).Input_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Branch)) -> 
		                           select(br | br.oclAsType(Branch).Input_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Queried_Branch)) -> 
		                           select(qb | qb.oclAsType(Queried_Branch).Input_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Join)) -> 
		                           select(jo | jo.oclAsType(Join).Input_Event_List -> includes(self)) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Merge)) -> 
		                           select(me | me.oclAsType(Merge).Input_Event_List -> includes(self)) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Message_Delivery)) -> 
		                           select(md | md.oclAsType(Message_Delivery).Input_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Message_Fork)) -> 
		                           select(mf | mf.oclAsType(Message_Fork).Input_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Message_Branch)) -> 
		                           select(mb | mb.oclAsType(Message_Branch).Input_Event = self) -> size()
		) < 2

context Step
	inv i_2_15_a_Step:
		Owner.Flow_Element_List -> includes(Output_Event)

context Delay
	inv i_2_15_a_Delay:
		Owner.Flow_Element_List -> includes(Output_Event)

context Rate_Divisor
	inv i_2_15_a_Rate_Divisor:
		Owner.Flow_Element_List -> includes(Output_Event)

context Join
	inv i_2_15_a_Join:
		Owner.Flow_Element_List -> includes(Output_Event)

context Merge
	inv i_2_15_a_Merge:
		Owner.Flow_Element_List -> includes(Output_Event)

context Message_Delivery
	inv i_2_15_a_Message_Delivery:
		Owner.Flow_Element_List -> includes(Output_Event)

context Fork
	inv i_2_15_a_Fork:
		Output_Event_List -> forAll(ev | Owner.Flow_Element_List -> includes(ev))
		
context Branch
	inv i_2_15_a_Branch:
		Output_Event_List -> forAll(ev | Owner.Flow_Element_List -> includes(ev))

context Queried_Branch
	inv i_2_15_a_Queried_Branch:
		Output_Event_List -> forAll(ev | Owner.Flow_Element_List -> includes(ev))

context Message_Fork
	inv i_2_15_a_Message_Fork:
		Output_Event_List -> forAll(ev | Owner.Flow_Element_List -> includes(ev))
		
context Message_Branch
	inv i_2_15_a_Message_Branch:
		Output_Event_List -> forAll(ev | Owner.Flow_Element_List -> includes(ev))

context Internal_Event
	inv i_2_15_b:
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Step)) -> 
		                           exists(s | s.oclAsType(Step).Output_Event = self) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsKindOf(Delay)) -> 
		                           exists(d | d.oclAsType(Delay).Output_Event = self) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Rate_Divisor)) -> 
		                           exists(rd | rd.oclAsType(Rate_Divisor).Output_Event = self) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Fork)) -> 
		                           exists(f | f.oclAsType(Fork).Output_Event_List -> includes(self)) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Branch)) -> 
		                           exists(b | b.oclAsType(Branch).Output_Event_List -> includes(self)) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Queried_Branch)) -> 
		                           exists(qb | qb.oclAsType(Queried_Branch).Output_Event_List -> includes(self)) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Join)) -> 
		                           exists(j | j.oclAsType(Join).Output_Event = self) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Merge)) -> 
		                           exists(m | m.oclAsType(Merge).Output_Event = self) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Message_Delivery)) -> 
		                           exists(md | md.oclAsType(Message_Delivery).Output_Event = self) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Message_Fork)) -> 
		                           exists(mf | mf.oclAsType(Message_Fork).Output_Event_List -> includes(self)) 
		or
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Message_Branch)) -> 
		                           exists(mb | mb.oclAsType(Message_Branch).Output_Event_List -> includes(self))
		
context Internal_Event
	inv i_2_15_c:
	   (Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Step)) -> 
		                           select(st | st.oclAsType(Step).Output_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsKindOf(Delay)) -> 
		                           select(de | de.oclAsType(Delay).Output_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Rate_Divisor)) -> 
		                           select(rd | rd.oclAsType(Rate_Divisor).Output_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Fork)) -> 
		                           select(fo | fo.oclAsType(Fork).Output_Event_List -> includes(self)) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Branch)) -> 
		                           select(br | br.oclAsType(Branch).Output_Event_List -> includes(self)) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Queried_Branch)) -> 
		                           select(qb | qb.oclAsType(Queried_Branch).Output_Event_List -> includes(self)) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Join)) -> 
		                           select(jo | jo.oclAsType(Join).Output_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Merge)) -> 
		                           select(me | me.oclAsType(Merge).Output_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Message_Delivery)) -> 
		                           select(md | md.oclAsType(Message_Delivery).Output_Event = self) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Message_Fork)) -> 
		                           select(mf | mf.oclAsType(Message_Fork).Output_Event_List -> includes(self)) -> size() +
		Owner.Flow_Element_List -> select(eh | eh.oclIsTypeOf(Message_Branch)) -> 
		                           select(mb | mb.oclAsType(Message_Branch).Output_Event_List -> includes(self)) -> size()
		) < 2


-- ------------------------------
-- Regarding sets of associations
-- ------------------------------

context Regular_Processor
	inv i_3_1_a: 
		if not System_Timer.oclIsUndefined() then 
			Timer_List -> includes(System_Timer)
		else
			true
		endif
		
context Primary_Scheduler
	inv i_3_2_a: 
		((Policy.oclIsTypeOf(Fixed_Priority_Policy) or 
		  Policy.oclIsTypeOf(EDF_Policy) or 
		  Policy.oclIsTypeOf(Timetable_Driven_Policy)) and Host.oclIsKindOf(Computing_Resource)) 		                            
		or 
		((Policy.oclIsTypeOf(FP_Packet_Based_Policy) or 
		  Policy.oclIsTypeOf(EDF_Policy) or 
		  Policy.oclIsTypeOf(Timetable_Driven_Packet_Based_Policy)) and Host.oclIsTypeOf(Packet_Based_Network)) 
		or 
		(Policy.oclIsTypeOf(AFDX_Policy) and Host.oclIsTypeOf(AFDX_Link))

context Thread
	inv i_3_3_a_I: 
		self.Scheduler.oclAsType(Primary_Scheduler).Host.oclIsKindOf(Computing_Resource)

context Communication_Channel
	inv i_3_3_a_II: 
		self.Scheduler.oclAsType(Primary_Scheduler).Host.oclIsKindOf(Network)

context Schedulable_Resource
	inv i_3_4_a: 
		self.Scheduling_Parameters.oclIsKindOf(Priority_Based_Params) and 
		self.Scheduler.Policy.oclIsTypeOf(Fixed_Priority_Policy) 
	    or
	    self.Scheduling_Parameters.oclIsKindOf(Interrupt_Based_Params) and 
	    self.Scheduler.Policy.oclIsTypeOf(Fixed_Priority_Policy) 
	    or 
	    self.Scheduling_Parameters.oclIsKindOf(EDF_Based_Params) and 
	    self.Scheduler.Policy.oclIsTypeOf(EDF_Policy) 
	    or 
	    self.Scheduling_Parameters.oclIsKindOf(Timetable_Driven_Params) and 
	    self.Scheduler.Policy.oclIsKindOf(Timetable_Driven)
	    or
	    self.Scheduling_Parameters.oclIsTypeOf(AFDX_Virtual_Link) and 
	    self.Scheduler.Policy.oclIsTypeOf(AFDX_Policy)
	    
context Thread
	inv i_3_4_b_I:
		if self.Scheduling_Parameters.oclIsKindOf(Priority_Based_Params) then
			self.Scheduling_Parameters.oclAsType(Priority_Based_Params).Priority <= self.Scheduler.Policy.oclAsType(Fixed_Priority_Policy).Max_Priority 
			and
			self.Scheduling_Parameters.oclAsType(Priority_Based_Params).Priority >= self.Scheduler.Policy.oclAsType(Fixed_Priority_Policy).Min_Priority
		else
			true
		endif
		
context Communication_Channel
	inv i_3_4_b_II:
		if self.Scheduling_Parameters.oclIsKindOf(Priority_Based_Params) then
			self.Scheduling_Parameters.oclAsType(Priority_Based_Params).Priority <= self.Scheduler.Policy.oclAsType(FP_Packet_Based_Policy).Max_Priority 
			and
			self.Scheduling_Parameters.oclAsType(Priority_Based_Params).Priority >= self.Scheduler.Policy.oclAsType(FP_Packet_Based_Policy).Min_Priority
		else
			true
		endif

context Step
	inv i_3_5_a: 
		Step_Operation.oclIsKindOf(Code_Operation) and Step_Schedulable_Resource.oclIsTypeOf(Thread) 
	    or 
	    Step_Operation.oclIsKindOf(Message_Operation) and Step_Schedulable_Resource.oclIsTypeOf(Communication_Channel)

context Timer
	inv i_3_6_a:
		Timed_Event.allInstances() -> exists(te | te.Timer = self)
		or
		Delay.allInstances() -> exists(d | d.Timer = self)

context Thread
	inv i_3_7_a:
		Step.allInstances() -> exists(s | s.Step_Schedulable_Resource = self)
		or
		Packet_Driver.allInstances() -> exists(pd | pd.Packet_Server = self)
		or
		Character_Packet_Driver.allInstances() -> exists(cpd | cpd.Character_Server = self)
		or
		RTEP_Packet_Driver.allInstances() -> exists(rpd | rpd.Packet_Interrupt_Server = self)

context Communication_Channel
	inv i_3_7_b:
		Step.allInstances() -> exists(s | s.Step_Schedulable_Resource = self)

context Message_Operation
	inv i_3_8_a:
    	Step.allInstances() -> exists(s | s.Step_Operation = self) 
    	or
    	Composite_Message.allInstances() -> exists(cm | cm.Message_List -> includes(self))

context Code_Operation
	inv i_3_9_a: 
	    Step.allInstances() -> exists(s | s.Step_Operation = self)
	    or
	    Packet_Driver.allInstances() -> exists(pd | pd.Packet_Receive_Operation = self or 
	    	                                        pd.Packet_Send_Operation = self) 
	    or 
	    Character_Packet_Driver.allInstances() -> exists(cpd | cpd.Character_Receive_Operation = self or 
	    	                                                   cpd.Character_Send_Operation = self)
	    or
	    RTEP_Packet_Driver.allInstances() -> exists(rpd | rpd.Packet_ISR_Operation = self or 
	    	                                              rpd.Packet_Discard_Operation = self or 
	    	                                              rpd.Packet_Retransmission_Operation = self or 
	    	                                              rpd.Token_Retransmission_Operation = self or 
	    	                                              rpd.Token_Manage_Operation = self or 
	    	                                              rpd.Token_Check_Operation = self) 
	    or 
	    Composite_Operation.allInstances() -> exists(co | co.Operation_List -> includes(self))

context Simple_Operation
	inv i_3_10_a: 
		not (
			(not Mutex_List -> isEmpty()) and (not Mutex_To_Lock_List -> isEmpty())
		)

context Simple_Operation
	inv i_3_10_b: 
		not (
			(not Mutex_List -> isEmpty()) and (not Mutex_To_Unlock_List -> isEmpty())
		)

endpackage