ltsmin

assert_all([]).

assert_all([H|T]) :-
    assertz(H), assert_all(T).

assert_guard_readsets([]).

assert_guard_readsets([[GuardName, ReadSet]|R]) :-
    assertz(guard_reads(GuardName, ReadSet)),
    assert_guard_readsets(R).

assert_label_to_accessed_vars([]).

assert_label_to_accessed_vars([[Label,ListOfVars]|T]) :-
    varname_list(L),
    findall(AccessedOrderedVars, (member(AccessedOrderedVars, L),
    member(AccessedOrderedVars, ListOfVars)),
    AccessedVarSet), % poor man's sort-by
    assertz(label_to_reads(Label, AccessedVarSet)),
    assert_label_to_accessed_vars(T).

assert_op_guards([], []).

assert_op_guards([Op|T], [GuardList|T2]) :-
    assertz(op_guards(Op, GuardList)),
    assert_op_guards(T, T2).

assert_short_state_info(MR, InitialState) :-
    varname_list(L),
    generate_bindings(InitialState, L, BoundInitialState),
    assert_short_state_transformations(MR, BoundInitialState).

assert_short_state_transformations([], InitialState) :-
    varname_list(L),
    prepare_binding(L, [], PreparedBinding, PreparedVarListForUnification),
    back_to_short(PreparedBinding, L, LongPattern, PreparedShort, InitialState, InitialState),
    assertz(black_magic_short_transformation('$init_state', PreparedBinding, PreparedVarListForUnification, LongPattern, PreparedShort, InitialState,
    PreparedBinding, PreparedVarListForUnification, LongPattern, PreparedShort, InitialState)).

assert_short_state_transformations([list([Op, ReadsGuard, ReadsAction, MustWrite, MayWrite|_])|T], InitialState) :-
    varname_list(L),
    sort_by_and_distinct(L, ReadsAction, SortedReadsAction),
    append([ReadsGuard, ReadsAction, MustWrite, MayWrite], AllAccessedVarsWithDups),
    append([ReadsAction, MustWrite, MayWrite], AllAccessedVarsForActionWithDups),
    append([ReadsGuard, ReadsAction], AllReadsWithDups),
    append([MustWrite, MayWrite], AllWritesWithDups),
    sort_by_and_distinct(L, AllAccessedVarsWithDups, AllAccessedVars),
    sort_by_and_distinct(L, AllAccessedVarsForActionWithDups, AllAccessedVarsForAction),
    sort_by_and_distinct(L, AllReadsWithDups, AllReads),
    sort_by_and_distinct(L, AllWritesWithDups, AllWrites),
    prepare_binding(AllAccessedVars, AllReads, PreparedBinding, PreparedVarListForUnification),
    prepare_binding(AllAccessedVarsForAction, SortedReadsAction, PreparedBindingForNextAction, PreparedVarListForUnificationForNextActionFactoryProviderSingleton),
    back_to_short(PreparedBinding, AllWrites, LongPattern, PreparedShort, Defaults, InitialState),
    back_to_short(PreparedBindingForNextAction, AllWrites, LongPatternForAction, PreparedShortForNextAction, DefaultsForAction, InitialState),
    assertz(black_magic_short_transformation(Op, PreparedBinding, PreparedVarListForUnification, LongPattern, PreparedShort, Defaults,
    PreparedBindingForNextAction, PreparedVarListForUnificationForNextActionFactoryProviderSingleton, LongPatternForAction, PreparedShortForNextAction, DefaultsForAction)),
    assert_short_state_transformations(T, InitialState).

atom_concat([X], X) :- !.

atom_concat([H1, H2|T], R) :-
    atom_concat(H1, H2, H),
    atom_concat([H|T], R).

back_to_short([], [], [], [], [], _InitialState).

back_to_short([bind(H, _)|T], [H|WriteTail], [bind(H, V)|LongStateTail], [bind(H, V)|ShortTail], [bind(H, Default)|DefaultBindingsTail], InitialState) :- !,
    % variable is written to
    memberchk(bind(H, Default), InitialState),
    back_to_short(T, WriteTail, LongStateTail, ShortTail, DefaultBindingsTail, InitialState).

back_to_short([bind(H, _)|T], Writes, [bind(H, _)|LongStateTail], Short, DefaultBindings, InitialState) :-
    back_to_short(T, Writes, LongStateTail, Short, DefaultBindings, InitialState).

