this repo has no description
dekker.one
1%--------------------------------------------------------------------%
2% 需要给出一个任务集合，其中起始时间为's',
3% 持续时间'd'以及资源需求量'r'，
4% 任何时候需求量都不能超过
5% 一个全局资源界限'b'。
6% 假设：
7% - forall i, d[i] >= 0 and r[i] >= 0
8%--------------------------------------------------------------------%
9predicate cumulative(array[int] of var int: s,
10 array[int] of var int: d,
11 array[int] of var int: r, var int: b) =
12 assert(index_set(s) == index_set(d) /\
13 index_set(s) == index_set(r),
14 "cumulative: the array arguments must have identical index sets",
15 assert(lb_array(d) >= 0 /\ lb_array(r) >= 0,
16 "cumulative: durations and resource usages must be non-negative",
17 let {
18 set of int: times =
19 lb_array(s) ..
20 max([ ub(s[i]) + ub(d[i]) | i in index_set(s) ])
21 }
22 in
23 forall( t in times ) (
24 b >= sum( i in index_set(s) ) (
25 bool2int( s[i] <= t /\ t < s[i] + d[i] ) * r[i]
26 )
27 )
28 )
29 );