b_read_write_info

accessed_vars_for_operation_call(MVars,NonDetMVars,RVars,LocalVars,Results,Arguments) -->
    add_non_local_modified_vars(MVars,LocalVars),
    add_non_local_read_vars(RVars,LocalVars),
    add_modified_vars(Results,LocalVars),
    add_non_local_non_det_modified_vars(NonDetMVars,LocalVars),
    add_read_vars_l(Arguments,LocalVars).

add_delta_modified_to_non_det_modified(ModIn,mrinfo(ModOut,NonDet,Read),mrinfo(ModOut,NonDet2,Read)) :-
    add_modified_to_non_det_modified(ModIn,ModOut,NonDet,NonDet2).

add_dollar_zero(Id,rename(P,Id)) :-
    number_suffix(Id,0,P).

add_modified_to_non_det_modified(ModIn,ModOut,NDOut,NDOut2) :-
    ord_subtract(ModOut,ModIn,Delta), % these variables were detected as written
    ord_union(Delta,NDOut,NDOut2).

add_modified_vars(Ids,LocalVars) -->
    {filter_result_vars(Ids,LocalVars,ModifiedVars)},
    add_modified_vars2(ModifiedVars).

add_modified_vars2(Vars,In,Res) :-
    (var(Vars)
    -> add_internal_error('Modified Vars variable: ',add_modified_vars2(Vars,In,Res))
    ; true),
    In = mrinfo(InModified,NonDetModified,Read),
    Res = mrinfo(OutModified,NonDetModified,Read),
    list_to_ord_set(Vars,SVars),
    my_ord_union(SVars,InModified,OutModified).

add_non_det_modified_vars(Ids,LocalVars) -->
    {filter_result_vars(Ids,LocalVars,ModifiedVars)},
    {list_to_ord_set(ModifiedVars,SModifiedVars)},
    add_non_det_modified_vars2(SModifiedVars).

add_non_det_modified_vars2(Vars,In,Res) :-
    (var(Vars)
    -> add_internal_error('Modified Vars variable: ',add_non_det_modified_vars2(Vars,In,Res))
    ; true),
    In = mrinfo(InModified,InNonDetModified,Read),
    Res = mrinfo(OutModified,OutNonDetModified,Read),
    my_ord_union(Vars,InModified,OutModified),
    my_ord_union(Vars,InNonDetModified,OutNonDetModified).

add_non_local_modified_vars(WriteVars,LocalVars) -->
    {ord_subtract(WriteVars,LocalVars,AddVars)},
    add_modified_vars2(AddVars).

add_non_local_non_det_modified_vars(WriteVars,LocalVars) -->
    {ord_subtract(WriteVars,LocalVars,AddVars)},
    add_non_det_modified_vars2(AddVars).

add_non_local_read_vars(ReadVars,LocalVars) -->
    {ord_subtract(ReadVars,LocalVars,AddVars)},
    add_read_vars2(AddVars).

add_read_vars(Expression,LocalVars) -->
    {find_identifier_uses(Expression,LocalVars,ReadVars)}, % TOOD: here we can have operation_call_in_expr with non-ground reads info!
    add_read_vars2(ReadVars).

add_read_vars2(SVars,mrinfo(Modified,NonDetModified,InRead),
    mrinfo(Modified,NonDetModified,OutRead)) :- my_ord_union(SVars,InRead,OutRead).

add_read_vars_l([],_LocalVars) --> !.

add_read_vars_l([Expr|Rest],LocalVars) --> !,
    add_read_vars(Expr,LocalVars),
    add_read_vars_l(Rest,LocalVars).

add_read_vars_l(E,LV) --> !, {add_internal_error('Not a list: ',add_read_vars_l(E,LV,_,_))}.

add_tvars_to_ord_list(SortedVars,TIds,NewVars,X,X) :-
    get_texpr_ids(TIds,Ids),
    list_to_ord_set(Ids,SIds),
    my_ord_union(SortedVars,SIds,NewVars).

add_variant_status_aux(convergent(VariantExpr),LocalVars) --> !,
    add_read_vars(VariantExpr,LocalVars).

add_variant_status_aux(anticipated(VariantExpr),LocalVars) --> !,
    add_read_vars(VariantExpr,LocalVars).

add_variant_status_aux(ordinary,_) --> !, [].

add_variant_status_aux(Status,_) --> {add_warning(b_read_write_info,'Unrecognised VARIANT status: ',Status)}.