backend_specific_flags(symbolic, ['--lace-workers=1'], _).

backend_specific_flags(sequential, FlagsSeq, MoreFlags) :-
    (member(nocache, MoreFlags) -> FlagsSeq = [] ; FlagsSeq = ['-c']).

build_initial_state(_, VType, VVal) :-
    any_value_for_type(VType, VVal).

calc_and_append_por_info(false, _Msg, _, _, _) :- !.

calc_and_append_por_info(_Por, Msg, GuardVector, GuardNames, TransitionGroups) :-
    may_be_coenabled(GuardVector, GuardNames, MayBeCoEnabledMatrix),
    write_matrix(Msg, MayBeCoEnabledMatrix, may_be_coenabled_matrix),
   
    necessary_enabling_set(GuardVector, TransitionGroups, NES),
    create_matrix(GuardNames, NES, NesMatrix),
    write_matrix(Msg, NesMatrix, necessary_enabling_set),
   
    necessary_disabling_set(GuardVector, TransitionGroups, NDS),
    create_matrix(GuardNames, NDS, NdsMatrix),
    write_matrix(Msg, NdsMatrix, necessary_disabling_set),
   
    do_not_accord(TransitionGroups, DNA),
    create_matrix(TransitionGroups, DNA, DnaMatrix),
    write_matrix(Msg, DnaMatrix, do_not_accord_matrix).

calculate_enabling_set(TransitionGroupList, Guard, Res) :-
    create_negation(Guard, NGuard),
    calculate_enabling_set_aux(TransitionGroupList, Guard, NGuard, Res).

calculate_enabling_set_aux([], _Guard, _NGuard, []) :- !.

calculate_enabling_set_aux([Transition|Rest], Guard, NGuard, [Transition|ResList]) :-
    can_enable(Transition, Guard, NGuard), !,
    calculate_enabling_set_aux(Rest, Guard, NGuard, ResList).

calculate_enabling_set_aux([_|Rest], Guard, NGuard, ResList) :-
    calculate_enabling_set_aux(Rest, Guard, NGuard, ResList).

can_enable(TransitionGroup, Guard, NGuard) :-
    ltsmin_test_path_possible(NGuard, [TransitionGroup], Guard).

check_ap_bound_state(bpred(Property),Node) :-
    b_test_boolean_expression_for_ground_state(Property, [], Node,'LTSMin atomic proposition',0).

check_ap_bound_state(enabled(Op),Node) :- !,
    op_enabled(Op, Node).

check_ap_bound_state(det(OpList),Node) :- !,
    max_enabled(OpList, Node, 1, 0, R),
    R < 2.

check_ap_bound_state(dlk(OpList),Node) :- !,
    max_enabled(OpList, Node, 0, 0, 0).

check_ap_bound_state(ctrl(OpList),Node) :- !,
    max_enabled(OpList, Node, 1, 0, 1).

check_ap_bound_state(deadlock,Node) :- !,
    get_transition_groups(OpList),
    check_ap_bound_state(dlk(OpList), Node).

compute_successors('$init_state',_,Result) :- !,
    findall(S,init_state(S),Result),
    debug:debug_println(9,res_init_state(Result)).

compute_successors(OpName,L,Result) :-
    temporary_set_preference(try_operation_reuse,false,CHNG2), % operation reuse done by LTSmin; we would only get no_packed_state_info messages and no benefit
    (debug:debug_mode(on) -> nl,print(compute_successors(OpName)),nl,flush_output ; true),
    findall(S,specfile:specfile_trans(L,OpName,_,S,_,_),Result),
    reset_temporary_preference(try_operation_reuse,CHNG2).

create_matrix(Headings, Entries, Res) :-
    create_matrix(Headings, Entries, [], Res).

create_matrix([], [], Res, Res) :- !.

create_matrix([H1|T1], [H2|T2], Acc, Res) :-
    create_matrix(T1, T2, [[H1,H2]|Acc], Res).

del_temp_file(F) :- (file_exists(F) -> delete_file(F) ; true).

distinct(X, Y) :-
    distinct(X, [], Y).

distinct([], _, []).

distinct([H|T], Seen, Res) :-
    member(H, Seen), !,
    distinct(T, Seen, Res).

distinct([H|T], Seen, [H|Res]) :-
    distinct(T, [H|Seen], Res).

