this repo has no description
dekker.one
1%--------------------------------------------------------------------%
2% Requiere que un conjunto de tareas dadas por los tiempos de inicio 's',
3% duraciones 'd' y requerimientos de recursos 'r',
4% nunca requieren más de un recurso global vinculado 'b' en cualquier momento.
5% Suposiciones:
6% - forall i, d[i] >= 0 and r[i] >= 0
7%--------------------------------------------------------------------%
8predicate cumulative(array[int] of var int: s,
9 array[int] of var int: d,
10 array[int] of var int: r, var int: b) =
11 assert(index_set(s) == index_set(d) /\
12 index_set(s) == index_set(r),
13 "cumulativo: los argumentos del array deben tener conjuntos de índices idénticos",
14 assert(lb_array(d) >= 0 /\ lb_array(r) >= 0,
15 "acumulativo: las duraciones y usos de los recursos deben ser no negativos",
16 let {
17 set of int: times =
18 lb_array(s) ..
19 max([ ub(s[i]) + ub(d[i]) | i in index_set(s) ])
20 }
21 in
22 forall( t in times ) (
23 b >= sum( i in index_set(s) ) (
24 bool2int( s[i] <= t /\ t < s[i] + d[i] ) * r[i]
25 )
26 )
27 )
28 );