// Place global declarations here.
const int BIG = 199999;
const int MAXTIME = 5500;
typedef int[0,MAXTIME] time_t;
const int MAXPRI = 50;
typedef int[0,MAXPRI] pri_t;
const int rid_n = 1; // Number of resources
typedef int[0,rid_n-1] rid_t;
const int tid_n = 2; // Number of tasks
typedef int[0,tid_n] tid_t;
typedef int[1,tid_n] tid_arr;
clock gclock;
bool error = false;
bool error1[tid_arr] = {false, false};
bool error2 = false;
int gbudget[rid_t];
clock cbudget[rid_t];
int[0,2] sPrdIndc[rid_t];
bool tPrdIndc[tid_t];
bool tRunIndc[tid_t];
typedef struct {
pri_t pri;
time_t initial_offset;
time_t offset;
time_t min_period;
time_t max_period;
time_t deadline;
time_t bcet;
time_t wcet;
bool preemptive;
} task_t;
clock curTime[tid_arr];
clock exeTime[tid_arr];
clock rt[tid_arr];
broadcast chan startSTask[tid_arr];
/* TASK Celling Priority */
typedef struct {
pri_t pri;
int[0,rid_n] pid;
time_t initial_offset;
time_t offset;
time_t min_period;
time_t max_period;
time_t deadline;
time_t bcet;
time_t wcet;
bool preemptive;
bool status;
} tstat_t;
tstat_t tstat[tid_arr];
typedef struct {
int[0,tid_n+1] length;
tid_t element[tid_arr];
} queue_t;
queue_t rq[rid_t] ;
typedef struct{
int val;
int prob;
} p_vector_t ;
const int p_vector_n = 2;
const int timing_attr_n = 3;
typedef p_vector_t t_prob_t[p_vector_n];
typedef t_prob_t t_timing_attr_t[timing_attr_n];
// 0 - Period, 1- Execution Time, 2 - Deadline
const int PERIOD = 0;
const int EXECUTION = 1;
const int DEADLINE = 2;
const t_timing_attr_t ta[tid_arr]={
//task1
{
{{5, 2},{6, 8}}, /*{{35, 4},{36, 2},{37, 2},{38, 1},{39, 1}}, Period*/
{{2, 1},{2, 1}}, /*{{5, 1},{ 4, 2},{ 3, 3},{ 2, 4},{ 1, 5}} Execution*/
{{5, 2},{6, 8}} /*{{35, 4},{36, 2},{37, 2},{38, 2},{39, 1}} Deadline*/
},
//task 2
{
{{7, 3},{8, 7}}, /*{{45, 5},{44, 2},{43, 2},{42, 1},{41, 0}}, Period*/
{{3, 9},{4, 1}}, /*{{10, 1},{ 9, 2},{ 8, 3},{ 7, 2},{ 6, 1}}, Execution*/
{{7, 3},{8, 7}} /*{{45, 5},{44, 2},{43, 1},{42, 0},{40, 0}} Deadline*/
}
/*,
//task 3
{
{{75, 5},{76, 2},{77, 2},{78, 1},{79, 0}},
{{15, 1},{16, 2},{17, 3},{18, 2},{19, 1}},
{{75, 5},{76, 2},{77, 2},{78, 1},{79, 0}}} */
};
//ta[tid][arrv|exe|deadline][probid].val
//ta[tid][arrv|exe|deadline][probid].prob
/* Resource Behavior */
typedef int[1,3] policy_t ;
const policy_t EDF = 1;
const policy_t FIFO = 2;
const policy_t FP = 3;
urgent broadcast chan r_req[rid_t];
urgent broadcast chan dummy;
broadcast chan r_sup[rid_t][tid_arr];
broadcast chan finished[rid_t];
broadcast chan run_sched[policy_t][rid_t];
broadcast chan ack_sched[policy_t][rid_t];
bool r_preemptive[rid_t];
const int runTime = 100000;
void enque(rid_t rid, tid_arr tid){
rq[rid].element[++rq[rid].length]=tid;
}
void deque(rid_t rid){
int[1,tid_n+1] i;
for(i=1;i<rq[rid].length;i++) {
rq[rid].element[i-1] = rq[rid].element[i];
}
rq[rid].element[rq[rid].length-1] = 0;
rq[rid].length--;
}
void insert_at(rid_t rid, tid_arr place, tid_arr tid){
tid_t i;
for(i = rq[rid].length; i > place; i--){
rq[rid].element[i] = rq[rid].element[i-1];
}
rq[rid].element[place] = tid;
}
void delete_tid(rid_t rid, tid_arr tid){
tid_t i=1;
assert(i <= rq[rid].length);
while(rq[rid].element[i]!=tid) {
i++;
assert(i <= rq[rid].length);
}
while(i < rq[rid].length){
rq[rid].element[i] = rq[rid].element[i+1];
i++;
}
rq[rid].element[i] = 0;
rq[rid].length--;
}
bool is_preemptive(rid_t rid){
return (r_preemptive[rid] && tstat[rq[rid].element[1]].preemptive);
}
typedef task_t taskatt_t[tid_arr];
void set_mode(tid_arr tid, task_t task){
tstat[tid].pri = task.pri;
tstat[tid].initial_offset = task.initial_offset;
tstat[tid].offset = task.offset;
tstat[tid].min_period = task.min_period ;
tstat[tid].max_period = task.max_period;
tstat[tid].deadline = task.deadline;
tstat[tid].bcet = task.bcet;
tstat[tid].wcet = task.wcet ;
tstat[tid].preemptive = task.preemptive;
}
STask
const tid_arr tid, task_t task
// Place local declarations here.
clock x;
//bool isTaskSched() {
// return (rq[tstat[tid].pid].element[1] == tid && supplying[tstat[tid].pid]);
//}
bool isTaskSched() {
return (rq[tstat[tid].pid].element[1] == tid);
}
Init
MissDL
Run
PDone
WaitOffset
Resource
const rid_t rid, const bool preemptive, const policy_t policy
Assign
WaitSched
ReqSched
InUse
Idle
Sched_FP
rid_t rid;
void policy_FP(rid_t rid){
tid_t place;
tid_t t;
place = (is_preemptive(rid)? 1:2);
t = rq[rid].element[rq[rid].length];
while (place < rq[rid].length && tstat[rq[rid].element[place]].pri > tstat[t].pri){
place++;
}
insert_at(rid, place, t);
}
AckSchedReq
WaitSchedReq
Sched_FIFO
rid_t rid;
void policy_FIFO(rid_t rid){
rq[rid].length++;
}
AckSchedReq
WaitSchedReq
Sched_EDF
tid_t place;
tid_t t;
rid_t rid;
int[1,2] start_pos(rid_t rid) {
return (is_preemptive(rid)?1:2);
}
AckSchedReq
Assigning
WaitSchedReq
SEvnTrigDProb
const tid_arr tid
clock x;
MissDL
Init
Dispatching
AssingPDeadline
AssingPExecutionTime
AssingPPeriod
WaitPeriodEnd
RTAnalyser
int[1,tid_n+1] j;
Initializing
Start
Wait
End
const task_t task[tid_arr] = {
{9, 0, 0, 0, 0, 0, 0, 0, true},
{8, 0, 0, 0, 0, 0, 0, 0, true}
};
CPU1 = Resource(0, true, FP);
Task1 = STask(1, task[1]);
Task2 = STask(2, task[2]);
system
Task1, Task2 //, Task3
, CPU1, Sched_FP
, SEvnTrigDProb, RTAnalyser
;
Pr[rt[1]<=runTime](<> gclock>=runTime)
E[<=1000;1000](max:rt[2])
E[<=1000;1000](max:rt[1])
Pr[rt[2]<=runTime](<> gclock>=runTime)
Pr[rt[1]<=runTime](<> gclock>=runTime)
Pr[<=1000] (<> error)
A[] error != 1
simulate 1[<=300]{tPrdIndc[1]*2, tRunIndc[1], 3+tPrdIndc[2]*2, 3+tRunIndc[2]}
E<> deadlock && not RTAnalyser.End