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		% LTL model checking with promela
6
7		:- module(promela_tools,[parse_promela_strings/4,eval_promela/4]).
8
9		:- use_module(library(file_systems)).
10		:- use_module(library(process)).
11
12		:- use_module(h_int, [eval/4]).
13		:- use_module(probsrc(tools),[host_platform/1]).
14		:- use_module(probsrc(error_manager)).
15
16		:- use_module(probsrc(module_information)).
17		:- module_info(group,promela).
18		:- module_info(description,'This module contains helper predicates for the Promela extension.').
19
20		eval_promela(Expr, PID, Env, Value) :- eval(Expr,PID,Env,Value).
21
22		parse_promela_strings(ExprStrings,PredStrings,[],PromPreds) :-
23		( ExprStrings = [_|_] ->
24		throw(parse_error('Unsupported expressions in Promela mode!'))
25		; true),
26		write_string_to_file(MMachine,PredStrings),
27		call_promela_parser(MMachine,PMachine),
28		load_promela(PMachine,PromPreds),
29		delete_file(PMachine).
30
31		write_string_to_file(Filename,Machine) :-
32		open(temp('ltl_prob.mch'),write,S,[if_exists(generate_unique_name)]),
33		stream_property(S, file_name(Filename)),
34		print_string_list(Machine,S),
35		close(S).
36
37		print_string([],_).
38		print_string([C|Rest],S) :- put_code(S,C),print_string(Rest,S).
39		print_string_list([],_).
40		print_string_list([H|T],S) :-
41		% ascii-nr 44 is ','.
42		append(H,[44],H2),
43		print_string(H2,S),
44		print_string_list(T,S).
45
46		load_promela(Filename,Term) :-
47		open(Filename, read, S),
48		read(S,Term),
49		close(S).
50
51		call_promela_parser(MCH,PL) :-
52		(call_promela_parser2(MCH,PL) -> Res=ok; Res=fail),
53		delete_file(MCH),
54		Res=ok.
55		call_promela_parser2(MCH,PL) :-
56		absolute_file_name(prob_lib('.'), LibDir),
57		atom_concat('-Djava.library.path=', LibDir, JLibpath),
58
59		absolute_file_name(prob_lib('Promela.jar'),Jar),
60		once(absolute_file_name(path(java),
61		JavaCmd,
62		[access(exist),extensions(['.exe','']),solutions(all),file_errors(fail)])),
63
64		replace_windows_path_backslashes(JavaCmd,JavaCmdW),
65		replace_windows_path_backslashes(Jar,JarW),
66		replace_windows_path_backslashes(MCH,MCHW),
67
68		process_create(JavaCmdW,
69		%['-jar',JarW,MCHW],
70		[JLibpath,'-jar',JarW,'-ltl',MCHW],
71		[process(Java),stdout(pipe(JStdout))]),
72
73		read_all(JStdout,Text),
74		process_wait(Java,JExit),
75		(JExit=exit(0) -> true;
76		(name(T,Text),JExit=exit(1) ->
77		raise_exception(parse_error(T));
78		add_error(ltl,'Error while parsing predicates',Text),fail)),
79		atom_chars(MCH,FilenameM),append(Core,['.','m','c','h'],FilenameM),
80		append(Core,['.','p','l'],FilenameP),atom_chars(PL,FilenameP).
81
82		/* replace backslashes by forward slashes in atoms, only under windows */
83		replace_windows_path_backslashes(Old,New) :-
84		( host_platform(windows) ->
85		name(Old,OldStr),
86		replace_string_backslashes(OldStr,NewStr),
87		name(New,NewStr)
88		; otherwise ->
89		Old=New).
90
91		% copy from parsercall:
92		replace_string_backslashes([],[]).
93		replace_string_backslashes([C|OldRest],[N|NewRest]) :-
94		( C=92 /* backslash */ ->
95		N=47 /* forward slash */
96		; otherwise ->
97		N=C ),
98		replace_string_backslashes(OldRest,NewRest).
99
100		read_all(S,Text) :- read_line(S,Line),
101		(Line=end_of_file -> Text="",close(S);
102		append(Line,"\n",Line1),
103		append(Line1,RText,Text),
104		read_all(S,RText)).