ltl_verification

access_index_in_path(Index,Path,State,Transition) :-
    path_statetransitions(Path,StateTransitions),
    nth0(Index,StateTransitions,strans(State,Transition)).

check_result(loop(_),unknown,Formula) :-
    !,add_error(ltl_verification,
    'evaluate_ltl_formula computed unknown result for infinite sequence',
    Formula).

check_result(loop(_),deadlock,Formula) :-
    !,add_error(ltl_verification,
    'evaluate_ltl_formula computed unknown result for dead locking sequence',
    Formula).

check_result(_Type,_Result,_Formula).

check_sequence(StateTransitions,Type) :-
    ( Type=loop(_),last(StateTransitions,strans(_,none)) ->
    add_error(ltl_verification,'last element of lasso sequence has no transition id',
    StateTransitions)
    ; true).

compute_unknown(CorePred,Arity,TargetPred) :-
    enumerate_true_false_unknown(Arity,InputArgs),
    compute_unknown_values(CorePred,InputArgs,Result),
    ToStore =.. [TargetPred | Result],
    % print( assertz(ToStore) ),nl,
    assertz( ToStore ),
    fail.

compute_unknown(_CorePred,_Arity,_TargetPred).

compute_unknown_values(CorePred,InputArgs,Result) :-
    length(InputArgs,N), N1 is N+1,
    length(Args,N1),
    append(IArgs,[R],Args),
    Call =.. [CorePred | Args],
    findall( R, (maplist(enumerate_unknown,InputArgs,IArgs),
    call(Call)),
    Outputs),
    sort(Outputs,SOutputs),
    ( SOutputs = [O] -> true
    ; SOutputs = [_|_] -> O=unknown),
    append(InputArgs,[O],Result).

enumerate_true_false_unknown(0,[]).

enumerate_true_false_unknown(Arity,[Value|Rest]) :-
    Arity > 0, member(Value,[true,false,unknown]),
    A2 is Arity-1, enumerate_true_false_unknown(A2,Rest).

enumerate_unknown(true,true).

enumerate_unknown(false,false).

enumerate_unknown(unknown,V) :- member(V,[true,false]).

eval_fairness(Type,Loop,FairCallEnabled,FairCallExecuted,Result) :-
    maplist(strans_state,Loop,States),
    find_enabled_fairids(Type,FairCallEnabled,States,RelevantIds),
    exclude(is_executed(FairCallExecuted,Loop),RelevantIds,NotExecuted),
    (NotExecuted = [] -> Result=fair ; Result=unfair(NotExecuted)).

eval_ltl_formula(false,_Index,_Path,false).

eval_ltl_formula(true,_Index,_Path,true).

eval_ltl_formula(ap(AP),Index,Path,Value) :-
    access_index_in_path(Index,Path,State,_Trans),
    path_ap(Path,Call),
    (call(Call,AP,State) -> Value=true ; Value=false).

eval_ltl_formula(action(TP),Index,Path,Value) :-
    access_index_in_path(Index,Path,State,Trans),
    ( Trans=none ->
    (eval_ltl_is_deadlock(Index,Path) -> Value=false ; Value=unknown)
    ;
    path_tp(Path,Call),
    (call(Call,TP,State,Trans) -> Value=true ; Value=false)).

eval_ltl_formula(not(A),Index,Path,Value) :-
    eval_ltl_formula(A,Index,Path,VA),
    ltl_eval_not(VA,Value),!.

eval_ltl_formula(and(A,B),Index,Path,Value) :-
    eval_ltl_formula(A,Index,Path,VA),
    eval_ltl_formula(B,Index,Path,VB),
    ltl_eval_and(VA,VB,Value),!.

eval_ltl_formula(or(A,B),Index,Path,Value) :-
    eval_ltl_formula(A,Index,Path,VA),
    eval_ltl_formula(B,Index,Path,VB),
    ltl_eval_or(VA,VB,Value),!.

eval_ltl_formula(implies(A,B),Index,Path,Value) :-
    eval_ltl_formula(A,Index,Path,VA),
    eval_ltl_formula(B,Index,Path,VB),
    ltl_eval_implies(VA,VB,Value),!.