do_not_accord(['$init_state'|TransitionGroups], [[]|DoNotAccordMatrix]) :-
    maplist(does_not_accord_with_aux(TransitionGroups), TransitionGroups, DoNotAccordMatrix).

does_not_accord_with_aux([], _, []).

does_not_accord_with_aux([H|T], TransitionGroup, [H|R]) :-
    debug_println(9,check_dependency(H,TransitionGroup)),
    get_preference(timeout_cbc_analysis,TO),
    dependent_actions(H, TransitionGroup, 0, TO, _), !, % TODO: handle interrupts?
    does_not_accord_with_aux(T, TransitionGroup, R).

does_not_accord_with_aux([_|T], TransitionGroup, R) :-
    does_not_accord_with_aux(T, TransitionGroup, R).

eval_label(Msg, State,invariant) :-
    bmachine:b_get_invariant_from_machine(Invariant),!, % Should we use: get_unproven_invariants
    (profile_single_call(check_invariant,
    b_interpreter:b_test_boolean_expression_for_ground_state(Invariant,[],State,'LTSMin invariant label',0)) ->
    put_number(Msg, 1); put_number(Msg, 0)).

eval_label(Msg, State,Label) :-
    (debug:debug_mode(on) -> print(eval(Label)),nl,flush_output ; true),
    state_label(Label, Type, AST),
    profile_single_call(Label,ltsmin:eval_label2(Type, Msg, State, AST)).

eval_label2(ltl_ap, Msg, State, AST) :-
    (check_ap_bound_state(AST,State) ->
    put_number(Msg, 1); put_number(Msg, 0)).

eval_label2(_, Msg, State, AST) :-
    (b_test_boolean_expression_for_ground_state(AST,[],State,'LTSMin label',0) ->
    put_number(Msg, 1) ; put_number(Msg, 0)).

extract_name_and_type([],[], []).

extract_name_and_type([b(identifier(HT),TypeTerm,_)|T], [HT|RT], [TypeTerm|RType]) :-
    extract_name_and_type(T,RT,RType).

extract_tg_and_nth_entry([], _, R, R).

extract_tg_and_nth_entry([list(H)|T], Arg, Acc, R) :-
    nth1(1, H, TransitionGroup),
    nth1(Arg, H, X),
    extract_tg_and_nth_entry(T, Arg, [[TransitionGroup, X]|Acc], R).

generate_bindings([], [], []) :- !.

generate_bindings([H|T], [Name|TN], [bind(Name, H)|R]) :-
    generate_bindings(T, TN, R).

generate_bound_long_state([CSP|BState],Res) :- csp_with_bz_mode,!,
    Res=csp_and_b(CSP,BoundState),
    varname_list(L),
    %print(gen_bind(BState,L)),nl,
    generate_bindings(BState, L, BoundState).

generate_bound_long_state(BState,BoundState) :-
    varname_list(L),
    generate_bindings(BState, L, BoundState).

generate_bound_state_short_label(BState,Label,BoundState) :-
    label_to_reads(Label, L),
    generate_bindings(BState, L, BoundState).

generate_names(Terms, PrefixAtom, Names) :-
    atom_codes(PrefixAtom, PrefixChars),
    generate_names_aux(Terms, PrefixChars, 1, [], Names).

generate_names_aux([], _, _, Acc, Acc) :- !.

generate_names_aux([_|T], Prefix, N, Acc, Res) :-
    number_codes(N, NC),
    append(Prefix, NC, NamedC),
    atom_codes(Named, NamedC),
    N1 is N+1,
    generate_names_aux(T, Prefix, N1, [Named|Acc], Res).

