parsercall

add_acc_string([],L,R) :- !, L=R.

add_acc_string(Acc,[string_codes(Str)|T],T) :- reverse(Acc,Str).

all_older([],_).

all_older([File|Rest],ProbTime) :-
    (file_exists(File)
    -> file_property(File, modify_timestamp, BTime),
    debug_format(9,' Subsidiary File Timestamp: ~w:~w~n',[File,BTime]),
    ( BTime < ProbTime -> true
    ; format('File has changed : ~w : ~w~n',[File,BTime]),
    fail )
    ; virtual_dsl_file(File) -> debug_format(9,'Virtual file generated by DSL translator: ~w~n',[File])
    ; debug_format(20,'File does not exist anymore: ~w; calling parser.~n',[File]),fail),
    all_older(Rest,ProbTime).

alloy_pl_filename(AlloyFile,BFile) :- atom_codes(AlloyFile,BasenameC),
    append(BasenameC,".pl",NewC),
    atom_codes(BFile,NewC),!.

alloy_pl_filename(Filename, BFile) :-
    add_failed_call_error(alloy_pl_filename(Filename,BFile)),fail.

analyse_java_error_msg(ErrMsgCodes) :-
    append([_,"java.lang.OutOfMemoryError",_],ErrMsgCodes),!,
    % a typical message contains: Exception in thread "main" java.lang.OutOfMemoryError: GC overhead limit exceeded
    % or: Exception in ...: Java heap space
    print_hint('Try increasing memory for Java by setting the JVM_PARSER_HEAP_MB preference.'),
    print_hint('You can also provide custom JVM arguments using the JVM_PARSER_ARGS preference.').

analyse_java_error_msg(ErrMsgCodes) :-
    append([_,"java.lang.StackOverflowError",_],ErrMsgCodes),!,
    print_hint('Try increasing stack size for Java using the JVM_PARSER_ARGS preference (e.g.,"-Xss10m").').

analyse_java_error_msg(_).

call_alloy2pl_parser(AlloyFile,BFile) :-
    alloy_pl_filename(AlloyFile,BFile),
    call_alloy2pl_parser_aux(AlloyFile,'alloy2b.jar',BFile).

call_alloy2pl_parser_aux(AlloyFile,JARFile,PrologBFile) :-
    compilation_not_needed(AlloyFile,PrologBFile,JARFile),!.

call_alloy2pl_parser_aux(AlloyFile,JARFile,PrologBFile) :-
    (file_exists(PrologBFile) -> delete_file(PrologBFile) ; true), % TODO: only delete generated files
    replace_windows_path_backslashes(PrologBFile,BFileW),
    call_jar_parser(AlloyFile,JARFile,['-toProlog',BFileW],alloy2b).

call_console_parser(Filename, ProB) :-
    profile_single_call('$parsing',unknown,parsercall:call_console_parser2(Filename, ProB)).

call_console_parser2(Filename, ProB) :-
    update_jvm_parser_preferences,
    get_console_parser(Stream,Out,Err),
   
    % path to the .prob file
    replace_windows_path_backslashes(ProB,ProBW),
    % the input file
    replace_windows_path_backslashes(Filename,FilenameW),
    % call PREPL 'machine' command
    debug_format(4,'PREPL command: machine~n~w~n~w~n',[FilenameW,ProBW]),
    format(Stream,'machine~n~w~n~w~n',[FilenameW,ProBW]), % tell parser to write output to ProBW .prob file
    flush_output(Stream),
   
    %% WARNING: if the java parser writes too much output on the out stream it will block
    %% until its output is read and we have a deadlock !
    %% hence we use safe_polling_read_line
    safe_polling_read_line(Stream,Out,Err,1,[],Term),
   
    display_pending_outputs(Out,user_output),
    handle_console_parser_result(Term,Err).

