Skip to content
Snippets Groups Projects
Commit 58833045 authored by Michal Patera's avatar Michal Patera
Browse files

Minor code adjustments. Mainly added and corrected used ACLS 

annotations.
parent 2294dce1
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 99 additions and 27 deletions
src/main.c
+ 99
− 27
View file @ 58833045
......@@ -10,12 +10,14 @@ typedef struct Node {
struct Node* next;
} Node;
 
/*@ requires \valid(head_ref) && \valid(new_data);
@ ensures *head_ref != \null && (*head_ref)->data == new_data;
/*@ requires \valid(head_ref);
@ ensures *head_ref != \null && (*head_ref)->data == new_data && (*head_ref)->next == \old(*head_ref) && \fresh(*head_ref, sizeof(Node));
@ allocates *head_ref;
@ assigns *head_ref;
@*/
void insertHead(Node** head_ref, int new_data) {
Node* new_node = (Node*) malloc(sizeof(Node));
Node* new_node = malloc(sizeof(Node));
//@ assert \valid(new_node);
new_node->data = new_data;
new_node->next = (*head_ref);
(*head_ref) = new_node;
......@@ -23,30 +25,45 @@ void insertHead(Node** head_ref, int new_data) {
 
/*@ requires \valid(head_ref) && *head_ref != \null;
@ assigns *head_ref;
@ ensures \free(head_ref);
@ frees *head_ref;
@ ensures *head_ref == \old((*head_ref)->next) && !\valid(\old(*head_ref));
@*/
void popHead (Node** head_ref){
void popHead(Node** head_ref) {
Node* nextHead = (*head_ref)->next;
/*@ assert \valid(*head_ref); */
free(*head_ref);
(*head_ref) = nextHead;
}
 
/*@ requires start >= 0 && end >= 0 && start < nodes && end < nodes;
@ requires graph != \null && \valid(levels + (0..nodes-1));
@ requires \forall int i; 0 <= i < nodes ==> \valid(graph[i] + (0..nodes-1));
@ assigns levels[0..nodes-1];
/*@ requires start >= 0 && end >= 0;
@ requires graph != \null && \valid(levels + (0..end));
@ requires \forall int i; 0 <= i < end + 1 ==> \valid(graph[i] + (0..end));
@ assigns levels[0..end];
@ ensures \result == 0 || \result == 1;
@*/
int BFS(int start, int end, double **graph, int *levels){
/*@ loop invariant 0 <= i <= end + 1;
@ loop invariant \forall int j; 0 <= j < i ==> levels[j] != -1;
@ loop assigns i, levels[0..end];
@ loop variant end - i;
@*/
for (int i = 0; i <= end; ++i) {
levels[i] = -1;
}
levels[start] = 0;
Node* queueHead = NULL;
insertHead(&queueHead, start);
int cur;
/*@ loop invariant \valid(queueHead) || queueHead == \null;
@ loop invariant \forall int i; 0 <= i <= end ==> levels[i] >= -1 && levels[i] <= end;
@ loop assigns cur, queueHead, levels[0..end];
@*/
while(queueHead != NULL){
int cur = queueHead->data;
cur = queueHead->data;
popHead(&queueHead);
/*@ loop invariant \forall int i; 0 <= i <= end ==> levels[i] >= -1 && levels[i] <= end;
@ loop assigns queueHead, levels[0..end];
@*/
for (int i = 0; i <= end; ++i) {
if(graph[cur][i] > 0){
if(levels[i] < 0){
......@@ -67,14 +84,19 @@ int BFS(int start, int end, double **graph, int *levels){
/*@ requires 0 <= cur <= end && end >= 0;
@ requires graph != \null && \valid(levels + (0..end)) && \valid(visited + (0..end));
@ requires \forall int i; 0 <= i <= end ==> \valid(graph[i] + (0..end));
@ assigns visited[0..end];
@ ensures \result >= 0.0;
@ assigns visited[0..end], graph[0..end][0..end];
@ ensures \result >= 0.0 && (\result > 0.0 ==> (\forall int i; 0 <= i <= end ==> (graph[cur][i] <= \old(graph[cur][i]) && graph[i][cur] >= \old(graph[i][cur]))));
@*/
double DFS (int cur, int end, double **graph, int *levels, int *visited, double flow){
if (cur == end){
return flow;
}
visited[cur] = 1;
/*@ loop invariant 0 <= i <= end + 1;
@ loop invariant 0 <= flow <= DBL_MAX;
@ loop assigns i, graph[0..end][0..end], visited[0..end];
@ loop variant end - i;
@*/
for (int i = 0; i <= end; ++i) {
if (!visited[i] && graph[cur][i] > 0 && levels[i] == levels[cur] + 1){
double augmentingFlow = DFS(i, end, graph, levels, visited, min(flow, graph[cur][i]));
......@@ -90,8 +112,10 @@ double DFS (int cur, int end, double **graph, int *levels, int *visited, double
 
/*@ requires \valid(graph);
@ ensures \result == -1 || (2 <= \result && \result <= 300000);
@ ensures *graph != \null && \forall int i; 0 <= i < *nodes ==> \valid((*graph)[i] + (0..*nodes-1));
@ assigns *nodes, *graph;
@ ensures *graph != \null && \forall int i; 0 <= i < \result ==> \valid((*graph)[i] + (0..\result-1));
@ assigns *graph;
@ allocates graph;
@ allocates graph[0..\result-1];
@*/
int readInput( double ***graph)
{
......@@ -107,16 +131,32 @@ int readInput( double ***graph)
return -1;
}
 
*graph = (double **)malloc((nodes) * sizeof(double *));
*graph = malloc((nodes) * sizeof(double *));
if (*graph == NULL){
return -1;
}
/*@ loop invariant 0 <= i <= nodes;
@ loop invariant \forall int j; 0 <= j < i ==> \valid((*graph)[j] + (0..nodes-1));
@ loop assigns i, (*graph)[0..nodes-1];
@ loop variant nodes - i;
@*/
for (int i = 0; i < (nodes); ++i)
{
(*graph)[i] = (double *)calloc((nodes), sizeof(double));
(*graph)[i] = calloc((nodes), sizeof(double));
if ((*graph)[i] == NULL){
return -1;
}
}
 
// Reading all the edges and saving them to the 2D array
int start, end;
double cap;
printf("Insert the edges of the graph.\n");
/*@ loop invariant 0 <= start < nodes;
@ loop invariant 0 <= end < nodes;
@ loop invariant 0 <= cap;
@ loop assigns start, end, cap, graph[0..nodes-1][0..nodes-1];
@*/
while (scanf("%d %d %lf", &start, &end, &cap) == 3)
{
if (start < 0 || end < 0 || cap <= 0 || start >= (nodes) || end >= (nodes))
......@@ -135,24 +175,50 @@ int readInput( double ***graph)
return nodes;
}
 
/*@ axiomatic SumCapacity {
@ logic double sum_capacity(double **graph, integer nodes, integer index) reads graph[0][0..nodes-1];
@ axiom sum_capacity_base:
@ \forall double **graph, integer nodes;
@ 0 <= nodes ==> sum_capacity(graph, nodes, 0) == 0;
@ axiom sum_capacity_step:
@ \forall double **graph, integer nodes, integer index;
@ 0 <= index < nodes - 1 ==>
@ sum_capacity(graph, nodes, index + 1) == sum_capacity(graph, nodes, index) + graph[0][index];
@ }
@*/
/*@ predicate valid_flow(double result, double **graph, integer nodes) =
@ result >= -1 && result <= sum_capacity(graph, nodes, nodes - 1);
@*/
/*@ requires nodes > 0;
@ requires graph != \null && \forall int i; 0 <= i < nodes ==> \valid(graph[i] + (0..nodes-1));
@ ensures \result >= -1;
@ ensures valid_flow(\result, graph, nodes);
@ assigns graph[0..nodes-1][0..nodes-1];
@*/
double dinicMaxFlow(int nodes, double **graph){
int total = 0;
int *vertexLevel = (int *)malloc(nodes * sizeof(int));
double total = 0;
int *vertexLevel = malloc(nodes * sizeof(int));
int *visited;
 
// Run BFS to check if flow is possible and set the levels of nodes
/*@ loop invariant 0 <= total && total <= sum_capacity(graph, nodes, nodes - 1);
@ loop assigns total, vertexLevel[0..nodes-1], *visited, graph[0..nodes-1][0..nodes-1];
@ loop variant nodes - 1 - vertexLevel[nodes-1];
@*/
while (BFS(0, nodes - 1, graph, vertexLevel))
{
 
// Initialize visited array
int *visited = (int *)calloc(nodes, sizeof(int));
visited = calloc(nodes, sizeof(int));
double flow;
/*@ loop invariant 0 <= total;
@ loop assigns flow, total, visited[0..nodes-1], graph[0..nodes-1][0..nodes-1];
@ loop variant (int)(DBL_MAX - total) * 1000;
@*/
while (1)
{
double flow = DFS(0, nodes - 1, graph, vertexLevel, visited, DBL_MAX);
flow = DFS(0, nodes - 1, graph, vertexLevel, visited, DBL_MAX);
if (flow == 0.0)
{
break;
......@@ -178,8 +244,10 @@ double dinicMaxFlow(int nodes, double **graph){
@ requires nodes > 0;
@ requires \valid(graph + (0 .. nodes-1));
@ requires \forall int i; 0 <= i < nodes ==> \valid(graph[i] + (0..nodes-1));
@ ensures \forall int i; 0 <= i < nodes ==> \free(graph[i] + (0..nodes-1));
@ ensures \free(graph);
@ ensures !\valid(graph) && (\forall int i; 0 <= i < nodes ==> !\valid(graph[i]));
@ frees graph[0..nodes-1];
@ frees graph;
@ assigns \nothing;
@*/
void cleanUp(int nodes, double** graph){
for (int i = 0; i < nodes; i++)
......@@ -187,16 +255,20 @@ void cleanUp(int nodes, double** graph){
free(graph);
}
 
/*@ ensures \result == 0 || \result == 1;
@ assigns \nothing;
@*/
int main()
{
int nodes;
double **graph;
double total = -1;
nodes = readInput(&graph);
if(nodes == -1){
return 1;
}
double total = dinicMaxFlow(nodes, graph);
if (total == -1)
total = dinicMaxFlow(nodes, graph);
if (total == -1.0)
{
cleanUp(nodes, graph);
return 1;
......@@ -207,4 +279,4 @@ int main()
cleanUp(nodes, graph);
}
return 0;
}
}
\ No newline at end of file
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