get_init(Msg, PorInt) :-
    (PorInt == 0 -> Por = false ; Por = true),
    get_ltsmin_variable_names(VS, VTypes),
    assertz(varname_list(VS)),
    formatsilent('List of variables for LTSmin (por=~w): ~w~n',[Por,VS]),
    maplist(build_initial_state, VS, VTypes, BInitialState),
    %maplist(any_value_for_type,VTypes,InitialState),
    maplist(term_to_atom, VTypes, VTypeAtoms),
    get_transition_groups(TransitionGroups),
    (csp_with_bz_mode
    -> InitialState = [stop(no_loc_info_available) | BInitialState], % DUMMY Values
    Vars = ['$CSP_CHUNK'|VS], Types = ['csp_process'|VTypeAtoms]
    ; InitialState = BInitialState,
    Vars = VS, Types = VTypeAtoms
    ),
    debug_println(9,initial(InitialState)),
    write_chunklist(Msg, InitialState, initial_state),
    write_chunklist(Msg, TransitionGroups, transition_group_list),
    write_chunklist(Msg, Vars, variables_name_list), % we use $CSP_CHUNK as name for the CSP chunk
    write_chunklist(Msg, Types, variables_type_list),
   
   
    put_read_write_matrices(Msg, MR),
    assert_short_state_info(MR, InitialState),
   
    (Por == false -> inv_state_label_matrix(InvStateLabelMatrix)
    ; inv_state_label_matrix_for_por(InvStateLabelMatrix)),
   
    %print(slm(InvStateLabelMatrix)),nl,
    %% split guards to state labels
    split_guards(Por, TransitionGroups, GuardVector, GuardNames, IndexVectors),
    get_state_labels(GuardVector, GuardNames, guard, GuardStateLabelMatrix),
   
    % memoize mapping OpName -> GuardNames
    assert_op_guards(TransitionGroups, IndexVectors),
    % memoize mapping GuardName -> ReadSet(Guard)
    assert_guard_readsets(GuardStateLabelMatrix),
   
    reverse(GuardNames, GuardNamesInOrder),
    assertz(guard_labels(GuardNamesInOrder)),
   
    get_ltl_labels(ListOfLabelASTs, LtlApNames),
    ltl_to_state_label_matrix(ListOfLabelASTs, LtlApNames, LtlStateLabelMatrix),
   
    % accessed variable names in order (for short states)
    assert_label_to_accessed_vars(InvStateLabelMatrix),
    assert_label_to_accessed_vars(GuardStateLabelMatrix),
    assert_label_to_accessed_vars(LtlStateLabelMatrix),
   
    %% write all state labels (invariant conjuncts and guard conjuncts)
    write_matrix(Msg, InvStateLabelMatrix, state_label_matrix),
    write_matrix(Msg, GuardStateLabelMatrix, guard_label_matrix),
    write_matrix(Msg, LtlStateLabelMatrix, ltl_label_matrix),
   
    %% create guard info matrix, i.e. which transition depends on which guards
    create_matrix(TransitionGroups, IndexVectors, GuardInfoMatrix),
    write_matrix(Msg, GuardInfoMatrix, guard_info_matrix),
    calc_and_append_por_info(Por, Msg, GuardVector, GuardNames, TransitionGroups).

get_label_group_guards(Msg, State) :-
    guard_labels(Labels),
    maplist(eval_label(Msg, State), Labels).

get_ltl_labels(ASTs, Names) :-
    findall(ap_representation(Hash, AST), ltl_safety:ap_representation(Hash, AST), APReprs),
    maplist(arg(2), APReprs, ASTs),
    maplist(arg(1), APReprs, Names).

get_ltl_readsets(bpred(X), ReadSet) :-
    bsyntaxtree:predicate_identifiers(X, ReadSet).

get_ltl_readsets(enabled(Op), ReadSet) :-
    op_to_reads_guard(Op, ReadSet). % get readset of guards of op

get_ltl_readsets(det(OpList), ReadSet) :-
    oplist_to_reads_guards(OpList, ReadSet).

get_ltl_readsets(dlk(OpList), ReadSet) :-
    oplist_to_reads_guards(OpList, ReadSet).

get_ltl_readsets(ctrl(OpList), ReadSet) :- !,
    oplist_to_reads_guards(OpList, ReadSet).

get_ltl_readsets(deadlock, ReadSet) :-
    get_transition_groups(OpList),
    oplist_to_reads_guards(OpList, ReadSet).

get_ltl_readsets(AP,_) :- !,
    add_error_fail(ltsmin, 'operation is not supported for LTSmin', AP).

get_ltsmin_flags(Backend, NoDead, NoInv, MoreFlags, TraceFile, ResFlags) :-
    backend_specific_flags(Backend, BackendFlags, MoreFlags),
    (member(por, MoreFlags) -> POR = true ; POR = false),
    property_flags(NoDead, NoInv, POR, PropertyFlags),
    convlist(ltsmin_flag, MoreFlags, EvenMoreFlags),
    TraceFlags = ['--trace', TraceFile],
    append([TraceFlags, BackendFlags, PropertyFlags, EvenMoreFlags], ResFlags).

