This file is indexed.

/usr/share/mozart/doc/system/node29.html is in mozart-doc 1.4.0-8ubuntu1.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below.

1
2
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD><TITLE>6.1 Serialization for Unary Resources</TITLE><LINK href="ozdoc.css" rel="stylesheet" type="text/css"></HEAD><BODY><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="node28.html">- Up -</A></TD><TD><A href="node30.html#section.schedule.distribute">Next &gt;&gt;</A></TD></TR></TABLE><DIV id="section.schedule.unary"><H2><A name="section.schedule.unary">6.1 Serialization for Unary Resources</A></H2><P><A name="label279"></A><EM>Serializing</EM> a unary resource which can execute at most one task simultaneously means that the tasks must be scheduled non-overlapping in time. </P><P>The following conventions hold. The argument <I>StartR</I> is a record of finite domain integers denoting start times of tasks. The argument <I>DurR</I> is a record of integers denoting durations of tasks. The arities of <I>StartR</I> and <I>DurR</I> must be equal. </P><P>The integers and literals occurring in <I>TasksLIvv</I> denote the tasks to be scheduled. Each element of <I>TasksLIvv</I> must occur in the arity of <I>StartR</I>. The tasks occurring in the vectors <I>TasksLIv</I> are scheduled on the same resource. </P><P></P><P></P><DL><DT><A name="label281"></A> <CODE>serializedDisj</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{Schedule<SPAN class="keyword">.</SPAN>serializedDisj&nbsp;</CODE><CODE>+<I>TasksLIvv</I></CODE><CODE>&nbsp;</CODE><CODE>+<I>StartR</I></CODE><CODE>&nbsp;</CODE><CODE>+<I>DurR</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>creates a propagator, which states that all tasks <I>TasksLIv</I> scheduled on the same resource must not overlap in time. </P><P>The propagator does the same propagation as the conjunction of all reified constraints modelling that two tasks must not overlap in time, i.&nbsp;e. </P><BLOCKQUOTE class="code"><CODE>(</CODE><I>StartR</I><CODE><SPAN class="keyword">.</SPAN></CODE><I>T1</I><CODE>&nbsp;<SPAN class="keyword">+</SPAN>&nbsp;</CODE><I>DurR</I><CODE><SPAN class="keyword">.</SPAN></CODE><I>T1</I><CODE>&nbsp;<SPAN class="keyword">=&lt;:</SPAN>&nbsp;</CODE><I>StartR</I><CODE><SPAN class="keyword">.</SPAN></CODE><I>T2</I><CODE>)&nbsp;<SPAN class="keyword">+</SPAN>&nbsp;<BR>(</CODE><I>StartR</I><CODE><SPAN class="keyword">.</SPAN></CODE><I>T2</I><CODE>&nbsp;<SPAN class="keyword">+</SPAN>&nbsp;</CODE><I>DurR</I><CODE><SPAN class="keyword">.</SPAN></CODE><I>T2</I><CODE>&nbsp;<SPAN class="keyword">=&lt;:</SPAN>&nbsp;</CODE><I>StartR</I><CODE><SPAN class="keyword">.</SPAN></CODE><I>T1</I><CODE>)&nbsp;<SPAN class="keyword">=:</SPAN>&nbsp;1</CODE></BLOCKQUOTE><P> where <I>T1</I> and <I>T2</I> are two tasks out of <I>TasksLIvv</I>. </P><P> Assume the following tasks and durations: </P><TABLE align="center" bgcolor="#f0f0e0"><TR valign="top"><TH><P>Task</P></TH><TH><P>Resource</P></TH><TH><P>Duration</P></TH></TR><TR valign="top"><TD><P><CODE>a</CODE></P></TD><TD><P><CODE>r</CODE></P></TD><TD><P><CODE>4</CODE></P></TD></TR><TR valign="top"><TD><P><CODE>b</CODE></P></TD><TD><P><CODE>r</CODE></P></TD><TD><P><CODE>6</CODE></P></TD></TR><TR valign="top"><TD><P><CODE>c</CODE></P></TD><TD><P><CODE>r</CODE></P></TD><TD><P><CODE>7</CODE></P></TD></TR><TR valign="top"><TD><P><CODE>d</CODE></P></TD><TD><P><CODE>s</CODE></P></TD><TD><P><CODE>7</CODE></P></TD></TR><TR valign="top"><TD><P><CODE>e</CODE></P></TD><TD><P><CODE>s</CODE></P></TD><TD><P><CODE>4</CODE></P></TD></TR></TABLE><P> In addition let us assume that no further restriction on the start times is given. </P><P>Then </P><BLOCKQUOTE class="code"><CODE>Dur&nbsp;&nbsp;&nbsp;=&nbsp;dur(a:4&nbsp;b:6&nbsp;c:7&nbsp;d:7&nbsp;e:4)<BR>Start&nbsp;=&nbsp;{FD<SPAN class="keyword">.</SPAN>record&nbsp;start&nbsp;[a&nbsp;b&nbsp;c&nbsp;d&nbsp;e]&nbsp;0<SPAN class="keyword">#</SPAN>FD<SPAN class="keyword">.</SPAN>sup}<BR>Tasks&nbsp;=&nbsp;(a<SPAN class="keyword">#</SPAN>b<SPAN class="keyword">#</SPAN>c)<SPAN class="keyword">#</SPAN>(d<SPAN class="keyword">#</SPAN>e)<BR>{Schedule<SPAN class="keyword">.</SPAN>serializedDisj&nbsp;Tasks&nbsp;Start&nbsp;Dur}</CODE></BLOCKQUOTE><P> serializes the tasks for the resources <CODE>r</CODE> and <CODE>s</CODE> (for <CODE>FD<SPAN class="keyword">.</SPAN>record</CODE> see <A href="node18.html#fd.record">*</A>). Note that the resources are kept anonymous, they are just reflected by the vector elements in <CODE>Tasks</CODE>. If we would like to make the resources more explicit we could use for <CODE>Tasks</CODE> the following: </P><BLOCKQUOTE class="code"><CODE>Tasks&nbsp;=&nbsp;tasks(r:[a&nbsp;b&nbsp;c]&nbsp;s:[d&nbsp;e])</CODE></BLOCKQUOTE><P> It also possible to use integers or names rather than atoms for the tasks. </P></DD><DT><A name="label283"></A> <CODE>serialized</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{Schedule<SPAN class="keyword">.</SPAN>serialized&nbsp;</CODE><CODE>+<I>TasksLIvv</I></CODE><CODE>&nbsp;</CODE><CODE>+<I>StartR</I></CODE><CODE>&nbsp;</CODE><CODE>+<I>DurR</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>creates a propagator, which states that all tasks <I>TasksLIv</I> scheduled on the same resource must not overlap in time. </P><P>The propagator does stronger propagation than <CODE>Schedule<SPAN class="keyword">.</SPAN>serializedDisj</CODE> by using so-called edge-finding. This type of edge-finding is a generalization of a technique described in <A href="bib.html#martin.96">[MS96]</A>. </P></DD><DT><A name="label285"></A> <CODE>taskIntervals</CODE></DT><DD><BLOCKQUOTE class="synopsis"><P></P><BLOCKQUOTE class="code"><CODE>{Schedule<SPAN class="keyword">.</SPAN>taskIntervals&nbsp;</CODE><CODE>+<I>TasksLIvv</I></CODE><CODE>&nbsp;</CODE><CODE>+<I>StartR</I></CODE><CODE>&nbsp;</CODE><CODE>+<I>DurR</I></CODE><CODE>}</CODE></BLOCKQUOTE><P></P></BLOCKQUOTE></DD><DD><P>creates a propagator, which states that all tasks <I>TasksLIv</I> scheduled on the same resource must not overlap in time. </P><P>The propagator does even stronger propagation than <CODE>Schedule<SPAN class="keyword">.</SPAN>serialized</CODE> by using so-called task-intervals&nbsp;<A href="bib.html#caseau.95">[CL95]</A>. The propagation of this propagator is slightly weaker than the propagation described in&nbsp;<A href="bib.html#caseau.95">[CL95]</A>. </P></DD></DL><P> </P></DIV><TABLE align="center" border="0" cellpadding="6" cellspacing="6" class="nav"><TR bgcolor="#DDDDDD"><TD><A href="node28.html">- Up -</A></TD><TD><A href="node30.html#section.schedule.distribute">Next &gt;&gt;</A></TD></TR></TABLE><HR><ADDRESS><A href="http://www.ps.uni-sb.de/~duchier/">Denys&nbsp;Duchier</A>, <A href="http://www.ps.uni-sb.de/~kornstae/">Leif&nbsp;Kornstaedt</A>, <A href="http://www.ps.uni-sb.de/~homik/">Martin&nbsp;Homik</A>, <A href="http://www.ps.uni-sb.de/~tmueller/">Tobias&nbsp;Müller</A>, <A href="http://www.ps.uni-sb.de/~schulte/">Christian&nbsp;Schulte</A> and&nbsp;<A href="http://www.info.ucl.ac.be/~pvr">Peter&nbsp;Van Roy</A><BR><SPAN class="version">Version 1.4.0 (20110908185330)</SPAN></ADDRESS></BODY></HTML>