add_variant_status_read_vars(b(Status,status,_Info),LocalVars) -->
    % TO DO: if member(convergence_proved,Info) should we add the vars?
    add_variant_status_aux(Status,LocalVars).

add_witness_read_vars(b(witness(ID,Predicate),witness,_),LocalVars) --> !,
    % a parameter witness talks about a parameter no longer there: it is not really read here, but the predicate is used to set the any local parameter in another context
    % a variable witness alks about a variable non-deterministically assigned in the abstraction; we also pretend it is not read here (but assigned somewhere else)
    add_tvars_to_ord_list(LocalVars,[ID],LocalVars2), % we add ID to local variables not read "really" read here
    %{print(witness_add_read_vars(ID)),nl},
    add_read_vars(Predicate,LocalVars2).

add_witness_read_vars_l([],_LocalVars) --> !.

add_witness_read_vars_l([Expr|Rest],LocalVars) -->
    add_witness_read_vars(Expr,LocalVars), !,
    add_witness_read_vars_l(Rest,LocalVars).

add_witness_read_vars_l(E,LV) --> !, {add_internal_error('Not a witness list: ',add_witness_read_vars_l(E,LV,_,_))}.

b_get_machine_operation_with_local_paras(OpName,AllLocalParas,Body) :-
    b_get_machine_operation(OpName,Results,Parameters,Body),
    append(Parameters,Results,TP),
    get_texpr_ids(TP,TPIds),
    list_to_ord_set(TPIds,AllLocalParas).

b_get_operation_read_guard_vars(Operation,JustVariables,VarsResult,VarsPrecise) :-
    (var(Operation) -> b_is_operation_name(Operation) ; true),
    b_get_operation_read_guard_vars2(Operation,JustVariables,VarsResult,VarsPrecise).

b_get_operation_read_guard_vars2(Operation,JustVariables,VarsResult,VarsPrecise) :-
    b_get_operation_read_guard_vars_cache(Operation,JustVariables,R,P),!,
    VarsResult=R, VarsPrecise=P.

b_get_operation_read_guard_vars2(Operation,JustVariables,VarsResult,VarsPrecise) :-
    b_get_machine_operation_with_local_paras(Operation,Paras,_),
    get_operation_guard(Operation,G,Precise),
    % RGuardVars can comprise also local variables by operations with parameters
    find_identifier_uses(G,Paras,RGuardVars),
    list_to_ord_set(RGuardVars,ReadGuard),
    (JustVariables=false
    -> Result = ReadGuard
    ; b_get_machine_variables(TVars),get_texpr_ids(TVars,Vars),
    list_to_ord_set(Vars,Variables),
    ord_intersection(ReadGuard,Variables,Result)
    ),
    assertz(b_get_operation_read_guard_vars_cache(Operation,JustVariables,Result,Precise)),
    VarsResult=Result, VarsPrecise=Precise.

b_get_read_guard_variables(ReadVariables) :-
    findall(Var,
    (b_top_level_operation(Operation),
    b_get_operation_read_guard_vars(Operation,true,ReadV,_),
    member(Var,ReadV),
    b_is_variable(Var)
    ),Vars),
    sort(Vars,ReadVariables).

b_get_read_may_must_write(Operation,MustWriteV,MayWriteV) :-
    b_get_machine_operation(Operation,ReturnVars,_P,Body),
    b_get_read_write(Operation,_,WriteV),
    (is_eventb_event(Body) -> MayWriteV = [],
    WriteV = MustWriteV % in Event-B there are no conditions on the actions
    ; extract_must_write(Body,nested,MustWriteV1) ->
    % remove return values: they are not global variables written to
    def_get_texpr_ids(ReturnVars,RV),list_to_ord_set(RV,SRV),
    ord_subtract(MustWriteV1,SRV,MustWriteV),
    ord_subtract(WriteV,MustWriteV,MayWriteV)
    ; add_internal_error('Extraction of Must-Write failed: ',extract_must_write(Body,nested,_)),
    MustWriteV=[], MayWriteV=WriteV).

