specfile

add_animation_minor_mode(X) :-
    (animation_minor_mode(X) -> true ; assertz(animation_minor_mode(X))).

animation_mode(b).

b_absolute_file_name_relative_to_opened_file(File,AbsFileName) :-
    currently_opened_file_status(MainFileName,_Status), % _Status=failure happens when error during loading
    get_parent_directory(MainFileName,Directory),
    safe_absolute_file_name(File,AbsFileName,[relative_to(Directory)]).

b_mode :- animation_mode(X), (X=b ; X=csp_and_b).

b_or_z_mode :-
    (animation_mode(X) -> (X=b -> true ; X=csp_and_b)). % basically the same as b_mode

b_or_z_mode(b). b_or_z_mode(csp_and_b).

b_or_z_mode(b). b_or_z_mode(csp_and_b).

b_possible_trans_name(root,OpName) :- !,
    (b_machine_has_constants_or_properties
    -> OpName = '$setup_constants'
    ; OpName = '$initialise_machine').

b_possible_trans_name(concrete_constants(_),OpName) :- !, OpName = '$initialise_machine'.

b_possible_trans_name(_State,OpName) :-
    (preferences:preference(randomise_operation_order,true),random(1,3,1)
    -> b_machine_operation_names_in_reverse_order(OpName) ; true),
    %b_get_machine_operation(OpName,_Res,_Params,_,_,_).
    b_top_level_feasible_operation(OpName). % TO DO: we could link also with cbc feasibility analysis if carried out

b_preference_par('MAXINT','=',MaxInt) :- get_preference(maxint,MaxInt).

b_preference_par('MININT','=',MinInt) :- get_preference(minint,MinInt).

b_preference_par(card(GlobalSet),Op,Card) :-
    b_global_set(GlobalSet),
    b_fd_card(GlobalSet,RCard),
    % provide feedback if unfixed_deferred_set
    (inferred_maximum_global_set_cardinality(GlobalSet,MaxCard),
    (inferred_minimum_global_set_cardinality(GlobalSet,MinCard) -> true ; MinCard=1),
    MinCard \= MaxCard,
    Op = ':', Card = '..'(MinCard,MaxCard)
   
    ;
   
    inferred_minimum_global_set_cardinality(GlobalSet,MinCard),
    \+ (inferred_maximum_global_set_cardinality(GlobalSet,_)),
    Op='>=',Card=MinCard % show minimum cardinality info
   
    ;
   
    Op= '=', (unfixed_deferred_set(GlobalSet)
    -> ajoin([RCard,' (assumed for deferred set)'],Card) ; Card=RCard)
).

b_property(root,Prop) :- !, b_preference_par(PARA,Op,VAL), Prop=.. [Op,PARA,VAL].

b_property([H|T],non_ground(Var)) :- debug:debug_mode(on),
    member(bind(Var,Val),[H|T]),\+(ground(Val)).

b_property([H|T],Prop) :- elementary_prop([H|T],Prop).

b_property([],Prop) :- elementary_prop([],Prop).

b_property(concrete_constants(DB),Prop) :- elementary_prop(DB,Prop).

b_syntax_available_for_source :-
    b_or_z_mode,
    (animation_minor_mode(X) -> X=event_b ; true).

b_trans(State,OpName,Operation,NewState,PathInfo) :-
    compute_operation_effect_max(State,OpName,Operation,NewState,PathInfo,_Max).

b_transition_for_csp(ChOpName,_CSPAction,ChArgs,OpArgs,BState,OpName,Operation,NewB,TransInfo) :-
    build_up_b_operation_for_csp(ChOpName,OpArgs,Operation),
    !,
    OpName = ChOpName,
    %% print_message(trying_b_trans(Operation,ChArgs,OpArgs)),
    (get_preference(try_operation_reuse,false)
    -> generate_b_operationargs_from_csp(ChArgs,OpArgs),
    b_trans(BState,OpName,Operation,NewB,TransInfo)
    ;
    % compute B transition without parameters so that we can cache
    b_trans(BState,OpName,Operation,NewB,TransInfo),
    % and unify afterwards
    generate_b_operationargs_from_csp(ChArgs,OpArgs)
).

