1		% (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(promela_ncprinter, [promela_save_as_neverclaim/2]).
6
7		:- use_module(library(avl)).
8
9		:- use_module(probsrc(tools)).
10		:- use_module(probsrc(state_space)).
11
12		:- use_module(probsrc(module_information)).
13		:- module_info(group,promela).
14		:- module_info(description,'Promela extension: This module contains predicates to print never claims.').
15
16		promela_save_as_neverclaim(FileIn, FileOut) :-
17		print_message('Saving State Space to never-claim file: '),
18		print_message(FileOut),
19		tell(FileOut),
20		print_transition_header(FileIn),
21		(gen_process -> true; true),
22		told,
23		print_message('Finished').
24
25		%gen_process :-
26		% print_transition_header,fail.
27
28		gen_process :-
29		visited_expression(NodeA,EnvA),
30		print_process_declaration_header(NodeA),
31		%retractall(selectsymbol),
32		(transition(NodeA,Trans,NodeB)
33		-> (check_stat(NodeA,EnvA,Trans,NodeB)
34		-> true
35		; check_env(EnvA,NodeB) )
36		/*; (not_all_transitions_added(NodeIDs)
37		-> print_open_detail(NodeIDs)
38		; print_stop_detail(NodeIDs))),*/
39		; print_end),
40		print_process_declaration_footer(NodeA), fail.
41		gen_process :-
42		print_transition_footer.
43
44
45		print_transition_header(FileIn) :-
46		print('#include "'),print(FileIn),print('"'),nl,nl,
47		print('never {'),nl.
48
49		print_transition_footer :-
50		print('}'),nl.
51
52		print_process_declaration_header(ID) :-
53		print('N'), print(ID), print(':'),nl.
54		%print(' do'),nl.
55
56		print_process_declaration_footer(_) :-
57		true.
58		%print(' od;'),nl.
59
60		check_stat(_NodeA, EnvA, Trans, NodeB) :-
61		print(' assert('),
62		Trans = io([Statement], proc(PID,_Proc), _Span),
63		analyse_stat(Statement, PID, EnvA),
64		print(') -> goto N'),print(NodeB),print(';'),nl.
65
66		analyse_stat(assign(vt(Name,Type),Value), PID, In) :-
67		In = env(Vars,_,_),
68		% check if variable is global
69		( avl_fetch(key(Name,PID),Vars,_) -> fail; true ),
70		print_name(Name,PID,In),
71		print(' == '),
72		print_value(Name,Type,Value,PID,In).
73
74		print_name(Name, PID, In) :-
75		( Name = record(Name2)
76		-> print_record(Name2,PID,In)
77		; Name = array(Name2,K)
78		-> print_array(Name2,K,PID,In)
79		; print(Name) ).
80
81		print_record([], _, _).
82		print_record([H|T], PID, In) :-
83		print_name(H,PID,In),
84		print('.'),
85		print_record(T,PID,In).
86
87		:- use_module(h_int).
88		print_array(Name, expr(K), PID, In) :-
89		h_int:eval(K,PID,In,R),
90		print(Name),
91		print('['),
92		print(R),
93		print(']').
94
95		print_value(Name, Type, expr(V), PID, In) :-
96		h_int:eval(V,PID,In,V1),
97		%%print(nt(Name,Type,V1)),nl,
98		h_int:check_type(Name,Type,V1,V2,In),
99		( V2 = ctype(V3) -> true; V3 = V2),
100		print(V3).
101
102		print_end :-
103		print(' do'),nl,
104		print(' :: true'),nl,
105		print(' od;'),nl.
106
107		%***********************************************%
108
109		check_env(EnvA, NodeB) :-
110		%print('('),
111		analyse_env(EnvA),
112		print(') -> goto N'),
113		print(NodeB),
114		print(';'),nl.
115
116		analyse_env(env(VarsA,_,_)) :-
117		avl_member(Key, VarsA, Val),
118		Key \= key(_,_), Key \= type(_), Key \= sys(_),
119		Key \= child(_,_), Key \= chan(_),
120		Val \= [_|_],
121		print(Key),
122		print(' == '),
123		print_env_value(Val),
124		print(' && '),
125		fail.
126
127		analyse_env(_) :-
128		print('true').
129
130		print_env_value(V) :-
131		number(V),
132		print(V),!.
133
134		print_env_value(ctype(V)) :-
135		print(V).
136
137		%print_goto(NodeB) :-
138		% print(' '),
139		% print('true -> goto N'),print(NodeB),print(';'),nl.
140