call_fuzz_parser(TexFile,FuzzFile) :-
    get_command_in_lib(fuzz,FuzzCmd),
    absolute_file_name(prob_lib('fuzzlib'),FUZZLIB), % TO DO: windows
    fuzz_filename(TexFile,FuzzFile),
    % fuzz options:
    % -d Allow use before definition
    % -l Lisp-style echoing of input
    % -p file Use in place of standard prelude
    debug_format(19,'Fuzz: running ~w -d -l with library ~w on ~w~n',[FuzzCmd,FUZZLIB,TexFile]),
    (file_exists(FUZZLIB)
    -> my_system_call5(FuzzCmd,['-d', '-l', '-p', file(FUZZLIB), file(TexFile)],call_fuzz_parser,Text,_ErrText)
    ; my_system_call5(FuzzCmd,['-d', '-l', file(TexFile)],call_fuzz_parser,Text,_ErrText)
    ),
    format('Writing fuzz AST to ~s~n',[FuzzFile]),
    open(FuzzFile,write,Stream),
    call_cleanup(format(Stream,'~s~n',[Text]), close(Stream)).

call_jar_parser(PMLFile,JARFile,Args,ParserName) :-
    get_java_command_path(JavaCmdW),
    replace_windows_path_backslashes(PMLFile,PMLFileW),
    phrase(jvm_options, XOpts),
    absolute_file_name(prob_lib(JARFile),FullJAR),
    append(XOpts,['-jar',FullJAR,PMLFileW|Args],FullArgs),
    %format('Java: ~w, Parser: ~w, Args: ~w~n',[JavaCmdW,ParserName,FullArgs]),
    my_system_call(JavaCmdW, FullArgs,ParserName).

call_ltl_parser(Formulas, CtlOrLtl, Result) :-
    get_ltl_lang_spec(LangSpec),
    maplist(parse_temporal_formula(CtlOrLtl,LangSpec),Formulas,Result).

call_tla2b_parser(TLAFile) :-
    get_java_command_path(JavaCmdW),
    replace_windows_path_backslashes(TLAFile,TLAFileW),
    phrase(jvm_options, XOpts),
    absolute_file_name(prob_lib('TLA2B.jar'),TLA2BJAR),
    append(XOpts,['-jar',file(TLA2BJAR),file(TLAFileW)],FullArgs),
    % other possible options -verbose -version -config FILE
    (my_system_call(JavaCmdW, FullArgs,tla2b_parser)
    -> true
    ; \+ file_exists(TLA2BJAR),
    print_error('Be sure to download TLA2B.jar from https://stups.hhu-hosting.de/downloads/prob/tcltk/jars/,'),
    print_error('and put it into the ProB lib/ directory.'),
    fail
).

check_java_version(VersionCheckResult,ResultStatus) :- get_java_fullversion(Version),!,
    check_java_version_aux(Version,VersionCheckResult,ResultStatus).

check_java_version(VersionCheckResult,error) :- get_java_command_for_parser(java_jar(JavaCmdW,JarPathW)),!,
    ajoin(['*** Unable to launch java command: ',JavaCmdW,' (classpath: ',JarPathW,')!'],VersionCheckResult).

check_java_version('*** Unable to launch Java or get path to java command!',error). % should not happen

check_java_version_aux(VersionCodes,VersionCheckResult,ResultStatus) :-
    get_java_fullversion_numbers(VersionCodes,V1,V2,V3Atom),!,
    check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,ResultStatus).

check_java_version_aux(VersionCodes,VersionCheckResult,error) :-
    atom_codes(VersionA,VersionCodes),
    ajoin(['*** Unable to identify Java version number: ',VersionA, ' !'],VersionCheckResult).

check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,compatible) :- java_version_ok_for_parser(V1,V2,V3Atom),
    get_java_version(_),!, % if get_java_version fails, this is an indication that Java not fully installed with admin rights
    ajoin(['Java is correctly installed and version ',V1,'.',V2,'.',V3Atom,
    ' is compatible with ProB requirements (>= 1.7).'],VersionCheckResult).

check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,error) :- java_version_ok_for_parser(V1,V2,V3Atom),!,
    ajoin(['*** Java version ',V1,'.',V2,'.',V3Atom,
    ' is compatible with ProB requirements (>= 1.7) ',
    'but does not seem to be correctly installed: reinstall Java with admin rights!'],VersionCheckResult).