b_transition_for_csp(ChOpName,_CSPAction,ChArgs,OpArgs,BState,OpName,Operation,NewB,TransInfo) :-
    OpName = ChOpName,
    (b_is_variable(ChOpName) ; b_is_constant(ChOpName)),
    %% print(probing(ChOpName)),nl,
    expand_const_and_vars_to_full_store(BState,FBState),
    try_lookup_value_in_store_and_global_sets(ChOpName,FBState,IdValue),
    !,
    remove_infos_from_prepared_state(BState,NewB),
    TransInfo=[],
    /* interpret as probing operation: get value of var,cst,SET */
    generate_b_operationargs_from_csp(ChArgs,OpArgs),
    (OpArgs=[SingleVal]
    -> SingleVal = IdValue, Operation='-->'(ChOpName,[IdValue])
    ; OpArgs=[Val1,Val2],
    tuple_of(Val1,Val2,IdValue), /* from bsets_clp, use exact_element_of ??? */
    OpCall =.. [ChOpName,Val1],
    Operation='-->'(OpCall,[Val2])
).

b_transition_for_csp(_ChOpName,CSPAction,_ChArgs,_OpArgs,BState,OpName,Operation,NewB,TransInfo) :-
    OpName = '$CSP', % all CSP events grouped together
    remove_infos_from_prepared_state(BState,NewB),
    TransInfo=[],
    /* no B operation of the name; could be tau or tick or extra comm channel */
    %Op1 =.. [ChOpName|OpArgs],
    Operation = CSPAction. % removed csp(.) wrapper [for LTL model checker]

build_up_b_operation_for_csp(OpName,OpArgs,Operation) :- %print(csp(OpName,OpArgs,Operation)),nl,
    nonvar(OpName),
    b_get_machine_operation(OpName,Res,Params,_), %print(get_machine_op(OpName,Res,Params)),nl,
    specfile:generate_args(OpArgs,Params,Res, BArgs,BResults,OpName), %print(gen_args(BArgs,BResults)),nl,
    % TO DO: either also extract types from Params, Res or better write a static checker that tests that the B operation and CSP channel types are compatible
    safe_univ(Op1,[OpName|BArgs]), %print(op1(Op1)),nl,
    (BResults = [] -> Operation = Op1 ; Operation = '-->'(Op1,BResults)).

build_up_b_real_operation(OpName,Operation) :-
    b_get_machine_operation_for_animation(OpName,Res,Params,_,_,true), %true==TopLevel
    length(Params,Len), length(OpArgs,Len),
    length(Res,RLen), length(BResults,RLen),
    safe_univ(Op1,[OpName|OpArgs]),
    (BResults = [] -> Operation = Op1 ; Operation = '-->'(Op1,BResults)).

check_compatibility(b(identifier(ID),TYPE,INFO),CSP_TYPE,ChannelOpName) :- !,
    (type_ok(TYPE,CSP_TYPE) -> true ;
    % TO DO: pretty print B and CSP Types
    add_error(type_check_csp_and_b,'Incompatible types between B and CSP: ',ChannelOpName:ID:(TYPE:CSP_TYPE),b(identifier(ID),TYPE,INFO))
).

check_compatibility(B,CSP,ChannelOpName) :- !,
    add_internal_error('Illegal types: ',check_compatibility(B,CSP,ChannelOpName)).

check_rest_couple([B],TB) :- !, type_ok(TB,B).

check_rest_couple([B1|BRest],couple(TB1,TBRest)) :- type_ok(TB1,B1),
    check_rest_couple(BRest,TBRest).

check_rest_couple_els([B],TB) :- !, type_ok(TB,setValue([B])).

check_rest_couple_els([B1|BRest],couple(TB1,TBRest)) :- type_ok(TB1,setValue([B1])),
    check_rest_couple_els(BRest,TBRest).

check_type(boolean,pred_true,_) :- !.

check_type(boolean,pred_false,_) :- !.

check_type(integer,int(_),_) :- !.

check_type(string,string(_),_) :- !.

check_type(global(GS),fd(_,GS),_) :- !.

check_type(couple(A,B),(VA,VB),OID) :- !, check_type(A,VA,OID), check_type(B,VB,OID).

check_type(set(_T),[],_) :- !.

check_type(set(_T),closure(_,_,_),_) :- !. % TO DO: check type signature of closure

check_type(set(T),[H|_],OID) :- !, check_type(T,H,OID).

check_type(set(T),avl_set((node(Y,_,_,_L,_R))),OID) :- !, check_type(T,Y,OID).

