ltl_propositions

add_parameter_values2([],[],State,State).

add_parameter_values2([TParameter|Prest],[Argument|Arest],InState,OutState) :-
    def_get_texpr_id(TParameter,Parameter),
    add_var_to_localstate(Parameter,Argument,InState,InterState),
    add_parameter_values2(Prest,Arest,InterState,OutState).

add_post_state_values([],_DstNode,State,State) :- !.

add_post_state_values(Access,Node,InState,OutState) :-
    visited_expression(Node,DstState1),
    state_corresponds_to_initialised_b_machine(DstState1,DstState),
    add_post_state_values2(Access,DstState,InState,OutState).

add_post_state_values2([],_DstState,State,State).

add_post_state_values2([poststate(Orig,Primed)|Prest],DstState,InState,OutState) :-
    lookup_value(Orig,DstState,Value),
    add_var_to_localstate(Primed,Value,InState,InterState),
    add_post_state_values2(Prest,DstState,InterState,OutState).

check_ap(bpred(Property),Node) :-
    !, test_boolean_expression_in_node(Node,Property,'LTL atomic proposition').

check_ap(enabled(Op),Node) :- !,
    check_enabled(Op,Node).

check_ap(det(OpList),Node) :- !,
    check_if_maximum_one_enabled(OpList,Node).

check_ap(dlk(OpList),Node) :- !,
    check_if_all_disabled(OpList,Node).

check_ap(ctrl(OpList),Node) :- !,
    is_exactly_one_operation_enabled(OpList,Node).

check_ap(det_output,Node) :- !,
    \+ non_det_output_transition(Node,_,_TID1,_TID2).

check_ap(deadlock,Node) :- !, \+ trans(Node,_,_,_).

check_ap(goal,Node) :- !, node_satisfies_goal(Node).

check_ap(state_error,Node) :- !, state_error(Node,_StateErrId,_Error).

check_ap(sink,Node) :- !,
    \+ ( trans(Node,Next,_,_),Next \= Node ).

check_ap(stateid(SpecNode),Node) :- !, SpecNode = Node.

check_ap(xtl_predicate_check(Prop),Node) :-
    visited_expression(Node,State),!,
    property(State,Prop).

check_ap(X,Node) :- visited_expression(Node,_),!,
    add_internal_error('Unknown atomic proposition:',check_ap(X,Node)),fail.

check_ap(X,Node) :- add_internal_error('Unknown state:',check_ap(X,Node)),fail.

check_atomic_property_formula(ap(ParsedFormula),NodeId) :- !,
    check_ap(ParsedFormula,NodeId).

check_atomic_property_formula(and(P1,P2),NodeId) :- !,
    check_atomic_property_formula(P1,NodeId),
    check_atomic_property_formula(P2,NodeId).

check_atomic_property_formula(or(P1,P2),NodeId) :- !,
    (check_atomic_property_formula(P1,NodeId) -> true
    ; check_atomic_property_formula(P2,NodeId)).

check_atomic_property_formula(implies(P1,P2),NodeId) :- !,
    (check_atomic_property_formula(P1,NodeId)
    -> check_atomic_property_formula(P2,NodeId) ; true).

check_atomic_property_formula(equivalent(P1,P2),NodeId) :- !,
    (check_atomic_property_formula(P1,NodeId)
    -> check_atomic_property_formula(P2,NodeId)
    ; \+ check_atomic_property_formula(P2,NodeId)).

check_atomic_property_formula(not(P1),NodeId) :- !,
    (check_atomic_property_formula(P1,NodeId) -> fail ; true).

check_atomic_property_formula(true,_) :- !.

check_atomic_property_formula(false,_) :- !,fail.

check_atomic_property_formula(Formula,_) :- %print(Formula),nl,
    pp_ltl_formula(Formula,Text),!,
    add_error(check_atomic_property_formula,'LTL formula is not an atomic property: ',Text).

check_atomic_property_formula(Formula,N) :-
    add_internal_error('LTL formula invalid: ',check_atomic_property_formula(Formula,N)),fail.

check_b_operation_value(OpValue,Expr,Node,State) :-
    ( var(State) ->
    visited_expression(Node,RawState),
    state_corresponds_to_initialised_b_machine(RawState,State)
    ; true),
    empty_state(LS),
    b_compute_expression_nowf(Expr,LS,State,PatternValue,'LTL check operation value',0),
    equal_object(PatternValue,OpValue),!.

check_before_after_transition(Predicate,_Transition,SrcNode,DstNode) :-
    get_primed_variable_state(SrcNode,LocalState),
    visited_expression(DstNode,DstState),
    state_corresponds_to_initialised_b_machine(DstState,DstBState),
    b_test_boolean_expression_cs(Predicate,LocalState,DstBState,'LTL before-after',SrcNode).