b_get_read_may_must_write_for_ltsmin(Operation,ReadsGuard,ReadsAction,MustW,MayW) :-
    get_operation(Operation,Results,Paras),
    % LTSmin needs the constants in the read matrices;
    % if they are not included, it will transfer the uninitialised constants from the root state
    %b_get_machine_constants(TConsts), append(Paras,TConsts,TP),
    append(Results, Paras, ResultsAndParas),
    get_texpr_ids(ResultsAndParas,TPIds),
    get_global_identifiers(Global),
    append(TPIds,Global,PIDs),list_to_ord_set(PIDs,VarsToIgnore), % the VarsToIgnore should not be included in the matrix
    b_get_read_may_must_write(Operation,MustW,MayW), % we ignore the info about guards and actions: LTS Min has another definition of what a guard is than b_get_read_may_must_write
    get_operation_propositional_guards(Operation,Guards,RestBody), % obtain LTSMin guards, which are independent of the parameters
    get_accessed_vars(RestBody,VarsToIgnore,_Modified,ReadsAction), % this computes the ReadsAction the LTSMin way
    %format('READS ACTION for ~w ~n ~w~n',[Operation,ReadsAction]),
    conjunct_predicates(Guards,G),
    find_identifier_uses(G,VarsToIgnore,ReadsGuard).

b_get_read_variables(ReadVariables) :-
    findall(Var,
    (b_top_level_operation(Operation),
    b_get_read_write(Operation,ReadV,_),
    member(Var,ReadV),
    b_is_variable(Var)
    ),Vars),
    sort(Vars,ReadVariables).

b_get_read_write(O,R,W) :-
    if(b_get_operation_normalized_read_write_info(O,R,W),true,
    (R,W)=('$all','$all')). % it used to be that in Event-B no read information was stored; all calls to b_get_operation_normalized_read_write_info failed; has been fixed

b_get_read_write_guard_action(Operation,ReadGuard,ReadAction,Read,Write) :-
    b_get_read_write(Operation,Read,Write),
    b_get_operation_read_guard_vars(Operation,false,ReadGuard,_Precise),
    b_get_machine_operation_with_local_paras(Operation,LocalParas,Body),
    get_texpr_expr(Body,RLEVENT),
    (RLEVENT = rlevent(_Name,_Section,_Stat,_Parameters,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,_AbsEvents) ->
    % special code to deal with *all* guards/actions (also in abstractions) + not extract guards from actions
    % TO DO: maybe move this to get_guard/get_action (see below) ; or maybe provide parameter to choose
    % in some circumstances (Deadlock checking) it is sufficient to look at lowest refinement level
    % for LTSMin,... : we need info from all refinement levels and from theorems
    % TO DO: look at _Unmod
    findall(A1,(get_full_eventb_action(RLEVENT,AA),member(A1,AA)),A)
    ; get_action(Operation,A) -> true
    ; add_error(b_get_read_write_guard_action,'Could not get action for operation: ',Operation), fail
    ),
    (is_list(A) % in case of Event-B events the action block is a list of assignments
    -> find_identifier_uses_l(A,LocalParas,RActionVars) % TO DO: use get_accessed_vars ?
    ; get_accessed_vars(A,LocalParas,_,RActionVars)
    ),
    list_to_ord_set(RActionVars,RActionVars1),
    rw_ord_intersection(RActionVars1,Read,ReadAction).

b_get_read_write_vars(Operation,ReadGuardV,ReadActionV,ReadV,Write) :-
    b_get_read_write_vars_and_consts(false,Operation,ReadGuardV,ReadActionV,ReadV,Write).

b_get_read_write_vars_and_consts(IncludeConstants,Operation,ReadGuardV,ReadActionV,ReadV,Write) :-
    b_get_read_write_guard_action(Operation,ReadGuard,ReadAction,Read,Write),
    b_get_machine_variables(TVars),
    (IncludeConstants==true
    -> b_get_machine_constants(TConsts), append(TConsts,TVars,TCV) % should we include get_global_identifiers ?
    ; TCV = TVars),
    get_texpr_ids(TCV,Vars),
    list_to_ord_set(Vars,Variables),
    ord_intersection(ReadGuard,Variables,ReadGuardV),
    ord_intersection(ReadAction,Variables,ReadActionV),
    ord_intersection(Read,Variables,ReadV).

b_get_written_variables(WrittenVariables) :-
    findall(Var,
    (b_top_level_operation(Operation),
    %get_operation(Operation,_Results,_Paras),
    b_get_read_write(Operation,_,WriteV),
    member(Var,WriteV)
    ),Vars),
    sort(Vars,WrittenVariables).

check_all_variables_written :-
    b_get_written_variables(WrittenVariables),
    b_get_machine_variables(TVars),
    member(TVar,TVars),
    get_texpr_id(TVar,Var),
    \+ ord_member(Var,WrittenVariables),
    (written_by_not_top_level_operation(Var,Op2)
    -> ajoin(['Variable is written by no top-level operation (but is written by ',Op2,'): '],Msg),
    add_warning(check_all_variables_written,Msg,Var,TVar)
    ; add_warning(check_all_variables_written,'Variable is written by no operation (consider defining it as a constant): ',Var,TVar)
    ),
    fail.