check_type(seq(T),V,OID) :- !, check_type(set(couple(integer,T)),V,OID).

check_type(Type,Value,OpName:TID) :-
    def_get_texpr_id(TID,ID),
    add_error(check_type_for_id,'Illegal CSP value for argument: ',OpName:ID:type(Type):value(Value)),
    fail.

check_type_for_id(Val,TID,OpName) :- get_texpr_type(TID,Type),
    check_type(Type,Val,OpName:TID).

choose_loaded_solution(Stores,ConstantsStore,_MaxReached) :-
    member(ConstantsStore,Stores).

choose_loaded_solution(_Stores,_ConstantsStore,true) :-
    % provoke the setting of the "maximum reached flag"
    succeed_max_call_id('$setup_constants',member(_,_),1),fail.

classical_b_mode :- b_mode, (animation_minor_mode(Mode) -> classical_minor_mode(Mode) ; true).

classical_minor_mode(rules_dsl).

compute_constants(ConstantsStore,_Max,C) :-
    % check if values have been computed and stored into a file before -- if yes, use them
    load_constants(Stores,MaxReached),!,
    C = complete_properties, % TODO: check that only complete properties stored or that we store this info
    choose_loaded_solution(Stores,ConstantsStore,MaxReached).

compute_constants(ConstantsStore,Max,Complete) :-
    % print('Searching for valid CONSTANTS'),nl,!,
    succeed_max_call_id('$setup_constants',b_interpreter:b_set_up_concrete_constants(ConstantsStore,Complete),Max).

compute_operation_effect_max([],OpName,Operation,NewState,PathInfo,Max) :-
    compute_operation_updates_on_expanded_store([],OpName,Operation,Updates,PathInfo,Max),
    store_updates_and_normalise(Updates,[],NewState).

compute_operation_effect_max([H|T],OpName,Operation,NewState,PathInfo,Max) :-
    compute_operation_updates_on_expanded_store([H|T],OpName,Operation,Updates,PathInfo,Max),
    store_updates_and_normalise(Updates,[H|T],NewState).

compute_operation_effect_max(const_and_vars(ConstID,Vars),OpName,Operation,ResultingStore,PathInfo,Max) :-
    prepare_state_for_specfile_trans(const_and_vars(ConstID,Vars),unknown,R),
    %print(expanded_const_and_vars(ConstID)),nl,
    compute_operation_effect_max(R,OpName,Operation,ResultingStore,PathInfo,Max).

compute_operation_effect_max(expanded_const_and_vars(ID,Vars,FullStore,Infos),OpName,Operation,NewState,PathInfo,Max) :-
    compute_operation_updates_on_expanded_store(expanded_const_and_vars(ID,Vars,FullStore,Infos),
    OpName,Operation,Updates,PathInfo,Max),
    NewState = const_and_vars(ID,NewVars),
    store_updates_and_normalise(Updates,Vars,NewVars).

compute_operation_effect_max(expanded_vars(FullStore,Infos),OpName,Operation,NewState,PathInfo,Max) :-
    compute_operation_updates_on_expanded_store(expanded_vars(FullStore,Infos),
    OpName,Operation,Updates,PathInfo,Max),
    store_updates_and_normalise(Updates,FullStore,NewState).

compute_operation_effect_max(concrete_constants(ConstantsStore),'$initialise_machine',OpInit,ResultingStore,PathInfo,Max) :-
    get_max_enablings_for_init(Max,'$initialise_machine',MaxForCall),
    succeed_max_call_id('$initialise_machine',
    b_interpreter:b_initialise_machine(ConstantsStore,InitialVars,InitialStore,PathInfo),MaxForCall),
    create_initialisation_operation(InitialVars,OpInit),
    (\+ preferences:preference(symmetry_mode,flood), /* TO DO : improve permutation to allow using const_and_vars optimisation */
    visited_expression(ConstID,concrete_constants(ConstantsStore))
    -> ResultingStore = const_and_vars(ConstID,InitialVars) /* avoid storing constant values again */
    ; ResultingStore = InitialStore).

compute_operation_effect_max(root,'$setup_constants',OpSetup,concrete_constants(FilteredConstantsStore),[],Max) :-
    b_machine_has_constants_or_properties,
    get_max_enablings_for_init(Max,'$setup_constants',MaxForCall),
    compute_constants(ConstantsStore,MaxForCall,Complete),
    create_setup_constants_operation(ConstantsStore,Complete,OpSetup),
    %%print_message('FOUND_CONSTANTS'(OpName)),
    (get_preference(filter_unused_constants,true) % possibly disable if VisB or Custom Graph Definitions exist
    -> exclude(unused_binding,ConstantsStore,FilteredConstantsStore)
    ; FilteredConstantsStore=ConstantsStore).