check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,incompatible) :-
    get_java_version(_),!,
    ajoin(['*** Java is correctly installed but version ',V1,'.',V2,'.',V3Atom,
    ' is *not* compatible with ProB requirements (>= 1.7)!'],VersionCheckResult).

check_java_version_aux2(V1,V2,V3Atom,VersionCheckResult,error) :-
    ajoin(['*** Java is not correctly installed and version ',V1,'.',V2,'.',V3Atom,
    ' is *not* compatible with ProB requirements (>= 1.7)!'],VersionCheckResult).

check_prob_file_first_code(Code,Stream,ProBFile,Options) :-
    (valid_start_code(Code) -> true
    ; fastrw_start_code(Code)
    -> close(Stream),
    % we need to do: open(ProBFile,read,S,[type(binary)]),
    (member(check_if_up_to_date(_,_),Options)
    -> add_warning(parsercall,'Re-running parser as .prob file seems to be in new fast-rw format: ',ProBFile)
    ; add_error(parsercall,'Cannot load .prob file; it seems to be in new fast-rw format:',ProBFile)
    ),
    fail
    ; add_message(parsercall,'Strange start character code in .prob file: ',[Code]) % probably syntax error will happen
).

check_prob_file_not_empty(Stream,Size,ProBFile,Options) :- Size=<0,!,
    close(Stream),
    (member(check_if_up_to_date(_,_),Options)
    -> add_warning(parsercall,'Re-running parser as .prob file is empty: ',ProBFile)
    % due to possible crash or CTRL-C of previous parser run
    ; add_internal_error('Generated .prob file is empty',ProBFile)
    ),fail.

check_prob_file_not_empty(_,_,_,_).

check_version_and_read_machine(Filename,ProBFile, ProbTime, Version, GitSha, Machine,Options) :-
    (Version='$UNKNOWN'
    -> add_warning(parsercall,'*** Unknown parser version number. Trying to load parsed file: ',ProBFile)
    /* keep CheckVersionNr as variable */
    ; CheckVersionNr=Version),
    read_machine_term_from_file(ProBFile,prob_parser_version(CheckVersionNr,GitSha),
    [check_if_up_to_date(Filename,ProbTime)|Options],Machine).

cleanup_newlines([],[]).

cleanup_newlines([H|T],CleanCodes) :- crlf(H),!,
    % this could also be inside a multi-line string; the string will be modified by this conversion
    CleanCodes=[8232|TC], % 8232 \x2028 is Unicode line separator
    cleanup_newlines(T,TC).

cleanup_newlines([H|T],[H|R]) :- cleanup_newlines(T,R).

clear_old_console_parsers :-
    retract(java_parser_process(PID,_,_,_)),
    parser_process_release(PID),
    fail.

clear_old_console_parsers.

compilation_not_needed(BaseFile,DerivedFile,LibraryFile) :-
    file_exists(BaseFile),
    file_property(BaseFile, modify_timestamp, BTime),
    %system:datime(BTime,datime(_Year,Month,Day,Hour,Min,Sec)), format('~w modfied on ~w/~w at ~w:~w (~w sec)~n',[BaseFile,Day,Month,Hour,Min,Sec]),
    file_exists(DerivedFile),
    file_property(DerivedFile, modify_timestamp, DTime),
    DTime > BTime,
    absolute_file_name(prob_lib(LibraryFile),FullLibFile),
    (file_exists(FullLibFile)
    -> file_property(FullLibFile, modify_timestamp, LibTime),
    DTime > LibTime % check that file was generated by this library (hopefully); ideally we should put version numbers into the DerivedFiles
    ; true % Jar/command not available anyway; use the derived file
).

connect_to_console_parser_on_port(PortTerm,PID,Out,Err,Stream) :-
    catch(
    socket_client_open('':PortTerm, Stream, [type(text),encoding(utf8)]),
    Exc, %error(system_error,system_error(E)), % SPIO_E_NET_HOST_NOT_FOUND
    (
    ajoin(['Exception while opening parser socket on port ', PortTerm,
    ' (possibly an error occurred during startup of the parser): '],Msg),
    add_internal_error(Msg,Exc),
    % e.g., not enough memory to start parser and wait for socket connection
    read_lines_and_add_as_error(Err), % try and read additional info;
    % if we set the stack size to be very small (-Xss20k) we get: Error: Could not create the Java Virtual Machine
    fail
    )),
    assertz(java_parser_process(PID,Stream,Out,Err)).

