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.