promela_tools

call_promela_parser(MCH,PL) :-
    (call_promela_parser2(MCH,PL) -> Res=ok; Res=fail),
    delete_file(MCH),
    Res=ok.

call_promela_parser2(MCH,PL) :-
    absolute_file_name(prob_lib('.'), LibDir),
    atom_concat('-Djava.library.path=', LibDir, JLibpath),
   
    absolute_file_name(prob_lib('Promela.jar'),Jar),
    once(absolute_file_name(path(java),
    JavaCmd,
    [access(exist),extensions(['.exe','']),solutions(all),file_errors(fail)])),
   
    replace_windows_path_backslashes(JavaCmd,JavaCmdW),
    replace_windows_path_backslashes(Jar,JarW),
    replace_windows_path_backslashes(MCH,MCHW),
   
    process_create(JavaCmdW,
    %['-jar',JarW,MCHW],
    [JLibpath,'-jar',JarW,'-ltl',MCHW],
    [process(Java),stdout(pipe(JStdout))]),
   
    read_all(JStdout,Text),
    process_wait(Java,JExit),
    (JExit=exit(0) -> true;
    (name(T,Text),JExit=exit(1) ->
    throw(parse_error(T));
    add_error(ltl,'Error while parsing predicates',Text),fail)),
    atom_chars(MCH,FilenameM),append(Core,['.','m','c','h'],FilenameM),
    append(Core,['.','p','l'],FilenameP),atom_chars(PL,FilenameP).

eval_promela(Expr, PID, Env, Value) :- eval(Expr,PID,Env,Value).

load_promela(Filename,Term) :-
    open(Filename, read, S),
    read(S,Term),
    close(S).

parse_promela_strings(ExprStrings,PredStrings,[],PromPreds) :-
    ( ExprStrings = [_|_] ->
    throw(parse_error('Unsupported expressions in Promela mode!'))
    ; true),
    write_string_to_file(MMachine,PredStrings),
    call_promela_parser(MMachine,PMachine),
    load_promela(PMachine,PromPreds),
    delete_file(PMachine).

print_string([],_).

print_string([C|Rest],S) :- put_code(S,C),print_string(Rest,S).

print_string_list([],_).

print_string_list([H|T],S) :-
    % ascii-nr 44 is ','.
    append(H,[44],H2),
    print_string(H2,S),
    print_string_list(T,S).

read_all(S,Text) :- read_line(S,Line),
    (Line=end_of_file -> Text="",close(S);
    append(Line,"\n",Line1),
    append(Line1,RText,Text),
    read_all(S,RText)).

replace_string_backslashes([],[]).

replace_string_backslashes([C|OldRest],[N|NewRest]) :-
    ( C=92 /* backslash */ ->
    N=47 /* forward slash */
    ;
    N=C ),
    replace_string_backslashes(OldRest,NewRest).

replace_windows_path_backslashes(Old,New) :-
    ( host_platform(windows) ->
    name(Old,OldStr),
    replace_string_backslashes(OldStr,NewStr),
    name(New,NewStr)
    ;
    Old=New).

write_string_to_file(Filename,Machine) :-
    open(temp('ltl_prob.mch'),write,S,[if_exists(generate_unique_name)]),
    stream_property(S, file_name(Filename)),
    print_string_list(Machine,S),
    close(S).