connect_to_external_console_parser_on_port(PortNumber) :-
    clear_old_console_parsers,
    format('Trying to connect to external parser on port ~w~n',[PortNumber]),
    Out=user_input, Err=user_input,
    (connect_to_console_parser_on_port(PortNumber,external_process,Out,Err,_)
    -> format('Connected to parser on port ~w~n',[PortNumber])
    ; add_error(parsercall,'Could not connect to parser on port:',PortNumber)
).

console_parser_jar_available_in_lib :-
    runtime_application_path(P),
    atom_concat(P,'/lib/probcliparser.jar',ConParser),
    file_exists(ConParser).

count_offset([],Line,Col,Line,Col).

count_offset(Codes,L,_ColOffset,Line,Col) :- newline(Codes,T),!,
    L1 is L+1,
    count_offset(T,L1,0,Line,Col).

count_offset([_|T],L,ColOffset,Line,Col) :- C1 is ColOffset+1,
    count_offset(T,L,C1,Line,Col).

count_template_offset(template_codes(Codes,_StartOffset,AdditionalChars,_),L,C,LineOffset,C3) :-
    count_offset(Codes,L,C,LineOffset,ColOffset),
    C3 is ColOffset+AdditionalChars. % e.g., 3 for ${.}

count_template_offset(string_codes(Codes),L,C,LineOffset,ColOffset) :-
    count_offset(Codes,L,C,LineOffset,ColOffset).

create_to_string_conversion(RawExpr,Pos,Options,
    external_function_call_auto(Pos,'STRING_PADLEFT',[RawStrExpr,Len,Char])) :-
    select(template_width(pad_string(PadChar),Nr),Options,RestOpts),!,
    create_to_string_conversion(RawExpr,Pos,RestOpts,RawStrExpr),
    Char = string(Pos,PadChar),
    Len = integer(Pos,Nr).

create_to_string_conversion(RawExpr,Pos,Options,RawStrExpr) :-
    is_definitely_string(RawExpr),!,
    (Options=[] -> true
    ; add_warning(string_template,'Ignoring options in string template (already a string): ',Options, Pos)),
    RawStrExpr=RawExpr.

create_to_string_conversion(RawExpr,Pos,Options,external_function_call_auto(Pos,'REAL_TO_DEC_STRING',[RawExpr,Prec])) :-
    select_option(template_width(float_fixed_point,Nr),Options,Pos),!,
    Prec = integer(Pos,Nr).

create_to_string_conversion(RawExpr,Pos,Options,external_function_call_auto(Pos,'INT_TO_DEC_STRING',[RawExpr,Prec])) :-
    select_option(template_width(integer_decimal_string,Nr),Options,Pos),!,
    Prec = integer(Pos,Nr).

create_to_string_conversion(RawExpr,Pos,Options,external_function_call_auto(Pos,'TO_STRING_UNICODE',[RawExpr])) :-
    select_option(unicode,Options,Pos),!. % TODO use a TO_STRING function with options list

create_to_string_conversion(RawExpr,Pos,_Options,external_function_call_auto(Pos,'TO_STRING',[RawExpr])).

crlf(10).

crlf(13).

debug_print_system_call(Command,Args) :-
    (debug_mode(off) -> true ; print_system_call(Command,Args)).

deregister_parsing_call_back :-
    retractall(prob2_call_back_available(_)).

digit(Nr) --> [X], {X >= 48, X=<57, Nr is X-48}.

digit_code_2_int(X,Val) :- X >= 48, X =< 57, Val is X - 48.

digits(MinusNr,Len) --> "-",!, digit(X), digits2(X,Nr,2,Len), {MinusNr is -Nr}.

digits(Nr,Len) --> digit(X), digits2(X,Nr,1,Len).

digits2(X,Nr,AccLen,Len) --> digit(Y), !, {XY is X*10+Y, A1 is AccLen+1}, digits2(XY,Nr,A1,Len).

