forked from giannkas/ecofolder
-
Notifications
You must be signed in to change notification settings - Fork 0
/
marking.c
211 lines (183 loc) · 5.49 KB
/
marking.c
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
#include <stdio.h>
#include <string.h>
#include "common.h"
#include "netconv.h"
#include "unfold.h"
hashcell_t **hash;
querycell_t **query;
int hash_buckets;
int *rep_marking;
/******************************************************/
void marking_init ()
{
hash_buckets = net->numpl*4 + 1;
hash = MYcalloc(hash_buckets * sizeof(hashcell_t*));
query = MYcalloc(1 * sizeof(querycell_t*));
}
/******************************************************/
/*
Compute the hash value of a marking. TODO: Is this a
good hash function?? If not, replace by something better.
Also, this might be the only place that really needs
pl->num.
*/
int marking_hash (nodelist_t *marking)
{
unsigned int val = 0, i = 0;
while (marking)
{
val += ((place_t*)(marking->node))->num * ++i;
marking = marking->next;
}
return val % hash_buckets;
}
/******************************************************/
/*
Check if a marking is already present in the hash table.
Return number of times the marking is repeated, negative
values are returned when the marking is present but its
corresponding instance does not match with the requested
one by the user when searching. If the marking is not
present at all, it returns 0. The given marking is left
unchanged.
*/
int find_marking (nodelist_t *marking, int m_query)
{
hashcell_t **buck = hash + marking_hash(marking);
int cmp = 2;
nodelist_t* list = NULL;
int tmp_repeat = 0;
while (*buck && (cmp = nodelist_compare(marking,(*buck)->marking)) > 0)
buck = &((*buck)->next);
if (m_query && !cmp){
for(list = marking; list && !cmp; list = list->next)
if(!((place_t*)(list->node))->queried) cmp = 1;
if(!cmp && (*buck)->repeat != m_repeat)
tmp_repeat = (*buck)->repeat*-1;
else if(!cmp && (*buck)->repeat == m_repeat)
tmp_repeat = (*buck)->repeat;
}
return !cmp && m_query ? tmp_repeat : !cmp;
}
/******************************************************/
/*
Inspecting the cone of an event to see if its
corresponding marking was seen before
*/
int check_back(cond_t **conds, int size, event_t *ev)
{
int i, found = 0;
for(i = 0; i < size && !found; i++)
{
//printf("i: %d, co name: %s and num: %d\n", i, conds[i]->origin->name, conds[i]->num + 1);
if(conds[i]->pre_ev && ev &&
conds[i]->pre_ev->mark != ev_mark)
{
if(conds[i]->pre_ev == ev)
found = 1;
else
{
//printf("conds[i]->pre_ev->preset, ev->id: %s, %d\n", conds[i]->pre_ev->origin->name, ev->id);
found = check_back(conds[i]->pre_ev->preset,
conds[i]->pre_ev->preset_size, ev);
}
conds[i]->pre_ev->mark = ev_mark;
}
}
return found;
}
/******************************************************/
/*
Add a marking to the hash table. It is assumed that
marking = Mark([ev]). Return 1 if the marking was not
yet present; otherwise, add ev to the list of cut-off
events and return 0.
*/
int add_marking (nodelist_t *marking, event_t *ev)
{
hashcell_t *newbuck;
hashcell_t **buck = hash + marking_hash(marking);
char cmp = 2;
nodelist_t* list = NULL;
int not_present = 0, checked_back = 0;
while (*buck && (cmp = nodelist_compare(marking,(*buck)->marking)) > 0)
buck = &((*buck)->next);
/* printf("hola\n");
if(ev) printf("creating marking: %s, %d\n", ev->origin->name, ev->id);
for(list = marking; list; list = list->next)
printf("%s, ", ((place_t*)(list->node))->name);
printf("\nchao\n"); */
if(!cmp && mcmillan) /* marking is already present */
{
list = (*buck)->pre_evs;
if(!list)
{
checked_back = 1;
nodelist_push(&cutoff_list,ev);
nodelist_push(&corr_list, NULL);
}
else
for(; list && !checked_back; list = list->next)
{
ev_mark++;
if ((checked_back = check_back(ev->preset, ev->preset_size,
list->node)))
{
nodelist_push(&cutoff_list,ev);
nodelist_push(&corr_list, ((event_t*)(list->node)));
}
}
not_present = !checked_back;
(*buck)->repeat++;
nodelist_push(&((*buck)->pre_evs),ev);
}
else if (!cmp && !mcmillan)
{
(*buck)->repeat++;
//nodelist_delete(marking);
nodelist_push(&cutoff_list,ev);
if ((*buck)->pre_evs)
nodelist_push(&corr_list,((event_t*)((*buck)->pre_evs->node)));
else
nodelist_push(&corr_list, NULL);
nodelist_push(&((*buck)->pre_evs),ev);
}
if(!!cmp) /* marking is not present */
{
newbuck = MYmalloc(sizeof(hashcell_t));
newbuck->marking = marking;
newbuck->pre_evs = NULL;
if (ev) nodelist_push(&(newbuck->pre_evs),ev);
newbuck->repeat = 1;
newbuck->next = *buck;
*buck = newbuck;
not_present = 1;
}
return not_present;
}
/******************************************************/
/* Collect the initial marking. */
nodelist_t* retrieve_list (char* attribute)
{
place_t *pl;
nodelist_t *list = NULL;
for (pl = net->places; pl; pl = pl->next)
if (((!strcmp("marked",attribute) && pl->marked) !=
(!strcmp("queried",attribute) && pl->queried)) !=
(!strcmp("harmful",attribute) && pl->harmful))
nodelist_insert(&list,pl);
return list;
}
/******************************************************/
void print_marking_pl (nodelist_t* list)
{
if (!list) return;
printf("%s ",((place_t*)(list->node))->name);
print_marking_pl(list->next);
}
void print_marking_co (nodelist_t* list)
{
if (!list) return;
printf("%s ",((cond_t*)(list->node))->origin->name);
print_marking_co(list->next);
}