check_bop_arg_pattern(Index,Expr,Node,State,Op) :-
    arg(Index,Op,OpValue), % exception if Index is expression like 1+1 <----
    check_b_operation_value(OpValue,Expr,Node,State).

check_bop_arg_patterns([],_,_,_).

check_bop_arg_patterns([P|Prest],Node,State,Op) :-
    check_bop_arg_patterns2([P|Prest],Node,State,Op).

check_bop_arg_patterns2([],_,_,_).

check_bop_arg_patterns2([Index/Expr|Prest],Node,State,Op) :-
    check_bop_arg_pattern(Index,Expr,Node,State,Op),
    check_bop_arg_patterns2(Prest,Node,State,Op).

check_bop_res_pattern(Index,Expr,Node,State,OpResult) :-
    nth1(Index,OpResult,OpValue),
    check_b_operation_value(OpValue,Expr,Node,State).

check_bop_res_patterns([],_,_,_).

check_bop_res_patterns([P|Prest],Node,State,OpResult) :-
    check_bop_res_patterns2([P|Prest],Node,State,OpResult).

check_bop_res_patterns2([],_,_,_).

check_bop_res_patterns2([Index/Expr|Prest],Node,State,OpResult) :-
    check_bop_res_pattern(Index,Expr,Node,State,OpResult),
    check_bop_res_patterns2(Prest,Node,State,OpResult).

check_change_expr_transition(Comp,_,_Transition,root,_DstNode) :- !, Comp=eq. % we assume initialisation is not a change

check_change_expr_transition(Comp,_,_Transition,SrcNode,_DstNode) :-
    is_concrete_constants_state_id(SrcNode),!, Comp=eq. % we assume initialisation is not a change

check_change_expr_transition(Comp,TExpr,_Transition,SrcNode,DstNode) :- !,
    % TO DO: provide optimized version for variable ids: just obtain value from unpacked state
    %print(check_unchanged(SrcNode,DstNode,_Transition)),nl,
    eval_expr_in_state(TExpr,SrcNode,BeforeValue),
    eval_expr_in_state(TExpr,DstNode,AfterValue),
    %print(unchanged(SrcNode,DstNode,BeforeValue,AfterValue)),nl,
    compare_values(Comp,BeforeValue,AfterValue).

check_enabled(Spec,SrcNode) :-
    trans(SrcNode,DestNode,Transition,TransId),
    check_transition_pred(Spec,Transition,SrcNode,TransId,DestNode),!.

check_eventb_transition(event(Name),Transition,_SrcNode,_DstNode) :- !,
    functor(Transition,Name,_).

check_eventb_transition(event(Name,Predicate,PoststateAccess),Transition,SrcNode,DstNode) :- !,
    functor(Transition,Name,_),
    visited_expression(SrcNode,CurState),
    state_corresponds_to_initialised_b_machine(CurState,CurBState),
    parameter_values(Transition,LocalState1),
    add_post_state_values(PoststateAccess,DstNode,LocalState1,LocalState),
    b_test_boolean_expression_cs(Predicate,LocalState,CurBState,'LTL event transition',SrcNode).

check_if_all_disabled([],_Node).

check_if_all_disabled([Op|Ops],Node) :-
    \+check_enabled(Op,Node),
    check_if_all_disabled(Ops,Node).

check_if_maximum_one_enabled(OpList,Node) :-
    check_if_maximum_one_enabled(OpList,0,Node).

check_if_maximum_one_enabled([],_NrEnabled,_Node).

check_if_maximum_one_enabled([Op|Ops],NrEnabled,Node) :-
    (check_enabled(Op,Node) ->
    NrEnabled == 0, NrEnabled1 = 1
    ; NrEnabled1 = 0
    ), check_if_maximum_one_enabled(Ops,NrEnabled1,Node).

check_transition(bop(Name,NumberArgs,NumberResults,ArgPatterns,ResPatterns),
    Transition,SrcNode,_DstNode) :-
    !, functor(Op,Name,NumberArgs),
    ( NumberResults == 0 -> Transition = Op
    ;
    Transition = '-->'(Op,ReturnValues),
    length(ReturnValues,NumberResults),
    check_bop_res_patterns(ResPatterns,SrcNode,State,ReturnValues)),
    check_bop_arg_patterns(ArgPatterns,SrcNode,State,Op).

check_transition(btrans(TransPred),Transition,SrcNode,DstNode) :-
    !, check_eventb_transition(TransPred,Transition,SrcNode,DstNode).

check_transition(change_expr(Comp,TExpr),Transition,SrcNode,DstNode) :-
    !, check_change_expr_transition(Comp,TExpr,Transition,SrcNode,DstNode).