digits2(X,X,Len,Len) --> "".

display_pending_outputs(OutStream,ToStream) :- stream_ready_to_read(OutStream,0), !, read_line(OutStream,Line),
    (Line=end_of_file -> true
    ; format(ToStream,' =parser-output=> ~s~n',[Line]),
    display_pending_outputs(OutStream,ToStream)).

display_pending_outputs(_,_).

dont_need_compilation(Filename,ProB,Machine,LoadResult,Options) :-
    file_exists(Filename),
    catch( ( get_parser_version(Version,GitSha),
    file_property(Filename, modify_timestamp, BTime),
    debug_format(9, 'Parser Version: ~w, Filename Timestamp: ~w : ~w~n',[Version,Filename,BTime]),
    file_exists(ProB), % the .prob file exists
    file_property(ProB, modify_timestamp, ProbTime),
    debug_format(9, '.prob Timestamp: ~w : ~w~n',[ProB,ProbTime]),
    % print(time_stamps(ProB,ProbTime,Filename,BTime)),nl,
    BTime < ProbTime, % .mch file is older than .prob file
    file_property(ProB,size_in_bytes,Size),
    (Size>0 -> true
    ; debug_mode(on),
    add_message(parsercall,'.prob file is empty; parsing again',ProB),
    % possibly due to crash or error before, cf second run of test 254
    fail),
    check_version_and_read_machine(Filename,ProB, ProbTime, Version, GitSha, Machine,Options),
    %Machine = complete_machine(_,_,_),
    LoadResult = loaded),
    error(A,B),
    (debug_println(9,error(A,B)),
    (A=resource_error(memory)
    -> add_error(load_b_machine,'Insufficient memory to load file.\nTry starting up ProB with more memory\n (e.g., setting GLOBALSTKSIZE=500M before starting ProB).'),
    LoadResult=A
    ; fail))).

ensure_console_parser_launched :-
    catch(parse_formula("1",_), E, (
    add_internal_error('Cannot launch console parser (probcliparser.jar)',E),
    fail
)).

epi(Row,Col,Filename) --> " ",!,epi(Row,Col,Filename).

epi(Row,Col,Filename) --> "[", epi_number(Row),",",epi_number(Col),"]",
    (epi_filename(Filename) -> [] ; {Filename=unknown}).

epi_filename(F) --> " in file: ",!,epi_path2(Chars),{safe_name(F,Chars)}.

epi_filename(F) --> [_], epi_filename(F).

epi_number(N) --> epi_numbers(Chars),{safe_number_codes(N,Chars)}.

epi_numbers([C|Rest]) --> [C],{is_number(C)},epi_numbers2(Rest).

epi_numbers2([C|Rest]) --> [C],{is_number(C),!},epi_numbers2(Rest).

epi_numbers2("") --> !.

epi_path2([C|Rest]) --> [C],!,epi_path2(Rest). % assume everything until the end is a filename

epi_path2([]) --> [].

extract_line_col_for_b_parser(Span,Line,Col1) :-
    extract_line_col(Span,Line,Col,_EndLine,_EndCol),
    Col1 is Col+1. % the BParser starts column numbering at 1

