Commit 963aead7 authored by Vladislav Kiselev's avatar Vladislav Kiselev

Новое сведение.

parent d9fddf86
...@@ -52,8 +52,8 @@ constraint forall (i in 1..n_operations, j in 1..(n_intervals + 1)) (op_start[i, ...@@ -52,8 +52,8 @@ constraint forall (i in 1..n_operations, j in 1..(n_intervals + 1)) (op_start[i,
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]));
% Непрерывность перемещения и швартовки. % Непрерывность перемещения и швартовки.
array [1..n_operations] of var int : operations_duration; array [1..n_operations] of int : operations_duration;
array [1..n_operations] of var bool : is_continuous_operation; array [1..n_operations] of bool : is_continuous_operation;
constraint forall (i in 1..n_operations where is_continuous_operation[i]) ( 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
......
...@@ -9,28 +9,60 @@ array [1..n_operations, 0..(n_intervals + 1)] of var bool : op_status; ...@@ -9,28 +9,60 @@ array [1..n_operations, 0..(n_intervals + 1)] of var bool : op_status;
array [1..n_operations, 0..(n_intervals + 1)] of var bool : op_start; array [1..n_operations, 0..(n_intervals + 1)] of var bool : op_start;
array [1..n_operations, 0..(n_intervals + 1)] of var bool : op_fin; array [1..n_operations, 0..(n_intervals + 1)] of var bool : op_fin;
% 0 - локация не определена. int : moving_op_of_obj_max_size;
array [1..n_moving_obj, 0..(n_intervals + 1)] of var 0..n_locations : m_obj_loc; % Moving object location. array [1..n_moving_obj] of 0..moving_op_of_obj_max_size : moving_op_of_obj_sizes;
array [1..n_moving_obj, 1..moving_op_of_obj_max_size] of 1..n_operations : moving_op_of_obj; % Операции перемещения затрагивающие данный объект.
int : arrival_op_max_size;
array [1..n_moving_obj, 1..n_locations, 1..arrival_op_max_size] of 1..n_operations : arrival_op; array [1..n_moving_obj, 0..(n_intervals + 1)] of var 0..moving_op_of_obj_max_size : current_moving_operation; % Текущая операция операция перемещения, в которой задействован данный объект.
array [1..n_moving_obj, 1..n_locations] of 0..arrival_op_max_size : arrival_op_sizes; % Текущая операция лежит в множестве тех, которые затрагивают данный объект.
constraint forall (obj in 1..n_moving_obj, t in 0..(n_intervals + 1)) (
int : departure_op_max_size; current_moving_operation[obj, t] <= moving_op_of_obj_sizes[obj]
array [1..n_moving_obj, 1..n_locations, 1..departure_op_max_size] of 1..n_operations : departure_op; );
array [1..n_moving_obj, 1..n_locations] of 0..departure_op_max_size : departure_op_sizes;
% Если операция, затрагивающая данный объект, выполняется - то именно она текущая операция перемещения для этого объекта.
% Определение m_obj_loc. constraint forall (obj in 1..n_moving_obj, op_no in 1..moving_op_of_obj_sizes[obj], t in 0..(n_intervals + 1)) (
constraint forall (obj in 1..n_moving_obj, j in 1..(n_intervals + 1)) (op_status[moving_op_of_obj[obj, op_no], t]) -> (current_moving_operation[obj, t] = op_no)
((m_obj_loc[obj, j] != 0) -> ( );
(m_obj_loc[obj, j] == m_obj_loc[obj, j - 1] /\
(forall (k in 1..departure_op_sizes[obj, m_obj_loc[obj, j]]) % Если объект движется, то выполняется какая-то операция перемещения, касаящаяся этого объекта.
(not op_status[departure_op[obj, m_obj_loc[obj, j], k], j - 1])) constraint forall (obj in 1..n_moving_obj, t in 0..(n_intervals + 1)) (
) (current_moving_operation[obj, t] > 0) ->
\/ (exists (op_no in 1..moving_op_of_obj_sizes[obj]) (op_status[moving_op_of_obj[obj, op_no], t]))
(exists (k in 1..arrival_op_sizes[obj, m_obj_loc[obj, j]]) );
(op_fin[arrival_op[obj, m_obj_loc[obj, j], k], j - 1]))
)); array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_m_obj_in_movement_before_start; % Находится ли объект в движении перед началом интервала.
% В начале никто не движется.
constraint forall (obj in 1..n_moving_obj) (not is_m_obj_in_movement_before_start[obj, 0]);
% Перед первым интервалом все тоже стоят на месте.
constraint forall (obj in 1..n_moving_obj) (not is_m_obj_in_movement_before_start[obj, 1]);
% Если в предыдущем интервале объект не движется - то в начале этого он не движется, иначе он движется если предыдущая операция не закончилась.
constraint forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) (
if (current_moving_operation[obj, t - 1] = 0) then
is_m_obj_in_movement_before_start[obj, t] = false
else
is_m_obj_in_movement_before_start[obj, t] = (current_moving_operation[obj, t - 1] != current_moving_operation[obj, t])
endif
);
array [1..n_operations] of 1..n_locations : operations_destination; % Локация в которой окажется объект после завершения операции.
% Теперь m_obj_loc означает где объект стоит или куда он движется перед началом определённого интервала.
array [1..n_moving_obj, 0..(n_intervals + 1)] of var 1..n_locations : m_obj_loc; % Moving object location.
% За фиктивный нулевой интервал объект не успевает ничего сделать с начальным положением.
constraint forall (obj in 1..n_moving_obj) (
m_obj_loc[obj, 1] = m_obj_loc[obj, 0]
);
% Направление движения/местоположение объекта может измениться только если перед этим началась операция перемещения.
constraint forall (obj in 1..n_moving_obj, t in 2..(n_intervals + 1)) (
if ((current_moving_operation[obj, t - 1] != current_moving_operation[obj, t - 2]) /\
(current_moving_operation[obj, t - 1] != 0)) then
m_obj_loc[obj, t] = operations_destination[moving_op_of_obj[obj, current_moving_operation[obj, t - 1]]]
else
m_obj_loc[obj, t] = m_obj_loc[obj, t - 1]
endif
);
% Начальное состояние. % Начальное состояние.
array [1..n_moving_obj] of var 0..n_locations : initial_m_obj_loc; array [1..n_moving_obj] of var 0..n_locations : initial_m_obj_loc;
...@@ -52,8 +84,8 @@ constraint forall (i in 1..n_operations, j in 1..(n_intervals + 1)) (op_start[i, ...@@ -52,8 +84,8 @@ constraint forall (i in 1..n_operations, j in 1..(n_intervals + 1)) (op_start[i,
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]));
% Непрерывность перемещения и швартовки. % Непрерывность перемещения и швартовки.
array [1..n_operations] of var int : operations_duration; array [1..n_operations] of int : operations_duration;
array [1..n_operations] of var bool : is_continuous_operation; array [1..n_operations] of bool : is_continuous_operation;
constraint forall (i in 1..n_operations where is_continuous_operation[i]) ( 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
...@@ -75,9 +107,10 @@ array [1..n_operations, 1..operations_resources_max_size] of 1..n_moving_obj : o ...@@ -75,9 +107,10 @@ array [1..n_operations, 1..operations_resources_max_size] of 1..n_moving_obj : o
array [1..n_operations] of 0..n_locations : operations_start_loc; array [1..n_operations] of 0..n_locations : operations_start_loc;
constraint forall (op in 1..n_operations, j in 1..n_intervals) ( constraint forall (op in 1..n_operations, t in 1..n_intervals) (
forall (op_res_id in 1..operations_resources_sizes[op]) ( forall (op_res_id in 1..operations_resources_sizes[op]) (
(op_start[op, j]) -> (m_obj_loc[operations_resources[op, op_res_id], j] == operations_start_loc[op]) (op_start[op, t]) -> ((m_obj_loc[operations_resources[op, op_res_id], t] == operations_start_loc[op]) /\
(not is_m_obj_in_movement_before_start[operations_resources[op, op_res_id], t]))
) )
); );
...@@ -215,13 +248,9 @@ array [1..n_moving_obj, 1..obj_useful_operations_max_size] of 1..n_operations : ...@@ -215,13 +248,9 @@ array [1..n_moving_obj, 1..obj_useful_operations_max_size] of 1..n_operations :
(op_status[obj_useful_operations[obj, useful_op_no], t]) (op_status[obj_useful_operations[obj, useful_op_no], t])
); );
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_m_obj_in_movement; % Находится ли объект в движении в течении интервала.
int : moving_op_of_obj_max_size;
array [1..n_moving_obj] of 0..moving_op_of_obj_max_size : moving_op_of_obj_sizes;
array [1..n_moving_obj, 1..moving_op_of_obj_max_size] 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_no in 1..moving_op_of_obj_sizes[obj]) (op_status[moving_op_of_obj[obj, moving_op_no], t]) is_m_obj_in_movement[obj, t] = exists (moving_op_no in 1..moving_op_of_obj_sizes[obj]) (op_status[moving_op_of_obj[obj, moving_op_no], 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; % Была ли на текущем интервале полезная операция.
...@@ -233,7 +262,7 @@ array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_interval_useful; ...@@ -233,7 +262,7 @@ array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_interval_useful;
constraint forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) ( constraint forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) (
is_interval_useful[obj, t] = is_interval_useful[obj, t] =
if (is_obj_in_moving[obj, t]) then if (is_m_obj_in_movement[obj, t]) then
is_m_obj_useful[obj, t] is_m_obj_useful[obj, t]
else else
is_m_obj_useful[obj, t] \/ is_interval_useful[obj, t - 1] is_m_obj_useful[obj, t] \/ is_interval_useful[obj, t - 1]
...@@ -241,8 +270,7 @@ array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_interval_useful; ...@@ -241,8 +270,7 @@ array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_interval_useful;
); );
constraint forall (obj in 1..n_moving_obj, t in 1..n_intervals) ( % Само ограничение. constraint forall (obj in 1..n_moving_obj, t in 1..n_intervals) ( % Само ограничение.
(( m_obj_loc[obj, t] != 0) /\ ((prev_m_obj_loc[obj, t] != 0) /\
(prev_m_obj_loc[obj, t] != 0) /\
(next_m_obj_loc[obj, t + 1] != m_obj_loc[obj, t]) /\ (next_m_obj_loc[obj, t + 1] != m_obj_loc[obj, t]) /\
(next_m_obj_loc[obj, t + 1] == prev_m_obj_loc[obj, t]) (next_m_obj_loc[obj, t + 1] == prev_m_obj_loc[obj, t])
) -> is_interval_useful[obj, t - 1] ) -> is_interval_useful[obj, t - 1]
...@@ -255,11 +283,9 @@ output [show(sum(is_not_terminated)), "\n", ...@@ -255,11 +283,9 @@ output [show(sum(is_not_terminated)), "\n",
"m_obj_loc = ", show(m_obj_loc), "\n\n", "m_obj_loc = ", show(m_obj_loc), "\n\n",
"op_fin = ", show(op_fin), "\n\n", "op_fin = ", show(op_fin), "\n\n",
"op_start = ", show(op_start), "\n\n", "op_start = ", show(op_start), "\n\n",
"arrival_op = ", show(arrival_op), "\n\n",
"departure_op = ", show(departure_op), "\n\n",
"is_not_terminated = ", show(is_not_terminated), "\n\n", "is_not_terminated = ", show(is_not_terminated), "\n\n",
"storage_used_volume = ", show(storage_used_volume), "\n\n", "storage_used_volume = ", show(storage_used_volume), "\n\n",
"prev_m_obj_loc = ", show(prev_m_obj_loc), "\n\n", % "prev_m_obj_loc = ", show(prev_m_obj_loc), "\n\n",
"next_m_obj_loc = ", show(next_m_obj_loc), "\n\n", % "next_m_obj_loc = ", show(next_m_obj_loc), "\n\n",
"is_interval_useful = ", show(is_interval_useful), "\n\n" % "is_interval_useful = ", show(is_interval_useful), "\n\n"
]; ];
...@@ -636,7 +636,7 @@ public class ConversionUtil { ...@@ -636,7 +636,7 @@ public class ConversionUtil {
} }
/* Ограничение на необходимость полезной операции между движениями к одному пункту назначения. */ /* Ограничение на необходимость полезной операции между движениями к одному пункту назначения. */
private void constraintOnUsefulOperationBetweenMovements() throws IOException { private void constraintOnUsefulOperationBetweenMovements_0() throws IOException {
ArrayList<Set<Integer>> objUsefulOperations = new ArrayList<>(); ArrayList<Set<Integer>> objUsefulOperations = new ArrayList<>();
ArrayList<Set<Integer>> movingOpOfObj = new ArrayList<>(); ArrayList<Set<Integer>> movingOpOfObj = new ArrayList<>();
...@@ -684,6 +684,76 @@ public class ConversionUtil { ...@@ -684,6 +684,76 @@ public class ConversionUtil {
writer.write("\n"); writer.write("\n");
} }
private void constraintOnUsefulOperationBetweenMovements_1() throws IOException {
ArrayList<Set<Integer>> objUsefulOperations = new ArrayList<>();
BiConsumer<MovingObject, Integer> addUsOp = (MovingObject obj, Integer op) ->
objUsefulOperations.get(mObjToN.apply(obj)).add(op + 1);
for (int i = 0; i < movingObjects.size(); i++) {
objUsefulOperations.add(new TreeSet<>());
}
for (int i = 0; i < operationTemplates.size(); i++) {
OperationTemplate t = operationTemplates.get(i);
if (t instanceof MovingTemplate) {
MovingTemplate op = (MovingTemplate)t;
for (MovingObject obj : op.getResources()) {
addUsOp.accept(obj, i);
}
} else if (t instanceof MooringTemplate) {
MooringTemplate op = (MooringTemplate)t;
for (MovingObject obj : op.getResources()) {
addUsOp.accept(obj, i);
}
if (!op.isDirect()) { // Отшвартовка.
addUsOp.accept(op.getMoorer(), i);
}
} else if (t instanceof LoadingTemplate) {
LoadingTemplate op = (LoadingTemplate)t;
addUsOp.accept(op.getLoader(), i);
}
}
writeArrayOfSetAs2DArray(writer, "obj_useful_operations", objUsefulOperations);
writer.write("\n");
}
private void movingObjectLocationDefinition() throws IOException {
ArrayList<Set<Integer>> movingOpOfObj = new ArrayList<>();
ArrayList<Integer> operationsDestination = new ArrayList<>();
for (int i = 0; i < movingObjects.size(); i++) {
movingOpOfObj.add(new TreeSet<>());
}
for (int i = 0; i < operationTemplates.size(); i++) {
OperationTemplate t = operationTemplates.get(i);
if ((t instanceof MovingTemplate) || (t instanceof MooringTemplate)) {
int id = mObjToN.apply(getExecutor(t));
movingOpOfObj.get(id).add(i + 1);
}
if (t instanceof MovingTemplate) {
MovingTemplate op = (MovingTemplate)t;
operationsDestination.add(getLocNById.apply(op.getDestination().getId(), false));
} else if (t instanceof MooringTemplate) {
MooringTemplate op = (MooringTemplate)t;
operationsDestination.add(getLocNById.apply(op.getStartLocation().getId(), op.isDirect()));
} else {
// TODO аккуратно обработать погрузку.
operationsDestination.add(getLocNById.apply(t.getStartLocation().getId(), false));
}
}
writeArrayOfSetAs2DArray(writer, "moving_op_of_obj", movingOpOfObj);
writeArray(writer, "operations_destination", operationsDestination, (Integer val) -> val + 1);
writer.write("\n");
}
void portToMiniZinc_0() throws IOException { void portToMiniZinc_0() throws IOException {
try { try {
writer = new FileWriter(fileName, false); writer = new FileWriter(fileName, false);
...@@ -711,7 +781,42 @@ public class ConversionUtil { ...@@ -711,7 +781,42 @@ public class ConversionUtil {
cargoFlows(); cargoFlows();
cargoOperations(); cargoOperations();
constraintOnUsefulOperationBetweenMovements(); constraintOnUsefulOperationBetweenMovements_0();
} finally {
if (writer != null) {
writer.close();
}
}
}
void portToMiniZinc_1() throws IOException {
try {
writer = new FileWriter(fileName, false);
writer.write("n_intervals = " + n_intervals + ";\n");
writer.write("n_operations = " + task.getTemplates().size() + ";\n");
writer.write("n_locations = " + locationNumberById.size() + ";\n");
writer.write("n_moving_obj = " + movingObjects.size() + ";\n");
writer.write("\n");
movingObjectLocationDefinition();
initialLocations();
weatherWindows();
operationsContinuity();
finalLocations();
presenceOfResourcesInLocation();
conflictingOperations();
writer.write("n_obj_with_storage = " + nObjWithStorage + ";\n");
writer.write("n_cargo_types = " + cargoes.size() + ";\n");
maxStorageVolume();
boundaryStorageStates();
cargoFlows();
cargoOperations();
constraintOnUsefulOperationBetweenMovements_1();
} finally { } finally {
if (writer != null) { if (writer != null) {
writer.close(); writer.close();
...@@ -725,6 +830,11 @@ public class ConversionUtil { ...@@ -725,6 +830,11 @@ public class ConversionUtil {
taskData.portToMiniZinc_0(); taskData.portToMiniZinc_0();
} }
static public void portToMiniZinc_1(TaskCase task, String fileName) throws IOException {
Task taskData = new Task(task, fileName);
taskData.portToMiniZinc_1();
}
static public void resolveMiniZincResults(TaskCase task, String fileName) throws IOException, ParserException { static public void resolveMiniZincResults(TaskCase task, String fileName) throws IOException, ParserException {
List<Operation> operations = null; List<Operation> operations = null;
Integer result = null; Integer result = null;
......
...@@ -23,6 +23,18 @@ public class Main { ...@@ -23,6 +23,18 @@ public class Main {
} }
break; break;
} }
case "to_MiniZinc_1" : {
String input = args[1];
String output = args[2];
TaskCase task = new TaskCase();
try {
task.deserialize(input);
ConversionUtil.portToMiniZinc_1(task, output);
} catch (IOException ex) {
System.out.println(ex.getMessage());
}
break;
}
case "resolve_result" : { case "resolve_result" : {
String input = args[1]; String input = args[1];
String fileWIthResult = args[2]; String fileWIthResult = args[2];
......
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