check_transition(before_after(TPred),Transition,SrcNode,DstNode) :-
    !, check_before_after_transition(TPred,Transition,SrcNode,DstNode).

check_transition(csp(Channel,Arity,Args),Transition,_SrcNode,_DstNode) :-
    !, check_csp_event(Channel,Arity,Args,Transition).

check_transition(xtl(Op,Arity,PatternArgs),Transition,_SrcNode,_DstNode) :-
    !, check_xtl_transition(Op,Arity,PatternArgs,Transition).

check_transition(Spec,_Trans,_SrcNode,_DstNode) :-
    functor(Spec,Name,Arity), add_error(ltl, 'Unknown transition specification: ', Name/Arity), fail.

check_transition_pred(operation_call(OpCall),Transition,SrcNode,TransId,DstNode) :-
    !, % check if subsidiary operation called
    (transition_info(TransId,path(Path)) % path, eventtrace, event
    -> debug_format(9,'Checking subsidiary opcall : ~w for transition id ~w : ~w~n',[OpCall,TransId, Path]),
    (path_contains_operation_call(Path,matchop(SrcNode,OpCall)) -> true
    ; check_transition(OpCall, Transition,SrcNode,DstNode)
    -> true % user has actually used it not for a subsidiary operation call but for the top-level call;
    % should we warn the user?
    )
    ; fail
).

check_transition_pred(Spec,Transition,SrcNode,_TransId,DstNode) :-
    check_transition(Spec,Transition,SrcNode,DstNode).

check_xtl_arg('_',_,TArgs,RemArgs) :- !,RemArgs=TArgs.

check_xtl_arg('?',_,TArgs,RemArgs) :- !,RemArgs=TArgs.

check_xtl_arg(X,Y,TArgs,RemArgs) :- atomic(Y),!,X=Y,RemArgs=TArgs.

check_xtl_arg(X,Y,TArgs,RemArgs) :- nonvar(Y),!,Y=..[Functor|YArgs], Functor=X,
    append(YArgs,TArgs,RemArgs).

check_xtl_arg(X,Y,TArgs,RemArgs) :- var(Y),
    print(variable_for_ltl_pattern(X)),nl,
    X=Y,RemArgs=TArgs.

check_xtl_arguments([],[]).

check_xtl_arguments([],[H|T]) :-
    print('### Extra arguments in LTL/CTL pattern: '),print([H|T]),nl,fail.

check_xtl_arguments([_H|_T],[]).

check_xtl_arguments([H|T],[PatH|PatT]) :-
    check_xtl_arg(PatH,H,T,RemArgs),
    check_xtl_arguments(RemArgs,PatT).

check_xtl_transition(Op,Arity,PatternArgs,Transition) :-
    ( Arity=0 ->
    functor(Transition,Op,_) /* in this case: pattern match any operation with right number of args */
    ; %functor(Transition,Op,Arity),
    Transition =.. [Op|Args],
    check_xtl_arguments(Args,PatternArgs)
).

compare_values(eq,V1,V2) :- equal_object(V1,V2).

compare_values(neq,V1,V2) :- not_equal_object(V1,V2).

compare_values(lt,V1,V2) :- less_than_value(V1,V2).

compare_values(gt,V1,V2) :- less_than_value(V2,V1).

eval_expr_in_state(TExpr,ID,Val) :-
    visited_expression(ID,CurState),
    state_corresponds_to_initialised_b_machine(CurState,CurBState),
    empty_state(LS),
    (b_compute_expression_nowf(TExpr,LS,CurBState,Res,'LTL unchanged expression',0) -> Res=Val
    ; add_warning(ltl,'Evaluation of unchanged expression failed: ',TExpr),
    fail).

get_por_preferences(por(TYPE,UseEnableGraph,Depth,UsePGE)) :-
    get_preference(por,TYPE),
    get_preference(enable_graph,UseEnableGraph),
    get_preference(enable_graph_depth,Depth),
    UsePGE = off.

get_primed_variable_state(SrcNode,PrimedVarBindings) :-
    visited_expression(SrcNode,SrcState),
    extract_variables_from_state_as_primed(SrcState,PrimedVarBindings).

is_atomic_ltl_property(ap(_)).

is_atomic_ltl_property(false).

is_atomic_ltl_property(true).

is_atomic_ltl_property(not(P1)) :- is_atomic_ltl_property(P1).

is_atomic_ltl_property(and(P1,P2)) :- is_atomic_ltl_property(P1),is_atomic_ltl_property(P2).

is_atomic_ltl_property(or(P1,P2)) :- is_atomic_ltl_property(P1),is_atomic_ltl_property(P2).

