package uniprocessor_priority
public
	
	annex resolute {** 
			SystemWideReq1() <= ** "All threads have a period" ** 
			forall (t: thread). HasPeriod(t)
			HasPeriod(t : thread) <= ** "Thread " t " has a period" ** 
			has_property(t,Timing_Properties::Period)			
			
					**};
	
--	with Cheddar_Properties;
	thread Tache
		properties
			Dispatch_Protocol => Periodic;
	end Tache;
	thread implementation Tache.impl		
	end Tache.impl;
	
	process application
		
	end application;
	process implementation application.impl
		subcomponents
			T1: thread tache.impl
			{
				Compute_Execution_time => 1ms..1ms;
				Deadline => 4ms;
				Period => 5ms;
				Priority => 2;				
			};
			T2: thread tache.impl
			{
				Compute_Execution_time => 2ms..2ms;
				Deadline => 3ms;
				Period => 4ms;
				Priority => 3;				
			};	
			T3: thread tache.impl
			{
				Compute_Execution_time => 1ms..1ms;
				Deadline => 4ms;
				Period => 4ms;
				Priority => 1;		
			};				
	end application.impl;
	
	processor cpu
		properties
			Scheduling_Protocol =>(POSIX_1003_HIGHEST_PRIORITY_FIRST_PROTOCOL);
--			Cheddar_Properties::Preemptive_Scheduler => true;			
	end cpu;
	
	system priority		
	end priority;
	system implementation priority.impl
		subcomponents
			process1: process application.impl;
			cpu1 : processor cpu;			
		properties
			Actual_Processor_Binding =>(reference (cpu1)) applies to process1;	
		annex resolute {** 		
			prove (SystemWideReq1()
					**};
	end priority.impl;
	
end uniprocessor_priority;