fastrw_start_code(0'D). % typical start DSparser_version

findall_definitions(DefList) :-
    findall(def(Name,Type,Arity),(b_get_definition(Name,Type,Args,_,_),length(Args,Arity)),DefList).

fuzz_filename(TexFile,FuzzFile) :-
    split_filename(TexFile,Basename,_Extension),
    atom_chars(Basename,BasenameC),
    append(BasenameC,['.','f','u','z','z'],CC),
    atom_chars(FuzzFile,CC),!.

fuzz_filename(TexFile, FuzzFile) :-
    add_failed_call_error(fuzz_filename(TexFile,FuzzFile)),fail.

generate_conc_expr([],Pos,string(Pos,'')).

generate_conc_expr([OneEl],_,Res) :- !, Res = OneEl. % no need to concatenate

generate_conc_expr(List,Pos,general_concat(Pos,sequence_extension(Pos,List))).

get_binary_extensions(List) :-
    host_platform(windows),!, List=['.exe','']. % will backtrack in get_command_in_lib

get_binary_extensions(['']).

get_command_in_lib(Name,Command) :-
    get_binary_extensions(Extensions),
    absolute_file_name(prob_lib(Name),
    Command,
    [access(exist),extensions(Extensions),solutions(all),file_errors(fail)]).

get_compound_exceptions([],_) --> [].

get_compound_exceptions([Err1|T],ErrStream) -->
    {handle_and_catch(Err1,ErrStream,ParseErrors) },
    ParseErrors,
    get_compound_exceptions(T,ErrStream).

get_console_parser(Stream,Out,Err) :-
    java_parser_process(PID,Stream,Out,Err),
    % On SICStus, calling is_process seams to be unreliable (if the process has crashed)
    % and process_wait does not always work either,
    % so first check if in and output streams are still available.
    \+ at_end_of_stream(Stream),
    % On SWI, at_end_of_stream doesn't detect broken pipes,
    % so additionally also check that the process has not exited/crashed.
    process_wait(PID,timeout,[timeout(0)]),
    !,
    (at_end_of_stream(Err)
    -> add_error(parsercall,'Java process not running'),
    read_lines_and_add_as_error(Stream)
    ; true).

get_console_parser(Stream,Out,Err) :-
    clear_old_console_parsers,
    get_java_command_for_parser(ParserCmd),
    phrase(parser_command_args(ParserCmd, NativeCmd), FullArgs),
    debug_println(19,launching_java_console_parser(NativeCmd,FullArgs)),
    debug_print_system_call(NativeCmd,FullArgs),
    system_call_keep_open(NativeCmd,FullArgs,PID,_In,Out,Err,[]), % note: if probcliparser.jar does not exist we will not yet get an error here !
    debug_println(9,java_console_parser_launched(PID)),
    % read first line to get port number
    safe_read_line(Out,Err,1,[],PortTerm),
    connect_to_console_parser_on_port(PortTerm,PID,Out,Err,Stream),
    !.

get_console_parser(_,_,_) :- missing_parser_diagnostics, fail.

get_definitions(L) :- b_or_z_mode, b_machine_is_loaded,!, findall_definitions(L).

get_definitions([]).

get_error_position_from_codes([97,116,32,108,105,110,101,32|Tail],lineCol(Line,Col)) :- % "at line "
    epi_number(Line,Tail,RestTail),
    (RestTail = [32,99,111,108,117,109,110,32|Tail2], % "column "
    epi_number(Col,Tail2,_) -> true
    ; Col=0).

get_error_position_from_codes([_|T],Pos) :- get_error_position_from_codes(T,Pos).

get_error_position_from_term(alloy2b,Term,Pos) :- atom(Term),
    atom_codes(Term,Codes), get_error_position_from_codes(Codes,Pos).

get_extra_args_list(ExtraArgs) :-
    get_preference(jvm_parser_additional_args,ExtraArgsStr),
    ExtraArgsStr \= '',
    atom_codes(ExtraArgsStr,C),
    split_chars(C," ",CA),
    maplist(atom_codes,ExtraArgs,CA).

get_java_command_for_parser(native(GraalNativeCmd)) :-
    (parser_location(GraalNativeCmd)
    -> get_tail_filename(GraalNativeCmd,'cliparser'),
    (file_exists(GraalNativeCmd) -> true
    ; add_warning(parsercall,'Path to parser points to non-existant compiled GraalVM binary: ',GraalNativeCmd)
    )
    ; fail, % comment out fail to enable auto-detection of cliparser in lib folder
    library_abs_name('cliparser',GraalNativeCmd),
    file_exists(GraalNativeCmd)
    ),
    format('Using GRAAL native parser at ~w~n',[GraalNativeCmd]),
    !.

get_java_command_for_parser(java_jar(JavaCmdW,JarPathW)) :-
    (parser_location(JarPath) -> true ; library_abs_name('probcliparser.jar',JarPath)),
    get_java_command_path(JavaCmdW),
    replace_windows_path_backslashes(JarPath,JarPathW).

get_java_command_path(JavaCmdW) :-
    %host_platform(darwin)
    get_preference(path_to_java,X),
    debug_println(8,path_to_java_preference(X)),
    (X=''
    ; preference_default_value(path_to_java,Default), debug_println(8,default(Default)),
    Default=X
    ),
    % only try this when the Java path has not been set explicitly
    % on Mac: /usr/bin/java exists even when Java not installed ! it is a fake java command that launches a dialog
    absolute_file_name(path(java),
    JavaCmd,
    [access(exist),extensions(['.exe','']),solutions(all),file_errors(fail)]),
    debug_println(8,obtained_java_cmd_from_path(JavaCmd)),
    replace_windows_path_backslashes(JavaCmd,JavaCmdW),
    !.

get_java_command_path(JavaCmdW) :- get_preference(path_to_java,JavaCmd),
    JavaCmd \= '',
    debug_println(8,using_path_to_java_preference(JavaCmd)),
    (file_exists(JavaCmd) -> true
    ; directory_exists(JavaCmd) -> add_warning(get_java_command_path,'No Java Runtime (7 or newer) found; please correct the JAVA_PATH advanced preference (it has to point to the java tool, *not* the directory enclosing it): ',JavaCmd)
    ; add_warning(get_java_command_path,'No Java Runtime (7 or newer) found; please correct the JAVA_PATH advanced preference: ',JavaCmd)),
    replace_windows_path_backslashes(JavaCmd,JavaCmdW),
    !.

get_java_command_path(_JavaCmd) :-
    add_error(get_java_command_path,'Could not get path to the java tool. Make sure a Java Runtime (7 or newer) is installed',''),
    fail.

get_java_fullversion(Version) :-
    get_java_command_path(JavaCmdW),
    (my_system_call(JavaCmdW, ['-fullversion'],java_version,Text) -> Text=Version
    ; format(user_error,'Could not execute ~w -fullversion~n',[JavaCmdW]),
    fail).

get_java_fullversion(V1,V2,V3Atom) :-
    get_java_fullversion(VersionCodes),
    get_java_fullversion_numbers(VersionCodes,VV1,VV2,VV3),!,
    V1=VV1, V2=VV2, V3Atom=VV3.

get_java_fullversion_numbers(VersionCodes,V1,V2,V3Atom) :-
    append("java full version """,Tail,VersionCodes), !,
    get_java_fullversion_numbers_aux(Tail,V1,V2,V3Atom).

get_java_fullversion_numbers(VersionCodes,V1,V2,V3Atom) :-
    append("openjdk full version """,Tail,VersionCodes), !,
    get_java_fullversion_numbers_aux(Tail,V1,V2,V3Atom).

get_java_fullversion_numbers_aux(Tail,1,V2,V3Atom) :-
    % new version scheme (https://openjdk.java.net/jeps/223), leading 1 dropped, 13+33 stands for 1.13.33
    split_chars(Tail,"+",[V2C,V3C]),
    !,
    (try_number_codes(V2,V2C)
    -> get_v3_atom(V3C,V3Atom)
    ; append(V2CC,[0'. | FurtherC], V2C) % there is at least one more dot in the version nr (e.g. 17.0.1+12-LTS-39)
    ->
    try_number_codes(V2,V2CC),
    append(FurtherC,[0'+ | V3C], V3C3),
    get_v3_atom(V3C3,V3Atom)
).

get_java_fullversion_numbers_aux(Tail,V1,V2,V3Atom) :-
    split_chars(Tail,".",[V1C,V2C|FurtherC]),
    append(FurtherC,V3C),
    try_number_codes(V1,V1C),
    try_number_codes(V2,V2C),!,
    get_v3_atom(V3C,V3Atom).

get_java_version(Version) :-
    get_java_command_path(JavaCmdW),
    (my_system_call(JavaCmdW, ['-version'],java_version,Text) -> Text=Version
    ; format(user_error,'Could not execute ~w -version~n',[JavaCmdW]),
    fail).

get_ltl_lang_spec('B,none') :- csp_with_bz_mode,!.

get_ltl_lang_spec('B') :- b_or_z_mode,!.

get_ltl_lang_spec(none).

get_machine_term(machine(M),M).