You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: doc/src/resources.md
+70-39Lines changed: 70 additions & 39 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -16,6 +16,7 @@ The right-hand side of the operator could be either a constant or a variable.
16
16
### 1.2 Effects
17
17
18
18
The value of a resource can be :
19
+
19
20
- changed with an **assignment**, the new value could be either a constant or a variable
20
21
-**increased** by a constant value
21
22
-**decreased** by a constant value, internally it is an increased operation with a negative constant value
@@ -24,55 +25,85 @@ The value of a resource can be :
24
25
25
26
### 2.1. Effects
26
27
27
-
Every time a resource value is updated, new conditions are created in order to check that the value can be updated and that the new value is contained in the bounded domain of the resource.
28
+
Every time a resource value is updated, new constraints or conditions are created in order to check that the value can be updated and that the new value is contained in the bounded domain of the resource.
29
+
30
+
#### 2.1.1 Assign effects
31
+
32
+
For an assign effect $[t^a] R^a := z$, we will create the following constraints:
28
33
29
-
For an **assign effect** $[t^a] R^a := z$, we will create the following conditions:
30
-
$$\begin{cases}
34
+
$$
35
+
\begin{cases}
31
36
[t^a] z \ge l \\
32
37
[t^a] z \le u \\
33
-
\end{cases}$$
38
+
\end{cases}
39
+
$$
34
40
35
-
For an **increase effect** $[t^i] R^i \mathrel{+}= c$, we will create the following conditions:
36
-
$$\begin{cases}
37
-
[t^i] R^i \le u - c \\
38
-
[t^i] R^i \ge l - c \\
39
-
[t^i+\varepsilon] R^i \le u \\
40
-
[t^i+\varepsilon] R^i \ge l \\
41
-
\end{cases}$$
41
+
#### 2.1.2 Increase effects
42
42
43
-
For a **decrease effect** $[t^d] R^d \mathrel{-}= c$, we convert it into the increase effect $[t^d] R^d \mathrel{+}= (-c)$ and then create the associated conditions.
43
+
For an increase effect $[t^i] R^i \mathrel{+}= c$, we will create a new variable $v$ with the same domain as the resource and add a new condition $[t^i]R^i = v$.
44
44
45
-
Next, these conditions are converted into linear constraints as explained in the next section.
45
+
This will ensure that the new value of the resource is in the correct domain after the increase.
46
+
Next, this condition is converted into linear constraints as explained in the next section.
47
+
48
+
#### 2.1.3 Decrease effects
49
+
50
+
For a decrease effect $[t^d] R^d \mathrel{-}= c$, we convert it into the increase effect $[t^d] R^d \mathrel{+}= (-c)$ and then create the associated conditions.
46
51
47
52
### 2.2. Conditions
48
53
49
54
Every time a resource must be tested, a set of associated linear constraints are created.
50
55
51
-
For an **equality condition** $[t^c] R^c = z$, we will have the **linear constraints**
Where $l^a_jc^a_j$ represents an assignment to the resource and $l^i_{jk}c^i_k$ represents an increase, the $l$ variables are booleans used to know if the associated $c$ variable (which is the value of the assignment or the increase) should be used. The idea is to consider only the constraint corresponding to the latest assignment.
59
-
60
-
To do so, we define $\textit{SP}$ which test if the parameters of two resources are the same, $\textit{SPP}$ which test the presence and the parameters, $\textit{LA}$ which test if the assignment is the last one for the current condition:
Where $l^a_jc^a_j$ represents an assignment to the resource and $l^i_{jm}c^i_m$ represents an increase, the $l$ variables are boolean literals used to know if the associated $c$ variable (which is the value of the effect) should be used.
69
+
The idea is to consider only the constraint corresponding to the latest assignment.
70
+
71
+
To do so, we define $\textit{SP}$ which test if the parameters of two resources are the same by:
We also define $\textit{LA}$ which test if the assignment effect is the last one before the condition.
76
+
**There are two ways to define it**.
77
+
The **first** one is to check that the effect is before the condition and for other compatible assignment effects, check that they are not between the considering effect and the condition:
Moreover, we enforce to have at least one last assignment effect with the disjunction $\bigvee_{j}l^a_j$.
94
+
95
+
The $l^i_{jm}$ literal is true if the increase $m$ is present with the same resource as the condition, if the assignment $j$ is the last one and if the increase $m$ is between the assignment $j$ and the condition:
0 commit comments