Commit ae8664ab authored by Björn Brandenburg's avatar Björn Brandenburg

Remove HTML files

An up-to-date version can always be generated with 'make html'.
parent f7e398f8
*.d
*.glob
*.vo
*.html
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