eval_ltl_formula(equivalent(A,B),Index,Path,Value) :-
    eval_ltl_formula(A,Index,Path,VA),
    eval_ltl_formula(B,Index,Path,VB),
    ltl_eval_equivalent(VA,VB,Value),!.

eval_ltl_formula(finally(A),Index,Path,Value) :-
    eval_ltl_formula(until(true,A),Index,Path,Value). % TODO: Do not use normalisation

eval_ltl_formula(globally(A),Index,Path,Value) :-
    eval_ltl_formula(not(finally(not(A))),Index,Path,Value). % TODO: Do not use normalisation

eval_ltl_formula(weakuntil(A,B),Index,Path,Value) :-
    eval_ltl_formula(or(globally(A),until(A,B)),Index,Path,Value). % TODO: Do not use normalisation

eval_ltl_formula(release(A,B),Index,Path,Value) :-
    eval_ltl_formula(not(until(not(A),not(B))),Index,Path,Value). % TODO: Do not use normalisation

eval_ltl_formula(once(A),Index,Path,Value) :-
    eval_ltl_formula(since(true,A),Index,Path,Value). % TODO: Do not use normalisation

eval_ltl_formula(historically(A),Index,Path,Value) :-
    eval_ltl_formula(not(once(not(A))),Index,Path,Value). % TODO: Do not use normalisation

eval_ltl_formula(trigger(A,B),Index,Path,Value) :-
    eval_ltl_formula(not(since(not(A),not(B))),Index,Path,Value). % TODO: Do not use normalisation

eval_ltl_formula(next(A),Index,Path,Value) :-
    last_index_in_path(Path,Last),
    ( Index<Last -> % we're are somewhere in the path,
    Next is Index+1,eval_ltl_formula(A,Next,Path,Value) % just use the next position
    ; path_type(Path,loop(ReEntry)) -> % End of the path: If it's a loop,
    eval_ltl_formula(A,ReEntry,Path,Value) % use the start of the lasso as next
    ; eval_ltl_is_deadlock(Index,Path) -> % End of the path (no loop): In a
    Value=false % deadlock X(...) is always false
    ; % End of the path: We don't know the
    Value=unknown). % next state

eval_ltl_formula(yesterday(A),Index,Path,Value) :-
    ( Index > 0 ->
    Y is Index-1,eval_ltl_formula(A,Y,Path,Value)
    ; % Y(...) is always false in the
    Value=false). % initial state.

eval_ltl_formula(until(Inv,Goal),Index,Path,Value) :-
    future_indices(Index,Path,Indices),
    eval_until(Indices,Inv,Goal,Path,Value).

eval_ltl_formula(since(Inv,Goal),Index,Path,Value) :-
    eval_since(Index,Inv,Goal,Path,Value).

eval_ltl_is_deadlock(Index,Path) :-
    eval_ltl_formula(ap(deadlock),Index,Path,true).

eval_since(Index,Inv,Goal,Path,Result) :-
    eval_ltl_formula(Goal,Index,Path,GValue),
    ( Index = 0 -> Result=GValue
    ; GValue = true -> Result=true
    ;
    eval_ltl_formula(Inv,Index,Path,IValue),
    ( GValue=false,IValue=false -> Result=false
    ;
    Y is Index-1,
    eval_since(Y,Inv,Goal,Path,NValue),
    ltl_eval_until(IValue,GValue,NValue,Result),! % same logic as until
)
).

eval_until([],_,_,Path,Result) :-
    last_index_in_path(Path,Last),
    ( path_type(Path,loop(_)) -> Result=false
    ; eval_ltl_is_deadlock(Last,Path) -> Result=false
    ; Result=unknown).

eval_until([H|T],Inv,Goal,Path,Result) :-
    eval_ltl_formula(Goal,H,Path,GValue),
    ( GValue = true -> Result=true
    ;
    eval_ltl_formula(Inv,H,Path,IValue),
    eval_until(T,Inv,Goal,Path,NValue),
    ltl_eval_until(IValue,GValue,NValue,Result),!).

