Commit 5520bb48 authored by Vladislav Kiselev's avatar Vladislav Kiselev

Упрощение. Теперь все bool значения сравниваются только с соответствующими константами.

parent 49424e24
...@@ -18,9 +18,9 @@ array [1..n_moving_obj, 1..n_locations] of set of 1..n_operations : departure_op ...@@ -18,9 +18,9 @@ array [1..n_moving_obj, 1..n_locations] of set of 1..n_operations : departure_op
% Определение m_obj_loc. % Определение m_obj_loc.
constraint forall (obj in 1..n_moving_obj, j in 1..(n_intervals + 1)) constraint forall (obj in 1..n_moving_obj, j in 1..(n_intervals + 1))
((m_obj_loc[obj, j] != 0) -> ( ((m_obj_loc[obj, j] != 0) -> (
(m_obj_loc[obj, j] == m_obj_loc[obj, j - 1] /\ (forall (k in departure_op[obj, m_obj_loc[obj, j]]) (op_status[k, j - 1] == 0))) (m_obj_loc[obj, j] == m_obj_loc[obj, j - 1] /\ (forall (k in departure_op[obj, m_obj_loc[obj, j]]) (not op_status[k, j - 1])))
\/ \/
(exists (k in arrival_op[obj, m_obj_loc[obj, j]]) (op_fin[k, j - 1] != 0)) (exists (k in arrival_op[obj, m_obj_loc[obj, j]]) (op_fin[k, j - 1]))
)); ));
% Начальное состояние. % Начальное состояние.
...@@ -38,7 +38,7 @@ constraint forall (i in 1..n_operations, j in {0, n_intervals + 1}) (op_status[i ...@@ -38,7 +38,7 @@ constraint forall (i in 1..n_operations, j in {0, n_intervals + 1}) (op_status[i
% Определение op_start и op_fin. % Определение op_start и op_fin.
constraint forall (op in 1..n_operations, j in {0, n_intervals + 1}) constraint forall (op in 1..n_operations, j in {0, n_intervals + 1})
(op_start[op, j] == 0 /\ op_fin[op, j] == 0); (op_start[op, j] = false /\ op_fin[op, j] = false);
constraint forall (i in 1..n_operations, j in 1..(n_intervals + 1)) (op_start[i, j] = (op_status[i, j] /\ not op_status[i, j - 1])); constraint forall (i in 1..n_operations, j in 1..(n_intervals + 1)) (op_start[i, j] = (op_status[i, j] /\ not op_status[i, j - 1]));
constraint forall (i in 1..n_operations, j in 1..n_intervals ) (op_fin [i, j] = (op_status[i, j] /\ not op_status[i, j + 1])); constraint forall (i in 1..n_operations, j in 1..n_intervals ) (op_fin [i, j] = (op_status[i, j] /\ not op_status[i, j + 1]));
...@@ -50,15 +50,12 @@ constraint forall (i in 1..n_operations where is_continuous_operation[i]) ( ...@@ -50,15 +50,12 @@ constraint forall (i in 1..n_operations where is_continuous_operation[i]) (
let {var int : len = operations_duration[i]} in let {var int : len = operations_duration[i]} in
(forall (j in 1..(n_intervals - len + 1)) ( (forall (j in 1..(n_intervals - len + 1)) (
(op_start[i, j] == 1) -> ( (op_start[i, j] == 1) -> (
(forall (k in 1..(len - 1)) (forall (k in 1..(len - 1)) (op_status[i, j + k]))
(op_status[i, j + k] == 1) /\
) /\ (not op_status[i, j + len])
(op_status[i, j + len] == 0)
) )
)) /\ )) /\
(forall (j in (n_intervals - len + 2)..(n_intervals + 1)) (forall (j in (n_intervals - len + 2)..(n_intervals + 1)) (op_start[i, j] == false))
(op_start[i, j] == 0)
)
); );
% Наличие всех ресурсов на месте во время начала операции перемещения. % Наличие всех ресурсов на месте во время начала операции перемещения.
...@@ -78,7 +75,7 @@ array [1..n_conflicting_op] of 1..n_operations : confl_op_1; ...@@ -78,7 +75,7 @@ array [1..n_conflicting_op] of 1..n_operations : confl_op_1;
array [1..n_conflicting_op] of 1..n_operations : confl_op_2; array [1..n_conflicting_op] of 1..n_operations : confl_op_2;
constraint forall (t in 0..(n_intervals + 1), i in 1..n_conflicting_op) ( constraint forall (t in 0..(n_intervals + 1), i in 1..n_conflicting_op) (
(op_status[confl_op_1[i], t] -> not op_status[confl_op_2[i], t]) op_status[confl_op_1[i], t] -> not op_status[confl_op_2[i], t]
); );
% Окна непогоды. % Окна непогоды.
...@@ -88,7 +85,7 @@ array [1..n_bad_weather_windows] of 0..(n_intervals + 1) : bw_start; ...@@ -88,7 +85,7 @@ array [1..n_bad_weather_windows] of 0..(n_intervals + 1) : bw_start;
array [1..n_bad_weather_windows] of 0..(n_intervals + 1) : bw_fin; % Включительно. array [1..n_bad_weather_windows] of 0..(n_intervals + 1) : bw_fin; % Включительно.
constraint forall (i in 1..n_bad_weather_windows, t in bw_start[i]..bw_fin[i]) ( constraint forall (i in 1..n_bad_weather_windows, t in bw_start[i]..bw_fin[i]) (
op_status[bw_op[i], t] == 0 op_status[bw_op[i], t] == false
); );
% Грузообработка. % Грузообработка.
...@@ -140,11 +137,11 @@ constraint forall (storage in 1..n_obj_with_storage, cargo in 1..n_cargo_types, ...@@ -140,11 +137,11 @@ constraint forall (storage in 1..n_obj_with_storage, cargo in 1..n_cargo_types,
% Критерий оптимизации % Критерий оптимизации
array [0..(n_intervals + 1)] of var bool : is_not_terminated; array [0..(n_intervals + 1)] of var bool : is_not_terminated;
constraint (is_not_terminated[0] == 0 /\ is_not_terminated[n_intervals + 1] == 0); constraint (is_not_terminated[0] == false /\ is_not_terminated[n_intervals + 1] == false);
constraint forall (t in 1..n_intervals) ( constraint forall (t in 1..n_intervals) (
is_not_terminated[t] == ( is_not_terminated[t] == (
(exists (op in 1..n_operations) (op_status[op, t] == 1)) (exists (op in 1..n_operations) (op_status[op, t]))
\/ \/
is_not_terminated[t + 1] is_not_terminated[t + 1]
) )
...@@ -187,15 +184,13 @@ array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_m_obj_useful; % ...@@ -187,15 +184,13 @@ array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_m_obj_useful; %
op_status[useful_op_id[i], t] -> is_m_obj_useful[useful_op_obj[i], t] op_status[useful_op_id[i], t] -> is_m_obj_useful[useful_op_obj[i], t]
); );
constraint forall (obj in 1..n_moving_obj, t in 0..(n_intervals + 1)) ( % Недопущение "ложного срабатывания" is_m_obj_useful. constraint forall (obj in 1..n_moving_obj, t in 0..(n_intervals + 1)) ( % Недопущение "ложного срабатывания" is_m_obj_useful.
is_m_obj_useful[obj, t] -> exists (useful_op in obj_useful_operations[obj]) ( is_m_obj_useful[obj, t] -> exists (useful_op in obj_useful_operations[obj]) (op_status[useful_op, t])
op_status[useful_op, t] == true
)
); );
array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_obj_in_moving; array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_obj_in_moving;
array [1..n_moving_obj] of set of 1..n_operations : moving_op_of_obj; % Операции перемещения затрагивающие данный объект. array [1..n_moving_obj] of set of 1..n_operations : moving_op_of_obj; % Операции перемещения затрагивающие данный объект.
constraint forall (obj in 1..n_moving_obj, t in 0..(n_intervals + 1)) ( constraint forall (obj in 1..n_moving_obj, t in 0..(n_intervals + 1)) (
is_obj_in_moving[obj, t] = exists (moving_op in moving_op_of_obj[obj]) (op_status[moving_op, t] = true) is_obj_in_moving[obj, t] = exists (moving_op in moving_op_of_obj[obj]) (op_status[moving_op, t])
); );
array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_interval_useful; % Была ли на текущем интервале полезная операция. array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_interval_useful; % Была ли на текущем интервале полезная операция.
......
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