compute_operation_effect_max(root,'$initialise_machine',OpInit,InitialStore,PathInfo,Max) :-
    \+ b_machine_has_constants_or_properties,
    get_max_enablings_for_init(Max,'$initialise_machine',MaxForCall),
    empty_state(EmptyState),
    succeed_max_call_id('$initialise_machine',
    b_interpreter:b_initialise_machine(EmptyState,InitialVars,InitialStore,PathInfo),MaxForCall),
    create_initialisation_operation(InitialVars,OpInit).

compute_operation_on_expanded_store2(InState,OpName,Operation,Updates,PathInfo,Max) :-
    get_max_enablings_per_operation(Max,OpName,MaxForCall),
    succeed_max_call_id(OpName,
    b_interpreter:b_execute_top_level_operation_update(OpName,Operation,InState,Updates,PathInfo),
    MaxForCall).

compute_operation_updates_on_expanded_store(InState,OpName,Operation,NewState,PathInfo,Max) :-
    get_preference(try_operation_reuse,V), V \= false,
    b_or_z_mode, % now works with CSP || B
    %\+ animation_minor_mode(eventb), % projection used to confuse Event-B interpreter, see test 2138
    !,
    get_max_enablings_per_operation(Max,OpName,MaxForCall),
    compute_operation_on_expanded_store_cache(OpName,Operation,InState,NewState,PathInfo,MaxForCall).

compute_operation_updates_on_expanded_store(Store,OpName,Operation,Updates,PathInfo,Max) :-
    extract_full_store(Store,FullStore),!,
    compute_operation_on_expanded_store2(FullStore,OpName,Operation,Updates,PathInfo,Max).

compute_operation_updates_on_expanded_store(InState,OpName,Operation,Updates,PathInfo,Max) :-
    compute_operation_on_expanded_store2(InState,OpName,Operation,Updates,PathInfo,Max).

couple_int(couple(integer, T), T). % possible sequence

create_initialisation_operation(_InitialVars,'$initialise_machine').

create_local_store_for_operation([],[],_,Store) :- !, Store=[].

create_local_store_for_operation([Name|NT],[Val|VT],OpName,[bind(Name,Val)|StoreT]) :- !,
    create_local_store_for_operation(NT,VT,OpName,StoreT).

create_local_store_for_operation([Name|NT],[],OpName,Store) :- !,
    ajoin(['Missing values for operation ',OpName,':'],Msg),
    add_error(specfile,Msg,[Name|NT]),
    Store = [].

create_local_store_for_operation(_,V,OpName,Store) :-
    ajoin(['Too many values for operation ',OpName,':'],Msg),
    add_error(specfile,Msg,V),
    Store = [].

create_setup_constants_operation(_ConstantVars,complete_properties,R) :- !, R='$setup_constants'.

create_setup_constants_operation(_ConstantVars,_,'$partial_setup_constants').

create_value('...',_,R) :- !, R = b(string('...'),string,[]).

create_value(X,T,R) :-
    create_texpr(value(X),T,[],R).

csp_and_b_transition(root,OpName,Op,NewState,TransInfo) :- !,
    Op = start_cspm_MAIN, OpName=Op, NewState = csp_and_b_root,TransInfo = [].

csp_and_b_transition(csp_and_b_root,OpName,Trans,NewState,TransInfo) :- !,
    Trans = tau(Op), OpName = '$CSP',
    b_trans(root,_,Op,InitialBState,TransInfo),
    (InitialBState = concrete_constants(_)
    -> NewState = InitialBState
    ; csp_initialisation_for_b(InitialCSPState),
    NewState = csp_and_b(InitialCSPState,InitialBState)
).

csp_and_b_transition(concrete_constants(C),OpName,Trans,NewState,TransInfo) :- !,
    Trans = tau(Op), OpName = '$CSP',
    b_trans(concrete_constants(C),_,Op,InitialBState,TransInfo),
    csp_initialisation_for_b(InitialCSPState),
    NewState = csp_and_b(InitialCSPState,InitialBState).