check_all_variables_written.

empty_mrinfo(mrinfo([],[],[])).

extract_changed_id(Id,Name) :-
    get_texpr_id(Id,Name),!.

extract_changed_id(FuncOrRec,Name) :-
    get_texpr_expr(FuncOrRec,Expr),
    get_nested_modified_expr(Expr,TId),
    !,
    extract_changed_id(TId,Name). % we can have nested function calls f(x)(y) := z or nested records f(x)'field := z

extract_changed_id(X,Name) :-
    add_internal_error('Could not extract changed id: ',extract_changed_id(X,Name)),fail.

extract_must_write(b(Sub,_,_),Nested,MV) :- extract_must_write_aux(Sub,Nested,MV),!.

extract_must_write(O,N,MV) :- add_internal_error('Call failed: ',extract_must_write(O,N,MV)),MV=[].

extract_must_write_aux(assign(LHS,_),_,V) :- maplist(get_id,LHS,Vars), list_to_ord_set(Vars,V).

extract_must_write_aux(assign_single_id(TID,_),_,[ID]) :- get_id(TID,ID).

extract_must_write_aux(becomes_such(LHS,_),_,V) :- maplist(get_id,LHS,Vars), list_to_ord_set(Vars,V).

extract_must_write_aux(becomes_element_of(LHS,_),_,V) :- maplist(get_id,LHS,Vars), list_to_ord_set(Vars,V).

extract_must_write_aux(precondition(_,TBody),Nested,MV) :- extract_must_write(TBody,Nested,MV).

extract_must_write_aux(assertion(_,TBody),Nested,MV) :- extract_must_write(TBody,Nested,MV).

extract_must_write_aux(any(_,_,TBody),Nested,MV) :- extract_must_write(TBody,Nested,MV).

extract_must_write_aux(let(_,_,TBody),Nested,MV) :- extract_must_write(TBody,Nested,MV).

extract_must_write_aux(lazy_let_subst(_,_,TBody),Nested,MV) :- extract_must_write(TBody,Nested,MV).

extract_must_write_aux(block(TBody),Nested,MV) :- extract_must_write(TBody,Nested,MV).

extract_must_write_aux(choice([A]),Nested,MV) :- !, extract_must_write(A,Nested,MV).

extract_must_write_aux(choice([A|T]),Nested,MV) :-
    extract_must_write(A,Nested,MV1), extract_must_write_aux(choice(T),Nested,MV2), ord_intersection(MV1,MV2,MV).

extract_must_write_aux(if([I]),Nested,MV) :- !, get_texpr_expr(I,if_elsif(Cond,TBody)),
    (is_truth(Cond) -> extract_must_write(TBody,Nested,MV) ; MV=[]). % we have ELSE skip and then write nothing

extract_must_write_aux(if([I|T]),Nested,MV) :- get_texpr_expr(I,if_elsif(_,TBody)),
    extract_must_write(TBody,Nested,MV1), extract_must_write_aux(if(T),Nested,MV2), ord_intersection(MV1,MV2,MV).

extract_must_write_aux(select([SW]),Nested,MV) :- !,
    get_texpr_expr(SW,select_when(_,TBody)),extract_must_write(TBody,Nested,MV).

extract_must_write_aux(select([SW|T]),Nested,MV) :-
    get_texpr_expr(SW,select_when(_,TBody)), extract_must_write(TBody,Nested,MV1),
    extract_must_write_aux(select(T),Nested,MV2),ord_intersection(MV1,MV2,MV).

extract_must_write_aux(select(T,Else),Nested,MV) :-
    extract_must_write(Else,Nested,MV1),
    extract_must_write_aux(select(T),Nested,MV2),ord_intersection(MV1,MV2,MV).

extract_must_write_aux(case(_,[],Else),Nested,MV) :- extract_must_write(Else,Nested,MV).

extract_must_write_aux(case(E,[C|T],Else),Nested,MV) :-
    get_texpr_expr(C,case_or(_,TBody)),
    extract_must_write(TBody,Nested,MV1),
    extract_must_write_aux(case(E,T,Else),Nested,MV2),ord_intersection(MV1,MV2,MV).

extract_must_write_aux(parallel([A]),Nested,MV) :- !, extract_must_write(A,Nested,MV).

extract_must_write_aux(parallel([A|T]),Nested,MV) :-
    extract_must_write(A,Nested,MV1), extract_must_write_aux(parallel(T),Nested,MV2), ord_union(MV1,MV2,MV).

