ltl_prepositions

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).

check_ap(promela_pred(Predicate),Node) :-
    visited_expression(Node,State),!,
    eval_promela(Predicate,global,State,Result),!,
    ( Result == 0 -> fail
    ; number(Result) -> true
    ; otherwise -> add_error(ltl,'Promela eval returned a non-boolean value: ',Result),fail).

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(deadlock,Node) :- !, \+ trans(Node,_,_).

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

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

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) ;
    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(not(P1),NodeId) :- !,
    (check_atomic_property_formula(P1,NodeId) -> fail ; true).

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)
    ; otherwise -> true),
    empty_state(LS),
    b_compute_expression(Expr,LS,State,PatternValue),
    equal_object(PatternValue,OpValue),!.

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_enabled(Spec,SrcNode) :-
    check_transition(Spec,Transition,SrcNode,DestNode),
    trans(SrcNode,DestNode,Transition),!.

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_wf(Predicate,LocalState,CurBState).

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
    ; otherwise ->
    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(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(plugin_transition_check(Id,Predicate),Transition,_SrcNode,_DstNode) :-
    !, plugin_evaluate_transition_predicate(Id,Predicate,Transition).

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

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],[]) :- print(ltl_check_xtl_arguments_ignoring([H|T])),nl.

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)
).

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).

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

trans(A,B,Op) :-
    ( (preference(use_por_for_ltl,true), animation_mode(b))
    -> ltl: get_por_preferences(POROptions), % poor implementation (ltl predicates should not be called from here)
    user: compute_ample_set2(A,POROptions),
    transition(A,Op,B) % from state_space.pl
    ; impl_trans_term(A,Op,B) /* will automatically compute as required */
).