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.