extract_must_write_aux(sequence(S),Nested,MV) :- !, extract_must_write_aux(parallel(S),Nested,MV).

extract_must_write_aux(skip,_,[]).

extract_must_write_aux(external_subst_call(_,_),_,[]). % assume there is no guarantee that something is written

extract_must_write_aux(while(_,_,_,_),_,[]). % in case the condition is false, the loop is not entered

extract_must_write_aux(var(Parameters,TBody),Nested,MV) :-
    def_get_texpr_ids(Parameters,IDs),
    list_to_ord_set(IDs,MV2),
    extract_must_write(TBody,Nested,MV1),
    ord_subtract(MV1,MV2,MV).

extract_must_write_aux(operation_call(TOperation,Results,_),Nested,MustWriteV) :-
    maplist(get_id,Results,Vars), list_to_ord_set(Vars,WrittenResults),
    (Nested=not_nested -> MustWriteV=WrittenResults
    ; def_get_texpr_id(TOperation,op(Operation)),
    b_get_read_may_must_write(Operation,MustWriteVInner,_), %and ideally cache values
    ord_union(WrittenResults,MustWriteVInner,MustWriteV)
).

extract_must_write_aux(Other,_,[]) :-
    add_message('Uncovered substitution for must_write computation: ',Other).

extract_reads_and_modifies(mrinfo(_,_,_),mrinfo(Modified,NonDetModified,Reads),
    Modified,NonDetModified,Reads).

filter_result_vars(Ids,LocalVars,ModifiedVars) :-
    % extract_changed_id might fail if the user entered
    % a wrong LHS of an assignment. This should lead to an
    % type error, handled by the assign type checking rule.
    convlist(extract_changed_id,Ids,Names),
    remove_all(Names,LocalVars,ModifiedVars).

find_read_vars_for_becomes_such(TIds,Body,LocalVars0,BMSuchReadVars) :-
    add_tvars_to_ord_list(LocalVars0,TIds,LocalVars1,_,_), % ignore reading new values; this does not correspond to reading a value in the current state
    % all Ids are already marked as accessed, any reference to Id$0 is a read of the old value; do not add Id$0 to the accessed variables
    get_texpr_ids(TIds,Names),
    maplist(add_dollar_zero,Names,RenameList),
    list_to_ord_set(RenameList,SRenameList),
    find_identifier_uses(Body,LocalVars1,ReadVars),
    remap_primed_ids(ReadVars,SRenameList,LocalVars0,BMSuchReadVars).

get_accessed_vars(TSubst,LocalVars,Modified,Reads) :-
    get_accessed_vars(TSubst,LocalVars,Modified,_,Reads).

get_accessed_vars(TSubst,LocalVars,Modified,NonDetModified,Reads) :-
    get_global_identifiers(IS), % TO DO: currently this information is set up only *after* type checking !!
    % this means the accessed vars will also contain SETS and enumerated set elements !
    % either we need to filter them out later, or change the startup / precompilation process
    list_to_ord_set(LocalVars,SLV),
    ord_union(IS,SLV,LocalVarsToIgnore),
    empty_mrinfo(In),
    get_accessed_vars1(TSubst,LocalVarsToIgnore,In,Out),
    extract_reads_and_modifies(In,Out,Modified,NonDetModified,Reads).