evaluate_ltl_fairness(WeakStrong,StateTransitions,loop(ReEntry),FairCallEnabled,FairCallExecuted,Result) :-
    !,append_length(Loop,StateTransitions,ReEntry),
    eval_fairness(WeakStrong,Loop,FairCallEnabled,FairCallExecuted,Result).

evaluate_ltl_fairness(_WeakStrong,_ST,_Type,_FairCallEn,_FairCallEx,fair). % Fairness is only relevant for loops

evaluate_ltl_formula(Formula,StateTransitions,Type,CallbackAP,CallbackTP,Result) :-
    check_sequence(StateTransitions,Type),
    length(StateTransitions,N),
    Path = path(StateTransitions,N,Type,CallbackAP,CallbackTP),
    eval_ltl_formula(Formula,0,Path,Result),
    % In case of an unknown result, check if the sequence if finite
    check_result(Type,Result,Formula).

find_enabled_fairids(weak,FairCall,[StateId|RLoop],Ids) :-
    find_enabled_fairids_for_state(FairCall,StateId,Unsorted),
    sort(Unsorted,InitialIds),
    find_enabled_fairids_weak(RLoop,FairCall,InitialIds,Ids).

find_enabled_fairids(strong,FairCall,Loop,Ids) :-
    maplist(find_enabled_fairids_for_state(FairCall),Loop,LEnabled),
    append(LEnabled,Unsorted),
    sort(Unsorted,Ids).

find_enabled_fairids_for_state(FairCall,StateId,Enabled) :-
    findall(FairId,call(FairCall,StateId,_TransId,FairId),Unsorted),
    sort(Unsorted,Enabled).

find_enabled_fairids_weak([],_FairCall,Ids,Ids).

find_enabled_fairids_weak(_Loop,_FairCall,[],[]) :- !.

find_enabled_fairids_weak([StateId|RLoop],FairCall,InitialIds,Ids) :-
    find_enabled_fairids_for_state(FairCall,StateId,LocalIds),
    % we use intersect here, only those actions should be tested
    % for "executed in loop" that are enabled in each state of the loop
    ord_intersection(InitialIds,LocalIds,Ids1),
    find_enabled_fairids_weak(RLoop,FairCall,Ids1,Ids).

future_indices(Index,Path,Result) :-
    last_index_in_path(Path,Last),
    numlist(Index,Last,Rest),
    ( path_type(Path,loop(ReEntry)), Index>ReEntry ->
    I2 is Index-1,
    numlist(ReEntry,I2,Before),
    append(Rest,Before,Result)
    ;
    Result = Rest).

is_executed(FairCall,Loop,FairId) :-
    somechk(is_executed2(FairCall,FairId),Loop).

is_executed2(FairCall,FairId,strans(StateId,_TransId)) :-
    call(FairCall,StateId,FairId),!.

last_index_in_path(Path,Last) :-
    path_length(Path,N),Last is N-1.

ltl_eval_and_base(false,_, false).

ltl_eval_and_base(true, false,false).

ltl_eval_and_base(true, true, true).

ltl_eval_equivalent_base(false, false,true).

ltl_eval_equivalent_base(true, true,true).

ltl_eval_equivalent_base(true, false,false).

ltl_eval_equivalent_base(false,true,false).

ltl_eval_implies_base(false,_, true).

ltl_eval_implies_base(true, true, true).

ltl_eval_implies_base(true, false,false).

ltl_eval_not_base(true, false).

ltl_eval_not_base(false,true).

ltl_eval_or_base(true, _, true).

ltl_eval_or_base(false,true, true).

ltl_eval_or_base(false,false,false).

ltl_eval_until_base(_, true, _,true).

ltl_eval_until_base(false,false,_,false).

ltl_eval_until_base(true, false,N,N).

path_ap(path(_ST,_N,_Type,AP,_TP),AP).

path_length(path(_ST,N,_Type,_AP,_TP),N).

path_statetransitions(path(StateTransitions,_N,_Type,_AP,_TP),StateTransitions).

path_tp(path(_ST,_N,_Type,_AP,TP),TP).

path_type(path(_ST,_N,Type,_AP,_TP),Type).

strans_state(strans(StateId,_TransId),StateId).