is_atomic_ltl_property(equivalent(P1,P2)) :- is_atomic_ltl_property(P1),is_atomic_ltl_property(P2).

is_atomic_ltl_property(implies(P1,P2)) :- is_atomic_ltl_property(P1),is_atomic_ltl_property(P2).

is_exactly_one_operation_enabled(OpList,Node) :-
    is_exactly_one_operation_enabled(OpList,0,Node).

is_exactly_one_operation_enabled([],NrEnabled,_Node) :-
    NrEnabled=1.

is_exactly_one_operation_enabled([Op|Ops],NrEnabled,Node) :-
    (check_enabled(Op,Node) ->
    NrEnabled == 0, NrEnabled1 = 1
    ; NrEnabled1 = NrEnabled
    ), is_exactly_one_operation_enabled(Ops,NrEnabled1,Node).

is_set([]).

is_set([_|_]).

is_set(avl_set(_)).

is_set(closure(_,_,_)).

less_than_value(int(V1),int(V2)) :- !, V1 < V2.

less_than_value(pred_false,V2) :- !, V2=pred_true.

less_than_value(pred_true,_) :- !, fail.

less_than_value(string(V1),string(V2)) :- !, V1 @< V2.

less_than_value(fd(V1,G),fd(V2,G)) :- !, V1 < V2.

less_than_value((V1a,V1b),(V2a,V2b)) :- !,
    (less_than_value(V1a,V2a) -> true
    ; equal_object(V1a,V2a) -> less_than_value(V1b,V2b)).

less_than_value(V1,V2) :- is_set(V1), !, strict_subset_of(V1,V2).

less_than_value(R1,R2) :- is_real(R1), !, real_less_than_wf(R1,R2,no_wf_available).

less_than_value(V1,_) :- add_error(ltl,'Operator increasing/decreasing not supported for:',V1).

non_det_output_transition(ID,OperationName,TID1,TID2) :-
    impl_trans_id(ID,Transition,TID1,_ID1),
    get_operation_name(Transition,OperationName),
    get_operation_return_values_and_arguments(Transition,Results1,OperationArgs),
    Results1 \= [], % otherwise we have no return value
    impl_trans_id(ID,Transition2,TID2,_ID2),
    TID2 > TID1,
    % note: here we do not care whether ID1 \= ID2,
    get_operation_name(Transition2,OperationName), % same operation
    get_operation_return_values_and_arguments(Transition2,Results2,OperationArgs), % same arguments
    Results1 \= Results2. % Should we use equal_object ?

parameter_values(Transition,LocalState) :-
    Transition =.. [Name|Arguments],
    b_get_machine_operation(Name,_,Parameters,_),
    empty_state(Empty),
    add_parameter_values2(Parameters,Arguments,Empty,LocalState).

path_contains_operation_call(path(S),Pat) :- !, path_contains_operation_call(S,Pat).

path_contains_operation_call([H|T],Pat) :- !, member(S,[H|T]), path_contains_operation_call(S,Pat).

path_contains_operation_call(parallel(L),Pat) :- !, member(S,L), path_contains_operation_call(S,Pat).

path_contains_operation_call(sequence(A,B),Pat) :- !, member(S,[A,B]), path_contains_operation_call(S,Pat).

path_contains_operation_call(assertion(S),Pat) :- !, path_contains_operation_call(S,Pat).

path_contains_operation_call(pre(_,S),Pat) :- !, path_contains_operation_call(S,Pat).

path_contains_operation_call(choice(_,S),Pat) :- !, path_contains_operation_call(S,Pat).

path_contains_operation_call(if(_,S),Pat) :- !, path_contains_operation_call(S,Pat).

path_contains_operation_call(select(_,S),Pat) :- !, path_contains_operation_call(S,Pat).

path_contains_operation_call(let(S),Pat) :- !, path_contains_operation_call(S,Pat).

path_contains_operation_call(any(_,S),Pat) :- !, path_contains_operation_call(S,Pat).

path_contains_operation_call(var(_,S),Pat) :- !, path_contains_operation_call(S,Pat).

path_contains_operation_call(operation_call(Name,_ResultNames,Paras,ReturnValues, Path),Pat) :- !,
    %write(opcall(Name)),nl,
    (Pat = matchop(SrcNode,bop(Name,_NumberArgs,_NumberResults,ArgPatterns,ResPatterns)),
    Op =.. [Name|Paras],
    check_bop_arg_patterns(ArgPatterns,SrcNode,State,Op), % State instantiated upon demand
    check_bop_res_patterns(ResPatterns,SrcNode,State,ReturnValues)
    -> true
    ; path_contains_operation_call(Path,Pat)).

trans(A,B,Op,TransID) :- impl_trans_term(A,Op,TransID,B).