get_accessed_vars1(TSubst,LocalVars,In,Out) :-
    get_texpr_expr(TSubst,Subst),
    ( is_operation_call(Subst,Operation,Results,Arguments) ->
    get_texpr_info(TSubst,Info),
    def_get_texpr_id(Operation,op(OperationName)),
    memberchk(modifies(MVars),Info),
    (memberchk(non_det_modifies(NonDetMVars),Info) -> true ; NonDetMVars=[]),
    memberchk(reads(RVars),Info),
    % info fields added in btype2(operation(...) in btypechecker.pl
    %op_modifies_reads_cache(OperationName,MVarsC,RVarsC) %this is no longer necessary
    (ground(MVars),ground(RVars)
    -> true
    ; add_error(b_read_write_info, 'Cannot obtain modifies/reads info for called operation (probably illegal local call): ',OperationName),
    % TEST 655 used to reach this branch
    MVars=[], RVars=[], NonDetMVars=[]
    % this should only happen when local operation called !?!
    % or ensure that operations are processed before we reach operation calls
    % this may be problematic for local operations
    ),
    accessed_vars_for_operation_call(MVars,NonDetMVars,RVars,LocalVars,Results,Arguments,In,Out)
    ; get_accessed_vars2(Subst,LocalVars,In,Out) ->
    true
    ; Subst = identifier(ID) -> add_error(b_read_write_info,'Identifier not a valid B Operation: ',ID,TSubst),In=Out
    ;
    add_internal_error('Could not extract information about accessed variables for substitution',
    get_accessed_vars2(Subst,LocalVars,In,Out)),
    %trace, get_accessed_vars2(Subst,LocalVars,In,Out),
    fail).

get_accessed_vars2(skip,_) --> !.

get_accessed_vars2(block(Subst),LocalVars) --> get_accessed_vars1(Subst,LocalVars).

get_accessed_vars2(init_statement(Subst),LocalVars) --> get_accessed_vars1(Subst,LocalVars).

get_accessed_vars2(assertion(A,Subst),R) --> add_read_vars(A,R),get_accessed_vars1(Subst,R).

get_accessed_vars2(assign(LHS,E),R) --> %Note: LHS can be nested function application f(a)(b) :=
    {maplist(get_lhs_assigned_identifier,LHS,Ids)}, add_modified_vars(Ids,R),
    {convlist(get_lhs_read_expression,LHS,LHS_R), append(LHS_R,E,RE)}, add_read_vars_l(RE,R).

get_accessed_vars2(assign_single_id(Id,E),R) -->
    add_read_vars_l([E],R), % Note: LHS is a single Identifier: nothing is ever read there
    add_modified_vars([Id],R).

get_accessed_vars2(precondition(P,Subst),R) -->add_read_vars(P,R),get_accessed_vars1(Subst,R).

get_accessed_vars2(assertion(Subst),R) --> get_accessed_vars1(Subst,R).

get_accessed_vars2(choice(Substs),R) --> get_accessed_vars_for_choice(Substs,R).

get_accessed_vars2(if(Substs),R) --> get_accessed_vars_for_if(Substs,R).

get_accessed_vars2(select(Whens,Else),R) --> get_accessed_vars_for_select(Whens,Else,R).

get_accessed_vars2(select(Whens),R) --> get_accessed_vars_for_select(Whens,none,R).

get_accessed_vars2(case(Expr,Substs,Else),R) --> get_accessed_vars_for_case(Expr,Substs,Else,R).

get_accessed_vars2(case_or(Exprs,Subst),R) --> add_read_vars_l(Exprs,R),get_accessed_vars1(Subst,R).

get_accessed_vars2(any(Ids,G,Subst),R) --> get_mrinfo(ModIn,_,_),
    add_tvars_to_ord_list(R,Ids,L),add_read_vars(G,L),
    get_accessed_vars1(Subst,L),
    add_delta_modified_to_non_det_modified(ModIn). % variables modified within an ANY are supposed to be non-det assigned; e.g. ANY x WHERE x:1..2 THEN y:=x END

get_accessed_vars2(let(Ids,G,Subst),R) -->
    add_tvars_to_ord_list(R,Ids,L),add_read_vars(G,L),get_accessed_vars1(Subst,L).

get_accessed_vars2(lazy_let_subst(ID,SharedExpr,Subst),R) --> add_tvars_to_ord_list(R,[ID],L),
    add_read_vars(SharedExpr,L),get_accessed_vars1(Subst,L).

get_accessed_vars2(becomes_element_of(Ids,E),R) --> add_non_det_modified_vars(Ids,R),add_read_vars(E,R).

get_accessed_vars2(becomes_such(Ids,E),LocalVars0) -->
    add_non_det_modified_vars(Ids,LocalVars0),
    {find_read_vars_for_becomes_such(Ids,E,LocalVars0,ReadVars)},
    add_read_vars2(ReadVars).

get_accessed_vars2(sequence(Substs),R) --> get_accessed_vars_sequence(Substs,R).

get_accessed_vars2(parallel(Substs),R) --> get_accessed_vars_l(Substs,R).

get_accessed_vars2(while(Cond,Subst,Inv,Variant),R) -->
    get_accessed_vars_for_while(Cond,Subst,Inv,Variant,R).

get_accessed_vars2(var(Ids,Subst),R) --> add_tvars_to_ord_list(R,Ids,L),get_accessed_vars1(Subst,L).

get_accessed_vars2(external_subst_call(_Name,Exprs),R) --> add_read_vars_l(Exprs,R).

get_accessed_vars2(rlevent(_Name,_Section,VariantStatus,Params,Guard,Theorems,Actions,VWitnesses,PWitnesses,Unmod,AbstractEvents),R) -->
    % the code duplicates the logic in collect_read_vars in bmachine_eventb.pl; TO-DO: merge
    add_tvars_to_ord_list(R,Params,L),
    add_read_vars(Guard,L),
    add_read_vars_l(Theorems,L),
    add_read_vars_l(Unmod,L), % for unmodifiables we check that whether new values correspond to old values and thus need read accces to the old value in check_if_invalid_vars_are_modified
    add_variant_status_read_vars(VariantStatus,R), % the parameters should not be used in the Variant
    add_witness_read_vars_l(VWitnesses,L),
    add_witness_read_vars_l(PWitnesses,L),
    get_accessed_vars_l(Actions,L),
    get_accessed_vars_l(AbstractEvents,L).

get_accessed_vars_for_case(Expr,Eithers,Else,Locals) -->
    % we can treat a case statement analogously to an IF-THEN-ELSE statement
    % where an ELSE is present
    % additionally, we have to add all expressions to the read set
    add_read_vars(Expr,Locals),
    { maplist(split_case_or,Eithers,ExprsList,Substs), append(ExprsList,Exprs) },
    add_read_vars_l(Exprs,Locals),
    get_accessed_vars_for_if_when(has_else,[Else|Substs],Locals).

get_accessed_vars_for_choice(Substs,Locals,In,mrinfo(ModOut,NDOut2,Read)) :-
    get_accessed_vars_for_if_when(has_else,Substs,Locals,In,Out),
    In = mrinfo(ModIn,_,_),
    Out = mrinfo(ModOut,NDOut,Read), % these three fields will be all variables
    % mark all assignments as non-deterministically chosen:
    add_modified_to_non_det_modified(ModIn,ModOut,NDOut,NDOut2).

get_accessed_vars_for_if(ElseIfs,Locals) -->
    { maplist(split_elseif,ElseIfs,Conds,Subst),
    (if_has_else_block(Conds) -> HasElse = has_else ; HasElse = if_with_no_else) },
    % mark all used variables in the conditions as read
    add_read_vars_l(Conds,Locals),
    get_accessed_vars_for_if_when(HasElse,Subst,Locals).

get_accessed_vars_for_if_when(HasElse,Subst,Locals) -->
    { get_accessed_vars_for_if_when2(HasElse,Subst,Locals,Modified,NonDetModifies,Reads) },
    add_read_vars2(Reads),
    %add_modified_vars2(Modified)
    ({(HasElse==has_else ; HasElse==if_with_no_else ; Subst = [_,_|_])}
    -> {my_ord_union(NonDetModifies,Modified,M2)},
    add_non_det_modified_vars2(M2)
    ; add_non_det_modified_vars2(NonDetModifies),
    add_modified_vars2(Modified) % there is only one branch: Modified variables not also marked as non-det modified
).

get_accessed_vars_for_if_when2(has_else,Subst,Locals,ModifiedBySome,NonDetModifiedBySome,ReadBySome) :-
    maplist5(get_accessed_vars_x(Locals),Subst,Modifies,NonDetModifies,Reads),
    % We want to calculate those elements that are modified by some (in the union)
    % but not by all (in the intersection)
    ord_union(NonDetModifies,NonDetModifiedBySome),
    ord_union(Modifies,ModifiedBySome),
    ord_intersection(Modifies,ModifiedByAll),
    ord_subtract(ModifiedBySome,ModifiedByAll,ModifiedByNotAll),
    % we add those values that are not modified by all to the set of read variables
    % because e.g. "IF P THEN x:=1 END" is equivalent to "IF P THEN x:=1 ELSE x:=x END"
    ord_union([ModifiedByNotAll|Reads],ReadBySome).

get_accessed_vars_for_if_when2(select_no_else,Subst,Locals,ModifiedBySome,NonDetModifiedBySome,ReadBySome) :-
    % Note "SELECT P THEN x:=1 END" is NOT equivalent to "SELECT P THEN x:=1 ELSE x:=x END" !
    % there is no implicit skip, which copies all variables;
    % as such it can be treated like an if with an exhaustive list of cases
    % the treatment for computing ModifiedBySome,ReadBySome is identical
    get_accessed_vars_for_if_when2(has_else,Subst,Locals,ModifiedBySome,NonDetModifiedBySome,ReadBySome).

get_accessed_vars_for_if_when2(if_with_no_else,Subst,Locals,ModifiedBySome,NonDetModifiedBySome,ReadBySome) :-
    % no else block present, we must assume that each written variable
    % can also be treated like a read variable, see example in the other condition:
    % e.g. "IF P THEN x:=1 END" is equivalent to "IF P THEN x:=1 ELSE x:=x END" and thus reads the old value of x
    maplist5(get_accessed_vars_x(Locals),Subst,Modifies,NonDetModifies,Reads),
    ord_union(NonDetModifies,NonDetModifiedBySome),
    ord_union(Modifies,ModifiedBySome),
    ord_union([ModifiedBySome|Reads],ReadBySome).

get_accessed_vars_for_select(Whens,Else,Locals) -->
    { maplist(split_when,Whens,Conds,Subst1),
    ( Else = none ->
    HasElse=select_no_else, Subst = Subst1
    ;
    HasElse=has_else, Subst = [Else|Subst1]) },
    % mark all used variables in the conditions as read
    add_read_vars_l(Conds,Locals),
    get_accessed_vars_for_if_when(HasElse,Subst,Locals).

get_accessed_vars_for_while(Cond,Subst,Inv,Variant,Locals) -->
    get_accessed_vars_for_while_invariant(Inv,Locals),
    add_read_vars(Cond,Locals),
    add_read_vars(Variant,Locals),
    %get_accessed_vars1(Subst,Locals).
    % The Substitution may not be executed; just like an IF
    % e.g. "WHILE P DO x:=1 ... END" may keep (and thus virtually read) the old value of x if P is false initially
    get_accessed_vars_for_if_when(if_with_no_else,[Subst],Locals).

get_accessed_vars_for_while_invariant(Inv,Locals,In,Out) :-
    empty_mrinfo(LI),
    add_read_vars(Inv,Locals,LI,LO),
    extract_reads_and_modifies(LI,LO,Modified,_,Reads0),
    maplist(remove_optional_prime,Reads0,Reads),
    list_to_ord_set(Reads,SReads), % removing prime can create duplicates
    add_non_local_read_vars(SReads,Locals,In,Inter),
    add_non_local_modified_vars(Modified,Locals,Inter,Out).

get_accessed_vars_l([],_) --> [].

get_accessed_vars_l([S|Rest],LovalVars) -->
    get_accessed_vars1(S,LovalVars),
    get_accessed_vars_l(Rest,LovalVars).

get_accessed_vars_sequence([],_) --> [].

get_accessed_vars_sequence([S|Rest],LocalVars) --> %portray_mrinfo(seq(S)),
    % TO DO: we could always compute must_write information in get_accessed_vars, rather than re-traversing here:
    {Rest \= [], extract_must_write(S,not_nested,WIds),my_ord_union(WIds,LocalVars,LocalVars2)},!,
    % not_nested: do not look at nested operation calls: they may not be precompiled; and we cannot read them from here anyway? ; relevant tests: 1601, 1782, 1870
    % treat case x := 0 ; y := x+1 --> x is read after completely written
    % careful, we can have: f(1) := 0; y := f(2) !
    % we can also have: x:=x+1 ; y := x --> here x is read
    % Note: we need the must_write information to be sure that x cannot be read after S; may_write is not enough
    get_accessed_vars1(S,LocalVars),
    % in rest any read, write to LocalVars2 will not be registered;
    % only problem is that we could have something like x:=0 ; x::{1,2} and we would not register x as NonDetModifies
    % NonDetModifies is only used in animation interface to show additional virtual parameters for operations
    % it is thus not critical
    get_accessed_vars_sequence(Rest,LocalVars2).

get_accessed_vars_sequence([S|Rest],LocalVars) -->
    get_accessed_vars1(S,LocalVars),
    get_accessed_vars_sequence(Rest,LocalVars).

get_accessed_vars_x(Locals,Subst,Modifies,NonDetModifies,Reads) :-
    get_accessed_vars(Subst,Locals,Modifies,NonDetModifies,Reads).

get_action(OpName,Action) :- get_operation_propositional_guards(OpName,_,Action).

get_assign_val(assign_single_id(TID,Val),ID,Val) :-
    get_texpr_id(TID,ID),!,
    (simple_val(Val) -> true ; simple_modification(Val,ID)).

get_assign_val(any(_,_,TBody),Var,Val) :- get_texpr_expr(TBody,Body), get_assign_val(Body,Var,Val).

get_assign_val(select([b(select_when(_,TBody),_,_)]),Var,Val) :-
    get_texpr_expr(TBody,Body), get_assign_val(Body,Var,Val).

get_assign_val(parallel(Bodies),Var,Val) :- member(TBody,Bodies),
    get_texpr_expr(TBody,Body), get_assign_val(Body,Var,Val).