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