Commit 2f60e03c authored by Felipe Cerqueira's avatar Felipe Cerqueira

Commit HTML files

parent 7507d62e
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"/>
<link href="coqdoc.css" rel="stylesheet" type="text/css"/>
<title>task_arrival</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library task_arrival</h1>
<div class="code">
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <a class="idref" href="Vbase.html#"><span class="id" type="library">Vbase</span></a> <a class="idref" href="task.html#"><span class="id" type="library">task</span></a> <a class="idref" href="job.html#"><span class="id" type="library">job</span></a> <a class="idref" href="schedule.html#"><span class="id" type="library">schedule</span></a> <a class="idref" href="util_lemmas.html#"><span class="id" type="library">util_lemmas</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="library">ssreflect</span> <span class="id" type="library">ssrbool</span> <span class="id" type="library">eqtype</span> <span class="id" type="library">ssrnat</span> <span class="id" type="library">seq</span> <span class="id" type="library">fintype</span> <span class="id" type="library">bigop</span>.<br/>
<br/>
<span class="comment">(*&nbsp;Properties&nbsp;of&nbsp;the&nbsp;job&nbsp;arrival.&nbsp;*)</span><br/>
<span class="id" type="keyword">Module</span> <a name="SporadicTaskArrival"><span class="id" type="module">SporadicTaskArrival</span></a>.<br/>
<br/>
<span class="id" type="keyword">Import</span> <span class="id" type="var">SporadicTaskset</span> <span class="id" type="var">Schedule</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="id" type="keyword">Section</span> <a name="SporadicTaskArrival.ArrivalModels"><span class="id" type="section">ArrivalModels</span></a>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;Assume&nbsp;the&nbsp;task&nbsp;period&nbsp;is&nbsp;known.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Context</span> {<span class="id" type="var">sporadic_task</span>: <span class="id" type="abbreviation">eqType</span>}.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Variable</span> <a name="SporadicTaskArrival.ArrivalModels.task_period"><span class="id" type="variable">task_period</span></a>: <a class="idref" href="task_arrival.html#SporadicTaskArrival.ArrivalModels.sporadic_task"><span class="id" type="variable">sporadic_task</span></a> -&gt; <a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" type="inductive">nat</span></a>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Context</span> {<span class="id" type="var">Job</span>: <span class="id" type="abbreviation">eqType</span>}.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Variable</span> <a name="SporadicTaskArrival.ArrivalModels.arr_seq"><span class="id" type="variable">arr_seq</span></a>: <a class="idref" href="arrival_sequence.html#ArrivalSequence.arrival_sequence"><span class="id" type="definition">arrival_sequence</span></a> <a class="idref" href="task_arrival.html#SporadicTaskArrival.ArrivalModels.Job"><span class="id" type="variable">Job</span></a>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Variable</span> <a name="SporadicTaskArrival.ArrivalModels.job_task"><span class="id" type="variable">job_task</span></a>: <a class="idref" href="task_arrival.html#SporadicTaskArrival.ArrivalModels.Job"><span class="id" type="variable">Job</span></a> -&gt; <a class="idref" href="task_arrival.html#SporadicTaskArrival.ArrivalModels.sporadic_task"><span class="id" type="variable">sporadic_task</span></a>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;Then,&nbsp;we&nbsp;define&nbsp;the&nbsp;sporadic&nbsp;task&nbsp;model&nbsp;as&nbsp;follows.*)</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Definition</span> <a name="SporadicTaskArrival.sporadic_task_model"><span class="id" type="definition">sporadic_task_model</span></a> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">forall</span> (<span class="id" type="var">j</span> <span class="id" type="var">j'</span>: <a class="idref" href="arrival_sequence.html#ArrivalSequence.JobIn"><span class="id" type="record">JobIn</span></a> <a class="idref" href="task_arrival.html#SporadicTaskArrival.ArrivalModels.arr_seq"><span class="id" type="variable">arr_seq</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="task_arrival.html#j"><span class="id" type="variable">j</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Init.Logic.html#:type_scope:x_'<>'_x"><span class="id" type="notation">&lt;&gt;</span></a> <a class="idref" href="task_arrival.html#j'"><span class="id" type="variable">j'</span></a> -&gt; <span class="comment">(*&nbsp;Given&nbsp;two&nbsp;different&nbsp;jobs&nbsp;j&nbsp;and&nbsp;j'&nbsp;...&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="task_arrival.html#SporadicTaskArrival.ArrivalModels.job_task"><span class="id" type="variable">job_task</span></a> <a class="idref" href="task_arrival.html#j"><span class="id" type="variable">j</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Init.Logic.html#:type_scope:x_'='_x"><span class="id" type="notation">=</span></a> <a class="idref" href="task_arrival.html#SporadicTaskArrival.ArrivalModels.job_task"><span class="id" type="variable">job_task</span></a> <a class="idref" href="task_arrival.html#j'"><span class="id" type="variable">j'</span></a> -&gt; <span class="comment">(*&nbsp;...&nbsp;of&nbsp;the&nbsp;same&nbsp;task,&nbsp;...&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="arrival_sequence.html#ArrivalSequence.job_arrival"><span class="id" type="definition">job_arrival</span></a> <a class="idref" href="task_arrival.html#j"><span class="id" type="variable">j</span></a> <span class="id" type="notation">&lt;=</span> <a class="idref" href="arrival_sequence.html#ArrivalSequence.job_arrival"><span class="id" type="definition">job_arrival</span></a> <a class="idref" href="task_arrival.html#j'"><span class="id" type="variable">j'</span></a> -&gt; <span class="comment">(*&nbsp;...&nbsp;if&nbsp;the&nbsp;arrival&nbsp;of&nbsp;j&nbsp;precedes&nbsp;the&nbsp;arrival&nbsp;of&nbsp;j'&nbsp;...,&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;then&nbsp;the&nbsp;arrival&nbsp;of&nbsp;j&nbsp;and&nbsp;the&nbsp;arrival&nbsp;of&nbsp;j'&nbsp;are&nbsp;separated&nbsp;by&nbsp;at&nbsp;least&nbsp;one&nbsp;period.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="arrival_sequence.html#ArrivalSequence.job_arrival"><span class="id" type="definition">job_arrival</span></a> <a class="idref" href="task_arrival.html#j'"><span class="id" type="variable">j'</span></a> <span class="id" type="notation">&gt;=</span> <a class="idref" href="arrival_sequence.html#ArrivalSequence.job_arrival"><span class="id" type="definition">job_arrival</span></a> <a class="idref" href="task_arrival.html#j"><span class="id" type="variable">j</span></a> <span class="id" type="notation">+</span> <a class="idref" href="task_arrival.html#SporadicTaskArrival.ArrivalModels.task_period"><span class="id" type="variable">task_period</span></a> (<a class="idref" href="task_arrival.html#SporadicTaskArrival.ArrivalModels.job_task"><span class="id" type="variable">job_task</span></a> <a class="idref" href="task_arrival.html#j"><span class="id" type="variable">j</span></a>).<br/>
<br/>
&nbsp;&nbsp;<span class="id" type="keyword">End</span> <a class="idref" href="task_arrival.html#SporadicTaskArrival.ArrivalModels"><span class="id" type="section">ArrivalModels</span></a>.<br/>
<br/>
<span class="id" type="keyword">End</span> <a class="idref" href="task_arrival.html#"><span class="id" type="module">SporadicTaskArrival</span></a>.<br/>
</div>
</div>
<div id="footer">
<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>
</div>
</body>
</html>
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment