1 | | |
2 | | prob_pragma_string('PROCESS_ALGEBRA_MODE',true). |
3 | | |
4 | | prop(State,Prop) :- %print(state(State)),nl, |
5 | | promela_property(State,Prop). |
6 | | |
7 | | %:- dynamic inst/2, line/5. |
8 | | |
9 | | :- consult('atomic.pml.pl'). % PROLOG AST generated from atomic.pml using Java Parser |
10 | | |
11 | | |
12 | | /* |
13 | | * created by dewin dennis.winter@uni-duessldorf.de 2008 |
14 | | */ |
15 | | |
16 | | %:- module(h_int, [promela_transition/3, promela_property/2, open_promela_file/1,eval/4]). |
17 | | |
18 | | |
19 | | :- use_module(library(codesio)). |
20 | | :- use_module(library(samsort)). |
21 | | :- use_module(library(avl)). |
22 | | |
23 | | %:- use_module(probsrc(module_information)). |
24 | | %:- module_info(group,promela). |
25 | | %:- module_info(description,'This is the Promela (the Spin model checker language) extension.'). |
26 | | |
27 | | |
28 | | |
29 | | % -------------------------------------------------------- |
30 | | |
31 | | start(Out) :- |
32 | | %print('promela interpreter version 1.5, created by dennis winter'),nl, |
33 | | empty_avl(Vars), |
34 | | empty_avl(Procs), |
35 | | empty_avl(Chans), |
36 | | define(env(Vars,Procs,Chans), var(sys(pid),0), global, In2), |
37 | | define(In2, var(sys(chan_id),0), global, In3), |
38 | | define(In3, var(sys(unsafe),false), global, In4), |
39 | | define(In4, var(sys(mode),normal), global, In5), |
40 | | init(1,PC2,In5,In6), |
41 | | init2(PC2,In6,Out). |
42 | | |
43 | | init(PC, PC2, In, Out) :- |
44 | | inst(PC,S), |
45 | | %print(inst(PC,S)),nl, |
46 | | handle(S,In,In2), |
47 | | NewPC is PC+1, |
48 | | init(NewPC,PC2,In2,Out),!. |
49 | | |
50 | | init(PC,PC,In,In). |
51 | | |
52 | | |
53 | | % define array variable |
54 | | get_init_value(def(Type,array(Name,K)), Value, In, Out) :- |
55 | | ( Type=bool |
56 | | -> generate_false(K,Value), In=Out; |
57 | | Type=chan |
58 | | -> generate_chanid_array(K, Value, In, Out); |
59 | | (Type=bit; Type=byte; |
60 | | Type=pid; Type=short; Type=int; |
61 | | Type=unsigned; Type=mtype) |
62 | | -> generate_zero(K,Value), In=Out; |
63 | | %else: user-defined type |
64 | | generate_usertype_array(K, Type, Value, In, In2), |
65 | | define(In2, var(type(Name),Type), global, Out) ),!. |
66 | | |
67 | | % define variable |
68 | | get_init_value(def(Type,Name), Value, In, Out) :- |
69 | | ( Type=bool |
70 | | -> Value=false, In=Out; |
71 | | Type=chan |
72 | | -> generate_chanid(Value, In, Out); |
73 | | (Type=bit; Type=byte; |
74 | | Type=pid; Type=short; Type=int; |
75 | | Type=unsigned; Type=mtype) |
76 | | -> Value=0, In=Out; |
77 | | %else: user-defined type |
78 | | generate_usertype(Type, 0, [], Value, In, In2), |
79 | | define(In2, var(type(Name),Type), global, Out) ). |
80 | | |
81 | | % generate channel-id array |
82 | | generate_chanid_array(0, [], In, In) :- !. |
83 | | generate_chanid_array(K, [CID|Tail], In, Out) :- |
84 | | generate_chanid(CID, In, In2), |
85 | | K2 is K-1, |
86 | | generate_chanid_array(K2, Tail, In2, Out). |
87 | | |
88 | | % generate channel-id |
89 | | generate_chanid(CID, In, Out) :- |
90 | | lookup(var(sys(chan_id)), global, In, CID), |
91 | | CID2 is CID+1, |
92 | | define(In, var(sys(chan_id),CID2), global, In2), |
93 | | store(In2, chan(CID,empty), global, Out),!. |
94 | | |
95 | | % generate usertype array |
96 | | generate_usertype_array(0, _, [], In, In) :-!. |
97 | | generate_usertype_array(K, Type, [Value|Tail], In, Out) :- |
98 | | generate_usertype(Type, 0, [], Value, In, In2), |
99 | | K2 is K-1, |
100 | | generate_usertype_array(K2, Type, Tail, In2, Out). |
101 | | |
102 | | % generate usertype |
103 | | generate_usertype(Type, N, ValueIn, ValueOut, In, Out) :- |
104 | | inst(_,typedef(Type,N,def(EType,EName))), |
105 | | get_init_value(def(EType,EName), Value, In, In2), |
106 | | append(ValueIn, [Value], ValueIn2), |
107 | | N2 is N+1, |
108 | | generate_usertype(Type, N2, ValueIn2, ValueOut ,In2, Out),!. |
109 | | |
110 | | generate_usertype(_, _, Value, Value, In, In). |
111 | | |
112 | | % define globals |
113 | | handle(def(Type,Name), In, Out) :- |
114 | | trans3(def(Type,Name), global, In, Out). |
115 | | |
116 | | % typedef |
117 | | handle(typedef(_,_,_),In,In). |
118 | | |
119 | | % assign |
120 | | handle(assign(mtype,Value), In, Out) :- |
121 | | define(In, var(mtype,Value), global, Out),!. |
122 | | |
123 | | handle(assign(Name,Value), In, Out) :- |
124 | | trans3(assign(Name,Value), global, In, Out). |
125 | | |
126 | | % stop global initialisation here. |
127 | | handle(proctype(_,_,_), _, _) :- fail. |
128 | | |
129 | | |
130 | | set_record_element(Type, [array(EName,expr(K))], Value, V, PID, In, NewValue) :- |
131 | | inst(_, typedef(Type,X,def(_,array(EName,_)))), |
132 | | get_element(X, Value, Value2), |
133 | | eval(K, PID, In, K2), |
134 | | set_element(K2, Value2, V, Value3), |
135 | | set_element(X, Value, Value3, NewValue),!. |
136 | | set_record_element(Type, [EName], Value, V, _, _, NewValue) :- |
137 | | inst(_, typedef(Type,X,def(_,EName))), |
138 | | set_element(X, Value, V, NewValue),!. |
139 | | set_record_element(Type, [array(EName,expr(K))|T], Value, V, PID, In, NewValue) :- |
140 | | inst(_, typedef(Type,X,def(EType,array(EName,_)))), |
141 | | get_element(X, Value, Value2), |
142 | | eval(K, PID, In, K2), |
143 | | get_element(K2, Value2, V2), |
144 | | set_record_element(EType, T, V2, V, PID, In, V3), |
145 | | set_element(K2, Value2, V3, Value3), |
146 | | set_element(X, Value, Value3, NewValue),!. |
147 | | set_record_element(Type, [EName|T], Value, V, PID, In, NewValue) :- |
148 | | inst(_, typedef(Type,X,def(EType,EName))), |
149 | | get_element(X, Value, V2), |
150 | | set_record_element(EType, T, V2, V, PID, In, V3), |
151 | | set_element(X, Value, V3, NewValue). |
152 | | |
153 | | |
154 | | init2(PC, In, Out) :- |
155 | | inst(PC,S), |
156 | | %print(inst(PC,S)),nl, |
157 | ? | handle2(S,PC,In,In2), |
158 | | NewPC is PC+1, |
159 | | init2(NewPC,In2,Out),!. |
160 | | |
161 | | init2(_,In,In). |
162 | | |
163 | | |
164 | | handle2(proctype(active(X),Proc,_), PC, In, Out) :- |
165 | | NewPC is PC+1, |
166 | | lookup(var(sys(pid)), global, In, PID), |
167 | ? | store(In, proc(active(PID,Proc),NewPC), global, In2), |
168 | | NewPID is PID+1, |
169 | | define(In2, var(sys(pid),NewPID), global, In3), |
170 | | (X =< 1 |
171 | | -> In3=Out |
172 | | ; NewX is X-1, |
173 | | handle2(proctype(active(NewX),Proc,_), PC, In3, Out) |
174 | | ),!. |
175 | | |
176 | | handle2(proctype(inactive,_,_), _, In, In). |
177 | | |
178 | | handle2(init, PC, In, Out) :- |
179 | | NewPC is PC+1, |
180 | | lookup(var(sys(pid)), global, In, PID), |
181 | ? | store(In, proc(active(PID,init),NewPC), global, In2), |
182 | | NewPID is PID+1, |
183 | | define(In2, var(sys(pid),NewPID), global, Out). |
184 | | |
185 | | handle2(_,_,In,In). |
186 | | |
187 | | /********************************************************************/ |
188 | | |
189 | | %para_func(def(_,Name),Name). |
190 | | |
191 | | %map([], _, []). |
192 | | %map([H|T], P, [H2|T2]) :- |
193 | | % Call =.. [P,H,H2], call(Call), map(T,P,T2). |
194 | | |
195 | | |
196 | | % for type bool or mtype hone_value() must be called every time. |
197 | | % for all other types, hone_value() must only be called in case of an overflow. |
198 | | check_type(Name,Type,Value,NewValue,In) :- |
199 | | ( check_type2(Type,Value,Value2,In) |
200 | | -> ( (Type == bool; Type == mtype) |
201 | | -> hone_value(Type,Value2,NewValue,In) |
202 | | ; NewValue = Value2 ) |
203 | | ; print('Warning: Overflow of '),print(variable(Name,Type,Value)), |
204 | | hone_value(Type,Value,NewValue,In), |
205 | | print(', '),print(new_value(NewValue)),print('.'),nl ). |
206 | | |
207 | | check_type2(bit, Value, NewValue, _) :- |
208 | | number(Value), |
209 | | NewValue is round(Value), |
210 | | (NewValue == 0; NewValue == 1),!. |
211 | | |
212 | | check_type2(bool, Value, NewValue, _) :- |
213 | | number(Value), |
214 | | NewValue is round(Value), |
215 | | (NewValue == 0; NewValue == 1),!. |
216 | | |
217 | | check_type2(byte, Value, NewValue, _) :- |
218 | | number(Value), |
219 | | NewValue is round(Value), |
220 | | NewValue >= 0, |
221 | | NewValue =< 255,!. |
222 | | |
223 | | check_type2(pid, Value, NewValue, _) :- |
224 | | number(Value), |
225 | | NewValue is round(Value), |
226 | | NewValue >= 0, |
227 | | NewValue =< 255,!. |
228 | | |
229 | | check_type2(short, Value, NewValue, _) :- |
230 | | number(Value), |
231 | | NewValue is round(Value), |
232 | | NewValue >= -32768, |
233 | | NewValue =< 32767,!. |
234 | | |
235 | | check_type2(int, Value, NewValue, _) :- |
236 | | number(Value), |
237 | | NewValue is round(Value), |
238 | | NewValue >= -2147483648, |
239 | | NewValue =< 2147483647,!. |
240 | | |
241 | | check_type2(mtype, Value, Value2, In) :- |
242 | | number(Value), |
243 | | Value2 is round(Value), |
244 | | lookup(var(mtype), global, In, MList), |
245 | | length(MList, N), |
246 | | Value2 >= 1, |
247 | | Value2 =< N,!. |
248 | | |
249 | | check_type2(chan, Value, _, _) :- |
250 | | % what's the maximum chan_id? |
251 | | number(Value), |
252 | | print('chan typecheck. Use define(In var(chan(..)..) instead. chan_id: '),print(Value),nl. |
253 | | |
254 | | hone_value(bit, Value, NewValue, _) :- |
255 | | NewValue is Value mod 2,!. |
256 | | |
257 | | hone_value(bool, Value, NewValue, _) :- |
258 | | Value2 is Value mod 2, |
259 | | ( false(Value2) |
260 | | -> NewValue = false |
261 | | ; NewValue = true ),!. |
262 | | |
263 | | hone_value(byte, Value, NewValue, _) :- |
264 | | NewValue is Value mod 256,!. |
265 | | |
266 | | hone_value(pid, Value, NewValue, _) :- |
267 | | NewValue is Value mod 256,!. |
268 | | |
269 | | hone_value(short, Value, NewValue, _) :- |
270 | | ( Value > 32767 |
271 | | -> Value2 is Value mod 32768, |
272 | | NewValue is Value2 - 32768 ), |
273 | | ( Value < -32768 |
274 | | -> Value2 is Value mod 32769, |
275 | | NewValue is Value2 - 1 ),!. |
276 | | |
277 | | hone_value(int, Value, NewValue, _) :- |
278 | | ( Value > 2147483647 |
279 | | -> Value2 is Value mod 2147483648, |
280 | | NewValue is Value2 - 2147483648 ), |
281 | | ( Value < -2147483648 |
282 | | -> Value2 is Value mod 2147483649, |
283 | | NewValue is Value2 - 1 ),!. |
284 | | |
285 | | hone_value(mtype, Value, ctype(NewValue), In) :- |
286 | | lookup(var(mtype), global, In, MList), |
287 | | length(MList, N), |
288 | | Value2 is Value -1, |
289 | | Value3 is Value2 mod N, |
290 | | Value4 is Value3 + 1, |
291 | | K is N - Value4, |
292 | | get_element(K, MList, NewValue),!. |
293 | | |
294 | | hone_value(chan, Value, Value, _). |
295 | | |
296 | | /********************************************************************/ |
297 | | |
298 | | % store variable |
299 | | % (stores singles, arrays, records; all of them as global or as local variable) |
300 | | store(env(Vars,Procs,Chans), var(Name,Type,expr(V)), PID, env(NewVars,Procs,Chans)) :- |
301 | | % set Name4 |
302 | | ( Name = record([Name2|Tail]) -> true; Name2 = Name ), |
303 | | ( Name2 = array(Name3,expr(K)) -> true; Name3 = Name2 ), |
304 | | ( (PID \= global, lookup2(key(Name3,PID),Vars,_)) |
305 | | -> Name4 = key(Name3,PID) |
306 | | ; Name4 = Name3 ), |
307 | | lookup2(Name4, Vars, Value), |
308 | ? | eval(V, PID, env(Vars,Procs,Chans), V1), |
309 | | check_type(Name,Type,V1,V2,env(Vars,_,_)), |
310 | | % set Value4 |
311 | | ( Name2 = array(_,_) |
312 | ? | -> eval(K,PID,env(Vars,Procs,Chans),K2), get_element(K2,Value,Value2) |
313 | | ; Value2 = Value ), |
314 | | ( Name = record(_) |
315 | | -> lookup2(type(Name3),Vars,DType), set_record_element(DType,Tail,Value2,V2,PID,env(Vars,_,_),Value3) |
316 | | ; Value3 = V2 ), |
317 | | ( Name2 = array(_,_) |
318 | ? | -> set_element(K2,Value,Value3,Value4) |
319 | | % Value = [_|_]: for example short c[3] = 3, then set all elements of c to 3. |
320 | | ; Name \= record(_), Value = [_|_] |
321 | | -> set_all_elements(Value,V2,Value4) |
322 | | ; Value4 = Value3 ), |
323 | | %print(end_store(Name,Type,expr(V))),nl, |
324 | | store2(Vars,Name4,Value4,NewVars). |
325 | | |
326 | | % store global proctype |
327 | | store(env(Vars,Procs,Chans), proc(PID,PC), global, env(Vars,NewProcs,Chans)) :- |
328 | | store2(Procs, PID, PC, NewProcs). |
329 | | |
330 | | % store global channel |
331 | | store(env(Vars,Procs,Chans), chan(Name,Value), _, env(Vars,Procs,NewChans)) :- |
332 | | store2(Chans, Name, Value, NewChans). |
333 | | |
334 | | |
335 | | % define local variable |
336 | | define(env(Vars,Procs,Chans), var(Name,Value), PID, env(NewVars,Procs,Chans)) :- |
337 | | PID \= global, |
338 | | store2(Vars, key(Name,PID), Value, NewVars),!. |
339 | | |
340 | | % define global variable |
341 | | define(env(Vars,Procs,Chans), var(Name,Value), global, env(NewVars,Procs,Chans)) :- |
342 | | store2(Vars, Name, Value, NewVars). |
343 | | |
344 | | |
345 | | %store2([],Key,Value,[Key/Value]) :- |
346 | | % print(store_new_var(Key,Value)),nl. |
347 | | %store2([Key/_|T],Key,Value,[Key/Value|T]). |
348 | | %store2([Key2/Value2|T],Key,Value,[Key2/Value2|BT]) :- |
349 | | % Key \= Key2, store2(T,Key,Value,BT). |
350 | | |
351 | | store2(AVL,Key,Value,NewAVL) :- |
352 | | avl_store(Key, AVL, Value, NewAVL). |
353 | | |
354 | | % lookup variable |
355 | | % (looks up singles, arrays, records; all of them as global or as local variable) |
356 | | lookup(var(Name), PID, env(Vars,Procs,Chans), Value3) :- |
357 | | % set Name4 |
358 | | %print(lookup(var(Name))),nl, |
359 | | ( Name = record([Name2|Tail]) -> true; Name2 = Name ), |
360 | | ( Name2 = array(Name3,expr(K)) -> true; Name3 = Name2 ), |
361 | | ( (PID \= global, lookup2(key(Name3,PID),Vars,_)) |
362 | | -> Name4 = key(Name3,PID) |
363 | | ; Name4 = Name3 ), |
364 | | lookup2(Name4, Vars, Value), |
365 | | % get Value3 |
366 | | ( Name2 = array(_,_) |
367 | ? | -> (eval(K,PID,env(Vars,Procs,Chans),K2), get_element(K2,Value,Value2)) |
368 | | ; Value2 = Value ), |
369 | | ( Name = record(_) |
370 | | -> (lookup2(type(Name3),Vars,Type), get_record_element(Type,Tail,Value2,PID,env(Vars,_,_),Value3)) |
371 | | ; Value3 = Value2 ). |
372 | | |
373 | | % lookup global proctype |
374 | | lookup(proc(PID), global, env(_,Procs,_), PC) :- |
375 | ? | lookup3(PID, Procs, PC). |
376 | | |
377 | | % lookup global channel |
378 | | lookup(chan(Name), global, env(_,_,Chans), Value) :- |
379 | | lookup2(Name, Chans, Value). |
380 | | |
381 | | |
382 | | %lookup2(Key,[],_) :- |
383 | | % %ground(Key), |
384 | | % print(lookup_var_not_found(Key)),nl,fail. |
385 | | %lookup2(Key,[Key/Value|_T],Value). |
386 | | %lookup2(Key,[Key2/_|T],Value) :- |
387 | | % Key \= Key2, lookup2(Key,T,Value). |
388 | | |
389 | | % look up, given a key |
390 | | lookup2(Key,AVL,Value) :- |
391 | | avl_fetch(Key,AVL,Value). |
392 | | |
393 | | % look up, if there are possibly multiple matchings for key or value |
394 | | lookup3(Key,AVL,Value) :- |
395 | ? | avl_member(Key,AVL,Value). |
396 | | |
397 | | |
398 | | %remove(Key,[],_) :- |
399 | | % %print(remove_var_not_found(Key)),nl. |
400 | | % print(remove_var_not_found_error(Key)),nl,fail. |
401 | | %remove(Key,[Key/_|T],T). |
402 | | %remove(Key,[Key2/Value|T],[Key2/Value|T2]) :- |
403 | | % Key \= Key2, remove(Key,T,T2). |
404 | | |
405 | | remove(Key,AVL,NewAVL) :- |
406 | | avl_delete(Key, AVL, _, NewAVL). |
407 | | |
408 | | % remove local vars |
409 | | remove_vars(PID, env(Vars,Procs,Chans), env(NewVars,Procs,Chans)) :- |
410 | | %findall(key(Name,PID), lookup2(key(Name,PID),Vars,_), List), |
411 | | findall(key(Name,PID), lookup3(key(Name,PID),Vars,_), List), |
412 | | remove_func(List,Vars,NewVars). |
413 | | |
414 | | % remove pointers to channels and channels itself |
415 | | remove_chans(PID, env(Vars,Procs,Chans), env(NewVars,Procs,NewChans)) :- |
416 | | findall(key(chan(Name),PID), lookup3(key(chan(Name),PID),Vars,_), List), |
417 | | remove_func(List,Vars,NewVars), |
418 | | findall(CID, lookup3(key(chan(_),PID),Vars,CID), List2), |
419 | | remove_channels(List2,NewVars,Chans,NewChans). |
420 | | |
421 | | remove_children(PID2, env(Vars,Procs,Chans), env(NewVars,Procs,Chans)) :- |
422 | | findall(child(PID1, PID2), lookup3(child(PID1,PID2), Vars, true), List), |
423 | | remove_func(List,Vars,NewVars). |
424 | | |
425 | | remove_proc(active(PID,Name), env(Vars,Procs,Chans), env(Vars,NewProcs,Chans)) :- |
426 | | remove(active(PID,Name), Procs, NewProcs). |
427 | | |
428 | | remove_func([], Vars, Vars). |
429 | | remove_func([H|T], Vars, NewVars) :- |
430 | | remove(H, Vars, Vars2), |
431 | | remove_func(T, Vars2, NewVars). |
432 | | |
433 | | % remove global channels (only when no pointer is pointing to channel) |
434 | | remove_channels([], _, Chans, Chans). |
435 | | remove_channels([ID|Tail], Vars, Chans, NewChans) :- |
436 | | number(ID), |
437 | | ( (lookup3(chan(_),Vars,ID); lookup3(key(chan(_),_),Vars,ID)) |
438 | | -> Chans2=Chans |
439 | | ; remove(ID, Chans, Chans2) ), |
440 | | %print(remove_channel(ID)),nl, |
441 | | remove_channels(Tail, Vars, Chans2, NewChans). |
442 | | % list of CID's (array) |
443 | | remove_channels([[]|Tail], Vars, Chans, NewChans) :- |
444 | | remove_channels(Tail, Vars, Chans, NewChans). |
445 | | % list of CID's (array) |
446 | | remove_channels([[H|T]|Tail], Vars, Chans, NewChans) :- |
447 | | number(H), |
448 | | ( (lookup3(chan(_),Vars,H); lookup3(key(chan(_),_),Vars,H)) |
449 | | -> Chans2=Chans |
450 | | ; remove(H, Chans, Chans2) ), |
451 | | %print(remove_channels(H)),nl, |
452 | | remove_channels([T|Tail], Vars, Chans2, NewChans). |
453 | | |
454 | | |
455 | | /************************************************************/ |
456 | | |
457 | | eval_list([], _, _, []). |
458 | | eval_list([expr(H)|T], PID, In, [H2|T2]) :- |
459 | | eval(H, PID, In, H2), |
460 | | eval_list(T, PID, In, T2),!. |
461 | | |
462 | | eval(cond(X,Y,Z), PID, In, R) :- |
463 | | eval(X, PID, In, X1), |
464 | | ( true(X1) |
465 | | -> eval(Y, PID, In, R) |
466 | | ; eval(Z, PID, In, R) ). |
467 | | eval(or(X,Y), PID, In, R) :- |
468 | | eval(X, PID, In, R2), |
469 | | ( true(R2) |
470 | | -> R=R2 |
471 | | ; eval(Y, PID, In, R) ). |
472 | | eval(and(X,Y), PID, In, R) :- |
473 | | eval(X, PID, In, R2), |
474 | | ( true(R2) |
475 | | -> eval(Y, PID, In, R) |
476 | | ; R=R2 ). |
477 | | eval(eq(X,Y), PID, In, R) :- |
478 | | eval(X, PID, In, X1), eval(Y, PID, In, Y1), |
479 | | ( X1==Y1 |
480 | | -> R=1 |
481 | | ; R=0 ). |
482 | | eval(uneq(X,Y), PID, In, R) :- |
483 | | eval(X, PID, In, X1), eval(Y, PID, In, Y1), |
484 | | ( X1==Y1 |
485 | | -> R=0 |
486 | | ; R=1 ). |
487 | | eval(lt(X,Y), PID, In, R) :- |
488 | ? | eval(X, PID, In, X1), eval(Y, PID, In, Y1), |
489 | | ( X1<Y1 -> R=1; R=0 ). |
490 | | eval(gt(X,Y), PID, In, R) :- |
491 | | eval(X, PID, In, X1), eval(Y, PID, In, Y1), |
492 | | ( X1>Y1 -> R=1; R=0 ). |
493 | | eval(leqt(X,Y), PID, In, R) :- |
494 | | eval(X, PID, In, X1), eval(Y, PID, In, Y1), |
495 | | ( X1=<Y1 -> R=1; R=0 ). |
496 | | eval(geqt(X,Y), PID, In, R) :- |
497 | | eval(X, PID, In, X1), eval(Y, PID, In, Y1), |
498 | | ( X1>=Y1 -> R=1; R=0 ). |
499 | | eval('+'(X,Y), PID, In, R) :- |
500 | | eval(X, PID, In, X1), eval(Y, PID, In, Y1), R is X1+Y1. |
501 | | eval('-'(X,Y), PID, In, R) :- |
502 | | eval(X, PID, In, X1), eval(Y, PID, In, Y1), R is X1-Y1. |
503 | | eval('*'(X,Y), PID, In, R) :- |
504 | | eval(X, PID, In, X1), eval(Y, PID, In, Y1), R is X1*Y1. |
505 | | eval('/'(X,Y), PID, In, R) :- |
506 | | eval(X, PID, In, X1), eval(Y, PID, In, Y1), R is X1/Y1. |
507 | | eval('mod'(X,Y), PID, In, R) :- |
508 | | eval(X, PID, In, X1), eval(Y, PID, In, Y1), R is X1 mod Y1. |
509 | | eval(not(X), PID, In, R) :- |
510 | | eval(X, PID, In, X1), |
511 | | ( true(X1) -> R=0; R=1 ). |
512 | | % bit complement |
513 | | eval(compl(X), PID, In, R) :- |
514 | | eval(X, PID, In, X1), |
515 | | R is \ X1. |
516 | | eval(bitor(X,Y), PID, In, R) :- |
517 | | eval(X, PID, In, X1), eval(Y, PID, In, Y1), |
518 | | R is X1 \/ Y1. |
519 | | eval(bitxor(X,Y), PID, In, R) :- |
520 | | eval(X, PID, In, X1), eval(Y, PID, In, Y1), |
521 | | R is (X1 \/ Y1) /\ \(X1 /\ Y1). |
522 | | eval(bitand(X,Y), PID, In, R) :- |
523 | | eval(X, PID, In, X1), eval(Y, PID, In, Y1), |
524 | | R is X1 /\ Y1. |
525 | | eval(lshift(X,Y), PID, In, R) :- |
526 | | eval(X, PID, In, X1), eval(Y, PID, In, Y1), |
527 | | R is X1 << Y1. |
528 | | eval(rshift(X,Y), PID, In, R) :- |
529 | | eval(X, PID, In, X1), eval(Y, PID, In, Y1), |
530 | | R is X1 >> Y1. |
531 | | eval((expr(X)), PID, In, R) :- |
532 | | eval(X, PID, In, R),!. |
533 | | eval(true, _, _, 1) :- !. |
534 | | eval(false, _, _, 0) :- !. |
535 | | eval(skip, _, _, 1) :- !. |
536 | | eval(X, _, _, X) :- |
537 | | (number(X); X=[_|_]),!. |
538 | | eval(ctype(X), _, In, R) :- |
539 | | lookup(var(mtype), global, In, Value), |
540 | | get_element(K, Value, X), |
541 | | length(Value, N), |
542 | | R is N - K. |
543 | | eval(string(X), _, _, R) :- |
544 | | atom_codes(X,R). |
545 | | eval(timeout, _, In, R) :- |
546 | | ( find_exec(In) -> R=0; R=1 ),!. |
547 | | eval(pid, PID, _, PID) :- !. |
548 | | eval(nr_pr, _, env(_,Procs,_), R) :- |
549 | | %length(Procs,R),!. |
550 | | avl_size(Procs,R),!. |
551 | | eval(Name, PID, In, R) :- |
552 | | % looks up singles, chan(Name), array(Name,K), record(Name). |
553 | | (atomic(Name); Name=chan(_); Name=array(_,_); Name=record(_)), |
554 | ? | lookup(var(Name), PID, In, R2), |
555 | | eval(R2, PID, In, R). |
556 | | eval(nfull(chan(Name)), PID, In, R) :- |
557 | | eval(empty(chan(Name)), PID, In, R). % fixed by leuschel |
558 | | eval(empty(chan(Name)), PID, In, R) :- |
559 | | lookup(var(chan(Name)), PID, In, CID), |
560 | | lookup(chan(CID), global, In, Value), |
561 | | ( Value = [[empty]|_] -> R=1; R=0 ). |
562 | | eval(full(chan(Name)), PID, In, R) :- |
563 | | eval(nempty(chan(Name)), PID, In, R). |
564 | | eval(nempty(chan(Name)), PID, In, R) :- |
565 | | lookup(var(chan(Name)), PID, In, CID), |
566 | | lookup(chan(CID), global, In, Value), |
567 | | ( Value = [[empty]|_] -> R=0; R=1 ). |
568 | | eval(len(chan(Name)), PID, In, R) :- |
569 | | lookup(var(chan(Name)), PID, In, CID), |
570 | | lookup(chan(CID), global, In, Value), |
571 | | chan_length(Value,R). |
572 | | %print(chan_length(Value,R)),nl. |
573 | | eval(expr_poll(Name,Msg), PID, In, R) :- |
574 | | ( trans3(poll(Name,Msg),PID,In,_) -> R=1; R=0 ). |
575 | | eval(expr_random_poll(Name,Msg), PID, In, R) :- |
576 | | ( trans3(random_poll(Name,Msg),PID,In,_) -> R=1; R=0 ). |
577 | | |
578 | | true(X) :- |
579 | | \+false(X). |
580 | | false(X) :- |
581 | | X==0. |
582 | | |
583 | | |
584 | | chan_length(empty,0). |
585 | | chan_length([],0). |
586 | | chan_length([[empty]|_],0). |
587 | | chan_length([H|T],R) :- |
588 | | H \= [empty], chan_length(T,X), R is X+1. |
589 | | |
590 | | |
591 | | get_record_element(Type, [array(EName,expr(K))], Value, PID, In, R) :- |
592 | | inst(_, typedef(Type,X,def(_,array(EName,_)))), |
593 | | get_element(X, Value, Value2), |
594 | | eval(K, PID, In, K2), |
595 | | get_element(K2, Value2, R),!. |
596 | | get_record_element(Type, [EName], Value, _, _, R) :- |
597 | | inst(_, typedef(Type,X,def(_,EName))), |
598 | | get_element(X,Value,R),!. |
599 | | get_record_element(Type, [array(EName,expr(K))|T], Value, PID, In, R) :- |
600 | | inst(_, typedef(Type,X,def(EType,array(EName,_)))), |
601 | | get_element(X, Value, Value2), |
602 | | eval(K, PID, In, K2), |
603 | | get_element(K2, Value2, V2), |
604 | | get_record_element(EType, T, V2, PID, In, R),!. |
605 | | get_record_element(Type, [EName|T], Value, PID, In, R) :- |
606 | | inst(_, typedef(Type,X,def(EType,EName))), |
607 | | get_element(X, Value, V2), |
608 | | get_record_element(EType, T, V2, PID, In, R). |
609 | | |
610 | | |
611 | | /************************************************************/ |
612 | | |
613 | | % e.g.: get_element(4,[1,2,3,4,5],5), means 4th element of L is 5. |
614 | ? | get_element(R,List,E) :- get_element2(0,List,E,R). |
615 | | get_element2(X,[E|_],E,X). |
616 | ? | get_element2(X,[_|T],E,R) :- Y is X+1, get_element2(Y,T,E,R). |
617 | | |
618 | | % e.g.: set_element(1,[1,2,3,4],8,[1,8,3,4]) |
619 | | set_element(0,[_|T1],V,[V|T1]). |
620 | ? | set_element(X,[H1|T1],V,[H1|T2]) :- Y is X-1, set_element(Y,T1,V,T2). |
621 | | |
622 | | % e.g.: set_all_elements([1,2,3,4],6,[6,6,6,6]) |
623 | | set_all_elements([],_,[]). |
624 | | set_all_elements([_|T1],E,[E|T2]) :- |
625 | | set_all_elements(T1,E,T2). |
626 | | |
627 | | |
628 | | % e.g.: remove_element(2,[1,2,3,4],[1,2,4]) |
629 | | remove_element(0,[_|T1],T1). |
630 | | remove_element(X,[H1|T1],[H1|T2]) :- Y is X-1, remove_element(Y,T1,T2). |
631 | | |
632 | | % e.g.: X=4 -> L=[0,0,0,0] |
633 | | generate_zero(0,[]) :- !. |
634 | | generate_zero(X,[0|R]) :- Y is X-1, generate_zero(Y,R). |
635 | | |
636 | | generate_false(0,[]) :- !. |
637 | | generate_false(X,[false|R]) :- Y is X-1, generate_false(Y,R). |
638 | | |
639 | | generate_chan(0,_,[]) :- !. |
640 | | generate_chan(X,Msg,[Msg|R]) :- Y is X-1, generate_chan(Y,Msg,R). |
641 | | |
642 | | /************************************************************/ |
643 | | |
644 | | trans(io([Statement], proc(PID,Proc), Span), In, Out) :- % print(try_trans(In,Out)),nl,trace, |
645 | | lookup(proc(active(PID,Proc)), global, In, PC), |
646 | | inst(PC, S), |
647 | | lookup(var(sys(mode)), global, In, MValue), |
648 | | %print(try_execute(PC,S)),nl, |
649 | | check_mode(MValue, S), |
650 | | trans2(S, Statement, PC, PC2, PID, Span, In, In2), |
651 | | %print(executed(PC,S)),nl, |
652 | | check_jump(PC2, NewPC), |
653 | | %print(jump(PC2,NewPC)),nl, |
654 | | ( NewPC \== dead |
655 | | -> store(In2, proc(active(PID,Proc),NewPC), global, Out) |
656 | | ; remove_proc(active(PID,Proc), In2, Out) ). |
657 | | |
658 | | check_mode(normal, _). |
659 | | check_mode(p_atomic, p_atomic(_)). |
660 | | check_mode(d_step, d_step(_)). |
661 | | |
662 | | % executes igoto or ibreak when necessary. |
663 | | check_jump(PC, NewPC) :- |
664 | ? | ( inst(PC,S), check_jump2(S, PC2) |
665 | | -> check_jump(PC2, NewPC) |
666 | | ; NewPC = PC ). |
667 | | |
668 | | check_jump2(igoto(X), NewPC) :- |
669 | | ( number(X) |
670 | | -> NewPC is X |
671 | | ; inst(Y,label(X)), NewPC is Y ). |
672 | | check_jump2(ibreak(X), NewPC) :- |
673 | | number(X), |
674 | | NewPC is X. |
675 | | check_jump2(p_atomic(igoto(X)), NewPC) :- |
676 | | check_jump2(igoto(X), NewPC). |
677 | | check_jump2(p_atomic(ibreak(X)), NewPC) :- |
678 | | check_jump2(ibreak(X), NewPC). |
679 | | check_jump2(d_step(igoto(X)), NewPC) :- |
680 | | check_jump2(igoto(X), NewPC). |
681 | | check_jump2(d_step(ibreak(X)), NewPC) :- |
682 | | check_jump2(ibreak(X), NewPC). |
683 | | |
684 | | |
685 | | trans2(do(Alt), Statement, _, NewPC, PID, Span, In, Out) :- |
686 | ? | member(A,Alt), |
687 | | inst(A,S), |
688 | | ( (S=else; S=d_step(else); S=p_atomic(else)) |
689 | ? | -> delete(Alt,A,Alt2), |
690 | ? | ( find_exec(Alt2,PID,In) -> fail; true ) |
691 | | ; true ), |
692 | ? | trans2(S,Statement,A,NewPC,PID,Span,In,Out). |
693 | | |
694 | | trans2(if(Alt), Statement, _, NewPC, PID, Span, In, Out) :- |
695 | | trans2(do(Alt), Statement, _, NewPC, PID, Span, In, Out). |
696 | | |
697 | | trans2(unless(M,E), Statement, _, NewPC, PID, Span, In, Out) :- |
698 | | inst(E,Escape), |
699 | | ( trans2(Escape,Statement,E,NewPC,PID,Span,In,Out) |
700 | | -> true |
701 | | ; (inst(M,Main), trans2(Main,Statement,M,NewPC,PID,Span,In,Out)) ). |
702 | | |
703 | | % provided (constraint on proctypes) |
704 | | trans2(provided(expr(Expr)), Statement, PC, NewPC, PID, Span, In, Out) :- |
705 | | eval(Expr, PID, In, R), |
706 | | ( true(R) |
707 | | -> (PC2 is PC+1, inst(PC2,S), trans2(S,Statement,PC2,NewPC,PID,Span,In,Out)) |
708 | | ; fail ). |
709 | | |
710 | | % Distinction between d_step_start and d_step is important for to not recognize |
711 | | % a new starting d_step statement as a continuing d_step. |
712 | | trans2(d_step_start(S), Statement, PC, NewPC, PID, Span, In, Out) :- |
713 | | trans2(d_step(S), Statement, PC, NewPC, PID, Span, In, Out). |
714 | | |
715 | | trans2(p_atomic_start(S), Statement, PC, NewPC, PID, Span, In, Out) :- |
716 | ? | trans2(p_atomic(S), Statement, PC, NewPC, PID, Span, In, Out). |
717 | | |
718 | | trans2(d_step(S), Statement, PC, NewPC, PID, Span, In, Out) :- |
719 | | trans2(S, Statement, PC, PC2, PID, Span, In, In2), |
720 | | check_jump(PC2, NewPC), |
721 | | inst(NewPC, S2), |
722 | | % look, if next step is d_step |
723 | | ( S2 = d_step(_) |
724 | | -> define(In2, var(sys(mode),d_step), global, Out) |
725 | | ; define(In2, var(sys(mode),normal), global, Out) ),!. |
726 | | |
727 | | trans2(p_atomic(S), Statement, PC, NewPC, PID, Span, In, Out) :- |
728 | ? | trans2(S, Statement, PC, PC2, PID, Span, In, In2), |
729 | | check_jump(PC2, NewPC), |
730 | | inst(NewPC, S2), |
731 | | %print(p_atomic_inst(NewPC,S2)),nl, |
732 | | % look, if next step is p_atomic and is executable. |
733 | ? | ( S2 = p_atomic(S3), trans2(S3, _, NewPC, _, PID, _, In2, _) |
734 | | -> define(In2, var(sys(mode),p_atomic), global, Out)%, print(define(p_atomic)),nl |
735 | | ; define(In2, var(sys(mode),normal), global, Out) ).%, print(define(normal)),nl ). |
736 | | |
737 | | % destructor |
738 | | trans2(destructor, destructor, PC, NewPC, PID, src_span(SRow,SCol,ERow,ECol,_,_), In, Out) :- |
739 | | % ensure, PID has no child. |
740 | | In = env(Vars,_,_), |
741 | | \+ lookup3(child(PID,_), Vars, true), |
742 | | % remove channels that are not being referenced |
743 | | remove_chans(PID, In, In2), |
744 | | remove_vars(PID, In2, In3), |
745 | | remove_children(PID, In3, Out), |
746 | | NewPC = dead, |
747 | | line(PC,SRow,SCol,ERow,ECol),!. |
748 | | |
749 | | trans2(goto(X), goto(X), PC, NewPC, _, src_span(SRow,SCol,ERow,ECol,_,_), In, In) :- |
750 | | ( number(X) -> NewPC is X; inst(Y,label(X)), NewPC is Y ), |
751 | | inst(NewPC,S), |
752 | | % goto into a d_step is not allowed |
753 | | S \= d_step(_), |
754 | | line(PC,SRow,SCol,ERow,ECol). |
755 | | |
756 | | trans2(break(X), break(X), PC, NewPC, _, src_span(SRow,SCol,ERow,ECol,_,_), In, In) :- |
757 | | NewPC is X, |
758 | | line(PC,SRow,SCol,ERow,ECol). |
759 | | |
760 | | trans2(label(_), Statement, PC, NewPC, PID, Span, In, Out) :- |
761 | | PC2 is PC+1, |
762 | | inst(PC2,S), |
763 | | trans2(S, Statement, PC2, NewPC, PID, Span, In, Out). |
764 | | |
765 | | trans2(printf(TextList), printf(Text), PC, NewPC, _, src_span(SRow,SCol,ERow,ECol,_,_), In, In) :- |
766 | | % ex.: atom_codes(X,[97]). |
767 | | % X = a |
768 | | atom_codes(Text,TextList), |
769 | | NewPC is PC+1, |
770 | | line(PC,SRow,SCol,ERow,ECol). |
771 | | |
772 | | trans2(printf(TextList,VarList), printf(Result), PC, NewPC, PID, src_span(SRow,SCol,ERow,ECol,_,_), In, In) :- |
773 | | % ex.: format("~s~2f",[a,0.3]). |
774 | | % a0.30 |
775 | | % format_to_codes("a ~c",[13],R). |
776 | | % R = [97,32,13] ? |
777 | | % |
778 | | eval_list(VarList, PID, In, ValueList), |
779 | | atom_codes(Text,TextList), |
780 | | format_to_codes(Text,ValueList,ResultList), |
781 | | atom_codes(Result,ResultList), |
782 | | NewPC is PC+1, |
783 | | line(PC,SRow,SCol,ERow,ECol). |
784 | | |
785 | | trans2(printm(expr(Expr)), printm(Result), PC, NewPC, PID, src_span(SRow,SCol,ERow,ECol,_,_), In, In) :- |
786 | | eval(Expr, PID, In, Result), |
787 | | NewPC is PC+1, |
788 | | line(PC,SRow,SCol,ERow,ECol). |
789 | | |
790 | | trans2(Statement, Statement, PC, NewPC, PID, src_span(SRow,SCol,ERow,ECol,_,_), In, Out) :- |
791 | ? | trans3(Statement, PID, In, Out), |
792 | | NewPC is PC+1, |
793 | | line(PC,SRow,SCol,ERow,ECol). |
794 | | |
795 | | trans2(send(Name,Msg), Statement, PC, NewPC, PID, SpanOut, In, Out) :- |
796 | | lookup(var(Name), PID, In, CID), |
797 | | %% print(chan_id(CID)),nl, |
798 | | ( lookup(chan(CID), global, In, []) |
799 | | -> r_send(CID, Name, Msg, Statement, PID, Span2, In, Out), SpanOut = multi_span(SRow,SCol,ERow,ECol,_,_,Span2) |
800 | | ; n_send(CID, Name, Msg, Statement, PID, In, Out), SpanOut = src_span(SRow,SCol,ERow,ECol,_,_) ), |
801 | | NewPC is PC+1, |
802 | | line(PC,SRow,SCol,ERow,ECol). |
803 | | |
804 | | trans2(sorted_send(Name,Msg), Statement, PC, NewPC, PID, SpanOut, In, Out) :- |
805 | | lookup(var(Name), PID, In, CID), |
806 | | %% print(chan_id(CID)),nl, |
807 | | ( lookup(chan(CID), global, In, []) |
808 | | -> r_send(CID, Name, Msg, Statement, PID, Span2, In, Out), SpanOut = multi_span(SRow,SCol,ERow,ECol,_,_,Span2) |
809 | | ; s_send(CID, Name, Msg, Statement, PID, In, Out), SpanOut = src_span(SRow,SCol,ERow,ECol,_,_) ), |
810 | | NewPC is PC+1, |
811 | | line(PC,SRow,SCol,ERow,ECol). |
812 | | |
813 | | % normal send |
814 | | n_send(CID, Name, Msg, Statement, PID, In, Out) :- |
815 | | lookup(chan(CID), global, In, Value), |
816 | | get_element(K, Value, [empty]), % Backtracking! |
817 | | %print(map_send(Msg)),nl, |
818 | | eval_list(Msg, PID, In, Msg2), |
819 | | %print(map2_send(Msg2)),nl, |
820 | | set_element(K, Value, Msg2, NewValue), |
821 | | store(In, chan(CID,NewValue), global, Out), |
822 | | Statement = send(Name,Msg),!. |
823 | | |
824 | | % rendezvous-send |
825 | | r_send(CID, Name, Msg, Statement, PID, Span, In, Out) :- |
826 | | eval_list(Msg, PID, In, Msg2), |
827 | | %print(msg3(Msg2)),nl, |
828 | | store(In, chan(CID,[Msg2]), global, In2), |
829 | | % search matching receive |
830 | | lookup(proc(active(RPID,Proc)), global, In, PC), |
831 | | inst(PC, S), |
832 | | % S can be recv(), igoto(), ibreak(), etc. |
833 | | trans2(S,recv(RName,RMsg), PC, NewPC, RPID, Span, In2, In3), |
834 | | lookup(chan(CID), global, In3, [[empty]]), |
835 | | % reset channel |
836 | | store(In3, chan(CID,[]), global, In4), |
837 | | store(In4, proc(active(RPID,Proc), NewPC), global, Out), |
838 | | Statement = '.'(r_send(Name,Msg),r_recv(RName,RMsg)). |
839 | | % Permit Backtracking in this clause! |
840 | | |
841 | | % sorted send |
842 | | s_send(CID, Name, Msg, Statement, PID, In, Out) :- |
843 | | lookup(chan(CID), global, In, Value), |
844 | | get_element(K, Value, [empty]), % Backtracking! |
845 | | %print(map_send(Msg)),nl, |
846 | | eval_list(Msg, PID, In, Msg2), |
847 | | %print(map2_send(Msg2)),nl, |
848 | | set_element(K, Value, Msg2, NewValue), |
849 | | %print(newValue(NewValue)),nl, |
850 | | samsort(NewValue, SortedValue), |
851 | | %print(sortedValue(SortedValue)),nl, |
852 | | store(In, chan(CID,SortedValue), global, Out), |
853 | | Statement = sorted_send(Name,Msg),!. |
854 | | |
855 | | % normal receive |
856 | | trans3(recv(Name,Msg), PID, In, Out) :- |
857 | | lookup(var(Name), PID, In, Id), |
858 | | lookup(chan(Id), global, In, Value), |
859 | | get_element(0, Value, Msg2), |
860 | | Msg2 \== [empty], |
861 | | %print(map_recv(Msg)),nl, |
862 | | recv_eval(Msg, PID, In, In2, Msg2), |
863 | | %print(map2_recv(Msg2)),nl, |
864 | | remove_element(0, Value, Value2), |
865 | | append(Value2, [[empty]], NewValue), |
866 | | store(In2, chan(Id,NewValue), global, Out). |
867 | | |
868 | | % random receive |
869 | | trans3(random_recv(Name,Msg), PID, In, Out) :- |
870 | | lookup(var(Name), PID, In, Id), |
871 | | lookup(chan(Id), global, In, Value), |
872 | | get_element(K, Value, Msg2), % Backtracking! |
873 | | Msg2 \== [empty], |
874 | | %print(map_recv(Msg)),nl, |
875 | | recv_eval(Msg, PID, In, In2, Msg2), |
876 | | %print(map2_recv(Msg2)),nl, |
877 | | remove_element(K, Value, Value2), |
878 | | append(Value2, [[empty]], NewValue), |
879 | | store(In2, chan(Id,NewValue), global, Out),!. |
880 | | |
881 | | % normal poll |
882 | | trans3(poll(Name,Msg), PID, In, Out) :- |
883 | | lookup(var(Name), PID, In, Id), |
884 | | lookup(chan(Id), global, In, Value), |
885 | | get_element(0, Value, Msg2), |
886 | | Msg2 \== [empty], |
887 | | %print(map_recv(Msg)),nl, |
888 | | recv_eval(Msg, PID, In, Out, Msg2). |
889 | | %print(map2_recv(Msg2)),nl. |
890 | | |
891 | | % random poll |
892 | | trans3(random_poll(Name,Msg), PID, In, Out) :- |
893 | | lookup(var(Name), PID, In, Id), |
894 | | lookup(chan(Id), global, In, Value), |
895 | | get_element(_, Value, Msg2), % Backtracking! |
896 | | Msg2 \== [empty], |
897 | | %print(map_recv(Msg)),nl, |
898 | | recv_eval(Msg, PID, In, Out, Msg2),!. |
899 | | %print(map2_recv(Msg2)),nl,!. |
900 | | |
901 | | trans3(expr(run(Proc,ValueList)), PID, In, Out) :- |
902 | | inst(PC,proctype(_,Proc,PList)), |
903 | | PC2 is PC + 1, |
904 | | %-----------------% |
905 | | lookup(var(sys(pid)), global, In, PID2), |
906 | | store(In, proc(active(PID2,Proc),PC2), global, In2), |
907 | | set_local_vars(PList, ValueList, PID, PID2, In2, In3), |
908 | | PID3 is PID2+1, |
909 | | define(In3, var(sys(pid),PID3), global, In4), |
910 | | define(In4, var(child(PID,PID2),true), global, Out),!. |
911 | | |
912 | | trans3(expr(Name), PID, In, In) :- |
913 | ? | eval(Name, PID, In, R), |
914 | | %print(evaluated_expr(PID,Name,R)),nl, |
915 | | ( false(R) -> fail; true ). |
916 | | |
917 | | trans3(assert(expr(Name)), PID, In, Out) :- |
918 | | eval(Name, PID, In, R), |
919 | | %% print(evaluated_expr(Name,R)),nl, |
920 | | ( false(R) |
921 | | -> define(In, var(sys(unsafe),true), global, Out) |
922 | | ; In=Out ). |
923 | | |
924 | | trans3(else, _, In, In). |
925 | | trans3(skip, _, In, In). |
926 | | |
927 | | % define locals |
928 | | trans3(def(Type,Name), PID, In, Out) :- |
929 | | get_init_value(def(Type,Name), Value, In, In2), |
930 | | ( Name = array(Name2,_) -> true; Name2 = Name ), |
931 | | ( Type = chan |
932 | | -> define(In2, var(chan(Name2),Value), PID, Out) |
933 | | ; define(In2, var(Name2,Value), PID, Out) ). |
934 | | |
935 | | % assign rendezvous-channel |
936 | | trans3(assign(array(Name,expr(K)),chan(0,_)), PID, In, Out) :- |
937 | | lookup(var(chan(Name)), PID, In, CIDList), |
938 | | eval(K, PID, In, K2), |
939 | | get_element(K2, CIDList, CID), |
940 | | store(In, chan(CID,[]), global, Out),!. |
941 | | trans3(assign(Name,chan(0,_)), PID, In, Out) :- |
942 | | lookup(var(chan(Name)), PID, In, CID), |
943 | | assign_channel_value(CID, [], In, Out),!. |
944 | | % assign channel |
945 | | trans3(assign(array(Name,expr(K)),chan(N,_)), PID, In, Out) :- |
946 | | lookup(var(chan(Name)), PID, In, CIDList), |
947 | | eval(K, PID, In, K2), |
948 | | get_element(K2, CIDList, CID), |
949 | | generate_chan(N, [empty], Value), |
950 | | store(In, chan(CID,Value), global, Out),!. |
951 | | trans3(assign(Name,chan(N,_)), PID, In, Out) :- |
952 | | lookup(var(chan(Name)), PID, In, CID), |
953 | | generate_chan(N, [empty], Value), |
954 | | assign_channel_value(CID, Value, In, Out),!. |
955 | | |
956 | | % assign channel to an existing CID |
957 | | trans3(assign(array(chan(Name),expr(K)),expr(chan(Name2))), PID, In, Out) :- |
958 | | lookup(var(chan(Name)), PID, In, CIDList), |
959 | | eval(K, PID, In, K2), |
960 | | lookup(var(chan(Name2)), PID, In, CID), |
961 | | set_element(K2, CIDList, CID, NewCIDList), |
962 | | define(In, var(chan(Name),NewCIDList), PID, Out),!. |
963 | | trans3(assign(chan(Name),expr(chan(Name2))), PID, In, Out) :- |
964 | | lookup(var(chan(Name2)), PID, In, CID), |
965 | | define(In, var(chan(Name),CID), PID, Out),!. |
966 | | |
967 | | trans3(assign(vt(Name,Type),Value), PID, In, Out) :- |
968 | ? | store(In, var(Name,Type,Value), PID, Out). |
969 | | |
970 | | trans3(inc(vt(Name,Type)), PID, In, Out) :- |
971 | | lookup(var(Name), PID, In, Value), |
972 | | R is Value+1, |
973 | ? | store(In, var(Name,Type,expr(R)), PID, Out). |
974 | | |
975 | | trans3(dec(vt(Name,Type)), PID, In, Out) :- |
976 | | lookup(var(Name), PID, In, Value), |
977 | | R is Value-1, |
978 | | store(In, var(Name,Type,expr(R)), PID, Out). |
979 | | |
980 | | /**************************************************************/ |
981 | | |
982 | | % assign Value to CID |
983 | | assign_channel_value(CID, Value, In, Out) :- |
984 | | number(CID), |
985 | | store(In, chan(CID,Value), global, Out),!. |
986 | | % assign Value to a list of CID's |
987 | | assign_channel_value([], _, In, In). |
988 | | assign_channel_value([H|Tail], Value, In, Out) :- |
989 | | store(In, chan(H,Value), global, In2), |
990 | | assign_channel_value(Tail,Value, In2, Out). |
991 | | |
992 | | % set_local_vars(NameList, ValueList, PID, PID2, In, Out) |
993 | | set_local_vars([], [], _, _, In, In). |
994 | | % H2 = single-chan or array-chan |
995 | | set_local_vars([def(chan,H1)|T1], [expr(H2)|T2], PID, PID2, In, Out) :- |
996 | | lookup(var(H2), PID, In, Value), |
997 | | define(In, var(chan(H1),Value), PID2, In2), |
998 | | set_local_vars(T1, T2, PID, PID2, In2, Out),!. |
999 | | set_local_vars([def(Type,H1)|T1], [expr(H2)|T2], PID, PID2, In, Out) :- |
1000 | | eval(H2,PID,In,V), |
1001 | | check_type(H1,Type,V,V2,In), |
1002 | | define(In, var(H1,V2), PID2, In2), |
1003 | | set_local_vars(T1, T2, PID, PID2, In2, Out). |
1004 | | |
1005 | | |
1006 | | % recv_eval(NameList, PID, In, Out, ValueList) |
1007 | | recv_eval([], _, In, In, []). |
1008 | | recv_eval([ctype(A)|T], PID, In, Out, [R|T2]) :- |
1009 | | check_type(recv(ctype(A)),mtype,R,ctype(A),In), |
1010 | | recv_eval(T, PID, In, Out, T2),!. |
1011 | | recv_eval([true|T], PID, In, Out, [R|T2]) :- |
1012 | | check_type(recv(true),bool,R,true,In), |
1013 | | recv_eval(T, PID, In, Out, T2),!. |
1014 | | recv_eval([false|T], PID, In, Out, [R|T2]) :- |
1015 | | check_type(recv(false),bool,R,false,In), |
1016 | | recv_eval(T, PID, In, Out, T2),!. |
1017 | | recv_eval([skip|T], PID, In, Out, [skip|T2]) :- |
1018 | | recv_eval(T, PID, In, Out, T2),!. |
1019 | | recv_eval([chan(A)|T], PID, In, Out, [CID|T2]) :- |
1020 | | define(In, var(chan(A),CID), PID, In2), |
1021 | | recv_eval(T, PID, In2, Out, T2),!. |
1022 | | recv_eval([A|T], PID, In, Out, [A|T2]) :- |
1023 | | number(A), |
1024 | | recv_eval(T, PID, In, Out, T2),!. |
1025 | | recv_eval([underscore|T], PID, In, Out, [_|T2]) :- |
1026 | | recv_eval(T, PID, In, Out, T2),!. |
1027 | | recv_eval([eval(Expr)|T], PID, In, Out, [R|T2]) :- |
1028 | | eval(Expr, PID, In, R), |
1029 | | %% print(evaluated_expr(Expr,R)),nl, |
1030 | | recv_eval(T, PID, In, Out, T2),!. |
1031 | | recv_eval([vt(A,AType)|T], PID, In, Out, [R|T2]) :- |
1032 | | atomic(A), |
1033 | | store(In, var(A,AType,expr(R)), PID, In2), |
1034 | | recv_eval(T, PID, In2, Out, T2). |
1035 | | |
1036 | | % else check |
1037 | | find_exec(Alt, PID, In) :- |
1038 | | member(A, Alt), |
1039 | | inst(A,Statement), |
1040 | ? | trans2(Statement, _, A, _, PID, _, In, _). |
1041 | | |
1042 | | % timeout check |
1043 | | find_exec(In) :- |
1044 | | lookup(proc(active(PID,_)), global, In, PC), |
1045 | | inst(PC,Statement), |
1046 | | Statement \= expr(timeout), |
1047 | | trans2(Statement, _, PC, _, PID, _, In, _). |
1048 | | %print(find_exec(PC,Statement)),nl. |
1049 | | |
1050 | | |
1051 | | delete([X|T],X,T). |
1052 | ? | delete([Y|T],X,[Y|DT]) :- delete(T,X,DT). |
1053 | | |
1054 | | /***************************************************************/ |
1055 | | |
1056 | | promela_property(env(Vars,_,_), '='('OrderedPair'(PID,Name),Value)) :- %var(key(Name,PID),Value)) :- |
1057 | | lookup3(key(Name,PID), Vars, Value). |
1058 | | promela_property(env(Vars,_,_), var(Name,Value)) :- |
1059 | | lookup3(Name, Vars, Value), Name \= key(_,_). |
1060 | | promela_property(env(_,Procs,_), proc(active(PID,Name),PC)) :- |
1061 | | lookup3(active(PID,Name), Procs, PC). |
1062 | | promela_property(env(_,_,Chans), chan(Id,Value)) :- |
1063 | | Chans \= [], |
1064 | | lookup3(Id, Chans, Value). |
1065 | | |
1066 | | promela_property(env(_,Procs,_), active_proctypes(N)) :- |
1067 | | avl_size(Procs,N). |
1068 | | promela_property(env(Vars,_,_), unsafe) :- |
1069 | | lookup2(sys(unsafe), Vars, Value), |
1070 | | ( Value == true |
1071 | | -> true |
1072 | | ; fail ). |
1073 | | |
1074 | | % debugging: |
1075 | | %promela_property(env(Vars,_,_), true) :- |
1076 | | % avl_to_list(Vars,List), |
1077 | | % print(vars(List)),nl. |
1078 | | |
1079 | | %promela_property(env(_,Procs,_), true) :- |
1080 | | % avl_to_list(Procs,List), |
1081 | | % print(procs(List)),nl. |
1082 | | |
1083 | | %promela_property(env(_,_,Chans), true) :- |
1084 | | % avl_to_list(Chans,List), |
1085 | | % print(chans(List)),nl. |
1086 | | |
1087 | | %promela_property(env(Vars,Procs,Chans), 0) :- |
1088 | | % print('Vars: '),portray_avl(Vars),nl, |
1089 | | % print('Procs: '),portray_avl(Procs),nl, |
1090 | | % print('Chans: '),portray_avl(Chans),nl,fail. |