get_ltsmin_guards(OpName,Guards,RestBody) :-
    get_preference(ltsmin_guard_splitting,true),!,
    get_operation_propositional_guards(OpName,Guards,RestBody).

get_ltsmin_guards(OpName,ResGuards,RestBody) :-
    get_operation_propositional_guards(OpName,Guards,RestBody),
    conjunct_predicates(Guards,BigGuard),
    (always_well_defined(BigGuard)
    -> ResGuards = Guards
    ; ResGuards = [BigGuard] % avoid WD errors when splitting guard
).

get_ltsmin_invariant(LTSminInv, Por) :-
    (Por == false -> Type = invariant ; Type = por_invariant),
    findall(InvLabel, state_label(InvLabel, Type, _AST), InvariantNames),
    (InvariantNames == [] -> Invariant = ['true']; interpose(InvariantNames, ' && ', Invariant)),
    atom_concat(Invariant, Invariant2),
    atom_concat(['--invariant=!is_init || (', Invariant2, ')'], LTSminInv).

get_ltsmin_variable_names(Names, Types) :-
    bmachine:b_get_machine_variables(V),
    % bmachine:b_get_machine_all_constants(C), % this includes constants which have been moved to deferred sets; causes issue with hanoi model
    bmachine:b_get_machine_constants(C), % this does not include global set constants
    append(V,C,CV), % compatible with b_initialise_machine2 and expand_const_and_vars order
    extract_name_and_type(CV,Names,Types).

get_name([H|_], [Name|_], G, Name) :-
    same_texpr(G, H), !.

get_name([_|GV], [_|Names], G, R) :-
    get_name(GV, Names, G, R).

get_next_action(Type, Msg, State,Op) :- % State is a list of bindings
    temporary_set_preference(ltsmin_do_not_evaluate_top_level_guards,true,CHNG),
    get_next_states(Type, Msg, State,Op),
    reset_temporary_preference(ltsmin_do_not_evaluate_top_level_guards,CHNG).

get_next_states(LongOrPattern, Msg, State,Op) :- % State is a list of bindings
    % TO DO: set_context_state(SomeID) and look if state_error(SomeID,Id,Error) were added
    profile_single_call(Op,ltsmin:compute_successors(Op, State, Succs)),
    length(Succs,NrStates),
    % format(" ~w successor states for ~w~n ~w~n",[NrStates,Op,Succs]),nl,
    (NrStates>0 -> mark_operation_as_covered(Op) ; true), % TO DO: we should probably use another Prolog fact for this; to avoid confusion which operations are covered in ProB's internal statespace
    put_number(Msg, NrStates),
    put_successors(LongOrPattern, Succs, Msg).

get_opname(bop(Name, _, _, _, _), Name).

get_opname(btrans(event(Name)), Name).

get_opname(btrans(event(Name, _, _)), Name).

get_path_to_fresh_csv_trace_file(File) :- get_temporary_filename('prob-ltsmin-trace.csv',File).

get_path_to_fresh_ltsmin_endpoint(File) :- get_temporary_filename('ltsmin.probz',File).

get_path_to_fresh_trace_file(File) :- get_temporary_filename('prob-ltsmin-trace.gcf',File).

get_path_to_ltl_file('/tmp/prob-ltsmin-formula.ltl').

get_state_label(Msg, LabelA, StateA) :- mnf1(get_state_label_aux(long, Msg, LabelA, StateA)).

get_state_label_aux(Type, Msg, LabelA, StateA) :-
    read_state(StateA, State),
    fast_buf_read(Label,LabelA), %print(get_state_label(Label)),nl,
    (Type == long -> generate_bound_long_state(State,BoundState)
    ; generate_bound_state_short_label(State, Label, BoundState)),
    %print(get_state_label_state(Label, BoundState)),nl,
    eval_label(Msg, BoundState,Label).

get_state_label_group(Msg, OperationA, StateA) :- %print(prolog_get_succs),nl,flush_output,
    mnf1(get_state_label_group_aux(Msg, OperationA, StateA)).

get_state_label_group_aux(Msg, TypeA, StateA) :-
    read_state(StateA,State),
    %print(generate(State)),nl,
    generate_bound_long_state(State,BoundState),
    fast_buf_read(Type,TypeA),
    (debug:debug_mode(on)
    -> format('~n ** get_state_label_group for ~w~n',[Type]),
    translate:print_state(BoundState),nl
    ; true),
    (Type == '1' -> get_label_group_guards(Msg, BoundState)
    ; print(unhandled_group_type(Type)),nl,fail).