csp_and_b_transition(csp_and_b(CSPState,BState),OpName,EventVisibleToUser,csp_and_b(NewCSP,NewB),TransInfo) :-
    !,
    csp_transition_for_b(CSPState,ChOpName,ChArgs,CSPAction,NewCSP),
    % TO DO: split up csp_transition_for_b: into two parts; second part converts datatypes and only called if linking op exists
    %% print(csp_trans(ChOpName,ChArgs)),nl,
    length(ChArgs,Len), length(OpArgs,Len),
    b_transition_for_csp(ChOpName,CSPAction,ChArgs,OpArgs,BState,OpName,Operation,NewB,TransInfo),
    hide_csp_event(CSPAction,Operation,EventVisibleToUser).

csp_and_b_transition(State,'$CSP',Op,NewState,[]) :-
    % we have a pure CSP state: use CSP-M transition
    cspm_transition(State,Op,NewState).

csp_b_possible_trans_name(csp_and_b_root,OpName) :- !,
    (b_machine_has_constants_or_properties
    -> OpName = 'tau($setup_constants)'
    ; OpName = 'tau($initialise_machine)').

csp_b_possible_trans_name(concrete_constants(_),OpName) :- !,
    OpName = 'tau($initialise_machine)'.

csp_b_possible_trans_name(State,OpName) :-
    b_possible_trans_name(State,OpName).

csp_mode :- animation_mode(X), csp_mode(X).

csp_mode(cspm).

csp_mode(csp_and_b).

csp_with_bz_mode :- animation_mode(csp_and_b).

current_b_expression(CurBState) :-
    current_expression(_CurID,CurState),
    state_corresponds_to_set_up_constants(CurState,CurBState).

currently_opened_file(File) :- currently_opened_file_status(File,success).

dom_range_type(seq(R),integer,R).

dom_range_type(set(couple(D,R)),D,R).

elementary_fun_prop(Val,Var,Prop) :-
    simple(Prop), % will only succeed if Prop is var or atom; translate_bexpression will raise error if Prop is compound
    nonvar(Val),
    (var_cst_type(Var,Type),dom_range_type(Type,Dom,Ran) -> true ; Type=any,Dom=any, Ran=any),
    get_relation_element(Val,X,Y), % Show value in form: Var(X) = Y
    create_texpr(identifier(Var),Type,[],Fun),
    create_value(X,Dom,Arg),
    create_texpr(function(Fun,Arg),Ran,[],Lhs),
    create_value(Y,Ran,Rhs),
    create_texpr(equal(Lhs,Rhs),pred,[],Expr),
    translate_bexpression_with_limit(Expr,80,Prop).

elementary_prop(DB,Prop) :-
    member(bind(Var,Val),DB), %print(var_prop(Var)),nl_time,
    elementary_prop3(Val,Var,Prop).

elementary_prop3(Val,Var,Prop) :- var(Val),!, Prop = '='(Var,'_VAR_').

elementary_prop3(avl_set(Avl),Var,Prop) :- !,
    (show_avl_set(Avl) % \+ custom_explicit_sets:is_avl_sequence(Avl))
    -> elementary_fun_prop(avl_set(Avl),Var,Prop)
    ; elementary_var_prop(avl_set(Avl),Var,Prop)).

elementary_prop3([H|T],Var,Prop) :- H=(_,_),
    get_preference(show_function_tuples_in_property,true),!,
    elementary_fun_prop([H|T],Var,Prop).

elementary_prop3(Val,Var,Prop) :- elementary_var_prop(Val,Var,Prop).

elementary_var_prop(Val,Var,Prop) :-
    % TODO: use translate:translate_bvalue_for_expression/3
    animation_minor_mode(tla),!,
    ( identifier_has_tla_type(Var,TlaType) ->
    translate_bvalue_with_tlatype(Val,TlaType,Text)
    ;
    translate_bvalue(Val,Text)),
    Prop = '='(Var,Text).

elementary_var_prop(Val,Var,Prop) :-
    (var_cst_type(Var,Type)
    -> translate_bvalue_with_type_and_limit(Val,Type,320,Text)
    ; translate_bvalue_with_type_and_limit(Val,any,320,Text)), % translate_properties_with_limit uses 320 Limit
    Prop = '='(Var,Text).

eventb_mode :-
    animation_mode(X), (X=b ; X=csp_and_b),
    animation_minor_mode(eventb).