get_state_label_short(Msg, LabelA, StateA) :- mnf1(get_state_label_aux(short, Msg, LabelA, StateA)).

get_state_labels(ListOfConjuncts, Names, Type, StateLabelMatrix) :-
    %% format of StateLabelMatrix is
    % [[label1, [id1, id2, ...]]
    % [label2, [id2, id4, ...]]
    % ...]
    maplist(wrap_named_inv(Type), Names, ListOfConjuncts, Facts),
    assert_all(Facts),
    maplist(bsyntaxtree:predicate_identifiers, ListOfConjuncts, SLSVars),
    create_matrix(Names, SLSVars, StateLabelMatrix).

get_successors(Msg, OperationA, StateA) :- %print(prolog_get_succs),nl,flush_output,
    mnf1(get_successors_aux(long, Msg, OperationA, StateA)).

get_successors_aux(Type, Msg, OperationA, StateA) :-
    read_state(StateA,State),
    fast_buf_read(Operation,OperationA),
    %print(operation(Operation)),nl,
    % print(successors(Operation, State)),nl,
    (Type == short -> black_magic_short_transformation(Operation, BoundState, State, LongPattern, ShortSucc, Defaults, _, _, _, _, _), ShortOrLong = LongPattern-ShortSucc-Defaults
    ; generate_bound_long_state(State, BoundState), ShortOrLong = long),
    %print(generate(BoundState)),nl,
    (debug:debug_mode(on)
    -> format('~n ** get_successors for ~w (~w)~n',[Operation,ShortOrLong]),
    translate:print_state(BoundState),nl
    ; true),
    get_next_states(ShortOrLong, Msg, BoundState,Operation).

get_successors_short(Msg, OperationA, StateA) :- %print(prolog_get_succs),nl,flush_output,
    mnf1(get_successors_aux(short, Msg, OperationA, StateA)).

get_tool_name(symbolic, 'prob2lts-sym').

get_tool_name(sequential, 'prob2lts-seq').

get_tool_name(printtrace, 'ltsmin-printtrace').

get_transition_groups(['$init_state'|L]) :-
    (specfile:b_or_z_mode
    -> findall(OperationName, bmachine:b_top_level_feasible_operation(OperationName), BL),
    (csp_with_bz_mode -> L = ['$CSP'|BL] ; L=BL)
    ; L=[]). % FIXME: provide list for CSP-M

guard_seen(G, [H|_]) :-
    same_texpr(G, H), !.

guard_seen(G, [_|LofG]) :-
    guard_seen(G, LofG).

guard_vector(ListOfListOfGuards, Res) :-
    append(ListOfListOfGuards, ListOfGuards),
    setify_guards(ListOfGuards, Res).

guards_to_indices(GuardVector, Names, ListOfGuards, ListOfIndices) :-
    maplist(get_name(GuardVector, Names), ListOfGuards, ListOfIndices).

init_state(Res) :- specfile:specfile_trans(root,_,_,S,_,_),
    init_state2(S,Res). % , nl,print(init(Res)),nl.

init_state2(csp_and_b_root,Res) :- !,
    specfile:specfile_trans(csp_and_b_root,_,_,S,_,_),
    init_state2(S,Res).

init_state2(concrete_constants(L),FullRes) :- !,
    specfile:specfile_trans(concrete_constants(L),_,_,Res,_,_),
    expand_const_and_vars_to_full_store(Res,FullRes).

init_state2(R,R).

interpose([], _, []).

interpose([X], _, [X]) :- !.

interpose([H|T], I, [H,I|IT]) :-
    interpose(T, I, IT).

ltl_to_state_label_matrix(ListOfAPs, LtlApNames, LtlStateLabelMatrix) :-
    %% format of StateLabelMatrix is
    % [[label1, [id1, id2, ...]]
    % [label2, [id2, id4, ...]]
    % ...]
    maplist(wrap_named_inv(ltl_ap), LtlApNames, ListOfAPs, Facts),
    assert_all(Facts),
    maplist(get_ltl_readsets, ListOfAPs, SLSVars),
    create_matrix(LtlApNames, SLSVars, LtlStateLabelMatrix).

ltsmin_flag(por, '--por').

ltsmin_flag(g, '-g').

ltsmin_flag(ltl_formula(_), Flag) :-
    get_path_to_ltl_file(Path),
    atom_concat('--ltl=', Path, Flag).

ltsmin_generate_ltlfile(Formula, OutputFile) :-
    %% firstly, wrap the Formula into X(Formula)
    %% this avoids that a property is already considered true
    %% because it is in the artificial initial state
    atom_concat('X(', Formula, XFormula),
    atom_concat(XFormula, ')', FinalFormula),
    format('parsing LTL formula ~a~N', [FinalFormula]),
    setup_ltl_formula(FinalFormula, ResAtom),
    format('done. writing to: ~a~N', [OutputFile]),
    write_to_ltl_file(ResAtom, OutputFile).

ltsmin_init(Endpoint,Zocket) :-
    loadfr,
    reset_ltsmin_extension,
    split_invariant(ListOfInvariantConjuncts, InvNames, ListOfInvariantConjunctsForPOR, InvNamesForPOR),
    get_state_labels(ListOfInvariantConjuncts, InvNames, invariant, InvStateLabelMatrix),
    get_state_labels(ListOfInvariantConjunctsForPOR, InvNamesForPOR, por_invariant, InvStateLabelMatrixForPOR),
    assertz(inv_state_label_matrix(InvStateLabelMatrix)),
    assertz(inv_state_label_matrix_for_por(InvStateLabelMatrixForPOR)),
    ltsmin_initialize(Endpoint, Zocket).

ltsmin_init(Endpoint,Zocket, LtlFormula) :-
    (var(LtlFormula) -> true ; setup_ltl_formula(LtlFormula, _)),
    ltsmin_init(Endpoint, Zocket).

ltsmin_loop(Zocket) :-
    h_zocket2(Zocket, Ret), % this is a C function in ltsmin_c_interface, which does the call-backs to Prolog
    Ret == 0, !,
    ltsmin_loop(Zocket).

ltsmin_loop(_).

ltsmin_state_label(X) :- state_label(X, _, _).

ltsmin_test_path_possible(Conjunction,Path,Guard) :-
    get_preference(use_cbc_analysis,true),!,
    get_preference(timeout_cbc_analysis,TO),
    temporary_set_preference(use_chr_solver,true,CHNG1),
    test_path(Conjunction, Path, Guard, 0, TO, Result),
    reset_temporary_preference(use_chr_solver,CHNG1),
    (Result = ok ; Result == timeout ; Result == unknown).

ltsmin_test_path_possible(_,_,_). % assume possible

ltsmin_transition_group(X) :-
    get_transition_groups(TGs), member(X, TGs).

ltsmin_variable(X) :-
    varname_list(Variables), member(X, Variables).

max_enabled([], _State, _Max, R, R).

max_enabled([Op|T], State, Max, EnabledSoFar, R) :-
    (op_enabled(Op, State)
    -> Enabled is EnabledSoFar + 1,
    Max >= Enabled,
    max_enabled(T, State, Max, Enabled, R)
    ; max_enabled(T, State, Max, EnabledSoFar, R)).

may_be_coenabled(GuardVector, Names, MayBeCoEnabledMatrix) :-
    % calculates an upper triangle matrix without the elements on the diagonal
    may_be_coenabled2(GuardVector, Names, MayBeCoEnabledMatrix).

may_be_coenabled2([], [], []).

may_be_coenabled2([_], [_], []).

may_be_coenabled2([H|T], [Name|NameRest], [[Name,R]|RT]) :-
    include(may_be_coenabled_guards(H), NameRest, T, R),
    may_be_coenabled2(T, NameRest, RT).

may_be_coenabled_guards(G1, _G2Name, G2) :-
    conjunct_predicates([G1, G2], Conjunction),
    is_truth(Truth),
    ltsmin_test_path_possible(Conjunction, [], Truth).

mnf1(Call) :- %format('Calling ~w~n',[Call]), flush_output,
    if( catch(Call, E,
    (add_internal_error('LTSMin Extension Exception: ',[E]),flush_output,fail)
    ),
    true,
    (add_internal_error('LTSMin Extension Call Failed: ',[Call]),flush_output,fail)
).

necessary_disabling_set(GuardVector, TransitionGroups, R) :-
    maplist(create_negation, GuardVector, NGuardVector),
    necessary_enabling_set(NGuardVector, TransitionGroups, R).