b_interpreter_eventb

abstract_event_constraints([],_VWit,_PWit,_IS,_LS,_OS,[],D,_WF) :-
    % no more refined level exists, stop here
    !, eventtrace_finalise(D,_).

abstract_event_constraints(AbstractEvents,VWitnesses,PWitnesses,IS,LS,OS,AbstractPath,Din,WF) :-
    % copy a primed version of all values in the outstate
    % into the local state
    copy_primed(OS,LS,NewLS),
    % evaluate witnesses for dropped abstract vars
    abstract_var_witnesses_constraints(VWitnesses,IS,NewLS,OS,Din,D1,WF),
    % evaluate witnesses for dropped parameters
    abstract_parameter_witnesses_constraints(PWitnesses,IS,NewLS,AbsLS,_Params,_PValues,D1,D2,WF),
    % continue with the next refinement level
    execute_abstract_events_with_constraints(AbstractEvents,IS,AbsLS,OS,AbstractPath,D2,WF).

abstract_parameter_witnesses_constraints(Witnesses,IS,LS,AbsLS,Params,PValues,Din,Dout,WF) :-
    abstract_parameter_witnesses_constraints2(Witnesses,IS,LS,LS,AbsLS,Params,PValues,Din,Dout,WF).

abstract_parameter_witnesses_constraints2([],_State,_OrigLS,LS,LS,[],[],D,D,_WF).

abstract_parameter_witnesses_constraints2([Witness|WRest],State,OrigLS,LS,AbsLS,[TId|Params],[Value|PValues],Din,Dout,WF) :-
    witness_substate(Witness,OrigLS,LS,TId,Value,Predicate,TypedVals,WitnessLS,ExtLS),
    enumerate_predicate_wf(Predicate,TypedVals,WitnessLS,State,WF),
    eventtrace_add(eval_witness(parameter,TId,Value,Predicate),Din,D1),
    abstract_parameter_witnesses_constraints2(WRest,State,OrigLS,ExtLS,AbsLS,Params,PValues,D1,Dout,WF).

abstract_var_witnesses_constraints([],_IS,_LS,_OS,D,D,_WF).

abstract_var_witnesses_constraints([Witness|WRest],IS,LS,OS,Din,Dout,WF) :-
    extract_witness(Witness,TId,Id,Type,Predicate),
    b_enumerate_values_in_store([Id],[Type],[Value],LS,WF),
    b_test_boolean_expression(Predicate,LS,IS,WF),
    eventtrace_add(eval_witness(variable,TId,Value,Predicate),Din,D1),
    abstract_var_witnesses_constraints(WRest,IS,LS,OS,D1,Dout,WF).

b_event_constraints(TBody,Parameters,NormalisedParaValues,IS,OS,Path,WF) :-
    get_texpr_expr(TBody,Event),
    b_event_constraints_aux(Event,Parameters,NormalisedParaValues,IS,OS,Path,WF).

b_event_constraints_aux(Event,Parameters,NormalisedParaValues,IS,OS,Path,WF) :-
    extract_event(Event,Name,Section,Guard,Post),
    (is_truth(Post) -> true
    ; add_error_wf(b_event_constraints,'Ignoring additional post condition: ',Post,Post,WF)),
    setup_event_state(Parameters,ParaValues,NormalisedParaValues,ParamTypedVals,LS),
    % evaluate guard
    enumerate_predicate_wf(Guard,ParamTypedVals,LS,IS,WF),
    % execute the event
    init_trace_of_event(Name,Section,Parameters,ParaValues,Guard,Path,RestPath,Desc),
    event_body_constraints(Event,IS,LS,OS,RestPath,Desc,WF).

b_event_with_change_set_aux(Event,Parameters,NormalisedParaValues,InState,ChangeSet,Updates,Path,WF) :-
    extract_event(Event,Name,Section,Guard,PostCond),
    setup_event_state(Parameters,ParaValues,NormalisedParaValues,ParamTypedVals,LS),
    % evaluate the event's guard
    evaluate_predicate_if_necessary(Guard,ParamTypedVals,LS,InState,WF),
    % execute the event
    init_trace_of_event(Name,Section,Parameters,ParaValues,Guard,Path,RestPath,Desc),
    (ChangeSet==no_change_set_available -> OutState=Updates
    ; copy_variable_store(InState,ChangeSet,Updates,OutState)),
    % post condition, mainly for trace replay of initialisation
    b_test_boolean_expression(PostCond,LS,OutState,WF),
    execute_event_body_wf(Event,InState,LS,OutState,RestPath,Desc,WF).

b_execute_event(Name,TBody,Parameters,NormalisedParaValues,InState,OutState,Path) :-
    get_texpr_expr(TBody,Event),
    init_wait_flags_with_call_stack(WF,[operation_call(Name,Parameters,unknown)]),
    b_event_with_change_set_aux(Event,Parameters,NormalisedParaValues,InState,no_change_set_available,OutState,Path,WF),
    ground_wait_flags(WF).

b_execute_event_with_change_set_wf(TBody,Parameters,NormalisedParaValues,InState,ChangeSet,Updates,
    Path,WF,_OutputReq) :-
    get_texpr_expr(TBody,Event),
    b_event_with_change_set_aux(Event,Parameters,NormalisedParaValues,InState,ChangeSet,Updates,Path,WF).

b_execute_eventb_action(assign(Lhs,Exprs),IS,LS,OS,WF,Step) :- !,
    b_interpreter:b_compute_expressions(Exprs,LS,IS,VALs,WF), % VALs - a list of computed values
    b_interpreter:b_assign_values_or_functions(Lhs,VALs,LS,IS,NewValues,WF,output_required),
    eventb_store_new_values(NewValues,OS),
    Step = action(Lhs,Exprs,VALs).

b_execute_eventb_action(becomes_element_of(Lhs,Rhs),IS,LS,OS,WF,Step) :- !,
    convert_pairs_into_list(Lhs,Val,ValList),
    get_texpr_types(Lhs,Types),
    b_compute_expression(Rhs,LS,IS,ValueSet,WF),
    check_element_of_wf(Val,ValueSet,WF),
    b_enumerate_typed_values(ValList,Types,WF),
    % ground_det_wait_flag(WF),
    b_interpreter:b_assign_values_or_functions(Lhs,ValList,LS,IS,NewValues,WF,output_required),
    eventb_store_new_values(NewValues,OS),
    Step = action_set(Lhs,Rhs,ValueSet,ValList).

b_execute_eventb_action(becomes_such(Ids,Pred),IS,LS,OS,WF,Step) :- !,
    b_interpreter:b_execute_becomes_such(Ids,Pred,LS,IS,OutputValues,IdsValues,WF),
    eventb_store_new_values(OutputValues,OS),
    Step = action_pred(Ids,Pred,IdsValues).

b_execute_eventb_action(Action,IS,LS,OS,WF,Step) :-
    add_internal_error('Unknown Event-B action: ',b_execute_eventb_action(Action,IS,LS,OS,WF,Step)),fail.

b_execute_eventb_actions([],_Name,_IS,_LS,_OS,D,D).

b_execute_eventb_actions([TAction|ARest],Name,IS,LS,OS,Din,Dout) :-
    get_texpr_expr(TAction,Action),
    (get_texpr_pos(TAction,Pos) -> true ; Pos=unknown),
    if( ( init_wait_flags_with_call_stack(WF,[b_operator_call(Name,LS,Pos)]),
    b_execute_eventb_action(Action,IS,LS,OS,WF,Step),
    ground_wait_flags(WF)),
    ( eventtrace_add(Step,Din,D1),
    b_execute_eventb_actions(ARest,Name,IS,LS,OS,D1,Dout)),
    ((abort_error_occured_in_error_scope,
    \+ always_well_defined(TAction) % all actions are evaluated in the same error scope; just check
    -> WDERR=wd_error_possible; WDERR=no_wd_error),
    eventtrace_failure(action_not_executable(TAction,WDERR),Din))).

check_event_entry_status(TStatus,IS,LS,VariantValue,Din,Dout) :-
    get_texpr_expr(TStatus,Status),
    check_event_entry_status2(Status,IS,LS,VariantValue,Din,Dout).

check_event_entry_status2(ordinary,_IS,_LS,-,D,D).

check_event_entry_status2(anticipated(Variant),IS,LS,Val,Din,Dout) :-
    variant_is_not_negative(Variant,anticipated,IS,LS,Val,Din,Dout).

check_event_entry_status2(convergent(Variant),IS,LS,Val,Din,Dout) :-
    variant_is_not_negative(Variant,convergent,IS,LS,Val,Din,Dout).

check_event_exit_status(-,_TStatus,_OS,_LS,D,D) :- !.

check_event_exit_status(EntryValue,TStatus,OS,LS,Din,Dout) :-
    get_texpr_expr(TStatus,Status),
    % Status is convergent(VariantExpr) or anticipated(VariantExpr)
    functor(Status,CType,1),arg(1,Status,VariantExpr),
    get_texpr_type(VariantExpr,Type),
    if( b_compute_expression_nowf(VariantExpr,LS,OS,ExitValue,'variant (exit)',0),
    ( variant_condition(CType,Type,EntryValue,ExitValue) ->
    eventtrace_add(variant_checked_post(CType,VariantExpr,EntryValue,ExitValue),Din,Dout)
    ;
    eventtrace_store_event_error(invalid_variant(CType,VariantExpr,EntryValue,ExitValue),Din,Dout)),
    eventtrace_store_event_error(event_wd_error(VariantExpr,variant_after_event),Din,Dout)).

check_event_theorem(Theorem,Name,State,LState,Din,Dout) :-
    ( evaluate_predicate(Theorem,[],LState,State,event_theorem(Name)) ->
    Din = Dout
    %eventtrace_add(theorem_checked(Theorem),Din,Dout)
    ;
    eventtrace_store_event_error(invalid_theorem_in_guard(Theorem),Din,Dout)
).

check_event_theorems([],_Name,_State,_LState,D,D).

check_event_theorems([Theorem|Trest],Name,State,LState,Din,Dout) :-
    check_event_theorem(Theorem,Name,State,LState,Din,Dinter),
    check_event_theorems(Trest,Name,State,LState,Dinter,Dout).

check_if_invalid_vars_are_modified([],_IS,_OS,_D).

check_if_invalid_vars_are_modified([Unmod|UnmodRest],IS,OS,D) :-
    check_unmodifiable(Unmod,IS,OS,D),
    check_if_invalid_vars_are_modified(UnmodRest,IS,OS,D).

check_unmodifiable(Var,IS,OS,D) :-
    def_get_texpr_id(Var,Id),
    lookup_value(Id,IS,Pre),!,
    lookup_value(Id,OS,Post),!,
    (equal_object(Pre,Post) -> true ; eventtrace_failure(invalid_modification(Var,Pre,Post),D)).

copy_primed([], InStore, InStore).

copy_primed([bind(OldVar,Value)|Srest], InStore, OutStore) :-
    atom_concat(OldVar,'\'',NewVar), % is faster than caching this using a dynamic fact
    copy_primed(Srest,[bind(NewVar,Value)|InStore], OutStore).

enumerate_predicate_wf(Predicate,TypedVals,LS,State,WF) :-
    b_test_boolean_expression(Predicate,LS,State,WF),
    b_tighter_enumerate_values_in_ctxt(TypedVals,Predicate,WF). % moved this later for performance, see PerformanceTests/ParameterEnumeration_mch.eventb

evaluate_predicate(Predicate,TypedVals,LS,State,Context) :-
    init_wait_flags_with_call_stack(WF,[prob_command_context(Context,unknown)]),
    enumerate_predicate_wf(Predicate,TypedVals,LS,State,WF),
    ground_wait_flags(WF).

evaluate_predicate_if_necessary(Guard,ParamTypedVals,LS,InState,WF) :-
    (ParamTypedVals==[], get_preference(ltsmin_do_not_evaluate_top_level_guards,full) ->
    % if we already know that the event is enabled
    % in the current state, we don't need to evaluate the guard here
    debug_println(9,guard_will_not_be_evaluated_b_event)
    ;
    enumerate_predicate_wf(Guard,ParamTypedVals,LS,InState,WF)
%evaluate_predicate(Guard,ParamTypedVals,LS,InState,event_guard)
).

evaluate_witnesses_for_abstract_parameters(Witnesses,Name,IS,LS,AbsLS,Params,PValues,Din,Dout) :-
    evaluate_witnesses_for_abstract_parameters2(Witnesses,Name,IS,LS,LS,AbsLS,Params,PValues,Din,Dout).

evaluate_witnesses_for_abstract_parameters2([],_Name,_State,_OrigLS,LS,LS,[],[],D,D).

evaluate_witnesses_for_abstract_parameters2([Witness|WRest],Name,State,OrigLS,LS,AbsLS,
    [TId|Params],[Value|PValues],Din,Dout) :-
    witness_substate(Witness,OrigLS,LS,TId,Value,Predicate,TypedVals,WitnessLS,ExtLS),
    if( evaluate_predicate(Predicate,TypedVals,WitnessLS,State,event_parameter_witness(Name)),
    ( eventtrace_add(eval_witness(parameter,TId,Value,Predicate),Din,D1),
    evaluate_witnesses_for_abstract_parameters2(WRest,Name,State,OrigLS,ExtLS,AbsLS,Params,PValues,D1,Dout)),
    eventtrace_failure(no_witness_found(parameter,TId,Predicate), Din) ).

evaluate_witnesses_for_abstract_vars([],_Name,_IS,_LS,_OS,D,D).

evaluate_witnesses_for_abstract_vars([Witness|WRest],Name,IS,LS,OS,Din,Dout) :-
    extract_witness(Witness,TId,Id,Type,Predicate),
    if( (init_wait_flags_with_call_stack(WF,[prob_command_context(event_abstract_variable_witness(Name),unknown)]),
    b_enumerate_values_in_store([Id],[Type],[Value],LS,WF),
    b_test_boolean_expression(Predicate,LS,IS,WF),
    ground_wait_flags(WF)),
    ( eventtrace_add(eval_witness(variable,TId,Value,Predicate),Din,D1),
    evaluate_witnesses_for_abstract_vars(WRest,Name,IS,LS,OS,D1,Dout)),
    eventtrace_failure(no_witness_found(variable,TId,Predicate),Din) ).

event_body_constraints(Event,IS,LS,OS,AbstractPath,D,WF) :-
    Event = rlevent(_Name,_Section,_Status,_Params,_Guard,_Thms,Actions,VWitnesses,PWitnesses,_Unmodifiables,AbstractEvents),
    % for convergent/anticipated events: check if the variant is non-negative
    % check_event_entry_status(Status,IS,LS,VariantValue,D,D2),
    eventb_actions_constraints(Actions,IS,LS,OS,D,D2,WF),
    % for convergent/anticipated events: check if the variant has decreased/not increased
    % check_event_exit_status(VariantValue,Status,OS,LS,D3,D4),
    % check_if_invalid_vars_are_modified(Unmodifiables,IS,OS,D4),
    abstract_event_constraints(AbstractEvents,VWitnesses,PWitnesses,IS,LS,OS,AbstractPath,D2,WF).

eventb_actions_constraints([],_IS,_LS,_OS,D,D,_WF).

eventb_actions_constraints([TAction|ARest],IS,LS,OS,Din,Dout,WF) :-
    get_texpr_expr(TAction,Action),
    b_execute_eventb_action(Action,IS,LS,OS,WF,Step),
    eventtrace_add(Step,Din,D1),
    eventb_actions_constraints(ARest,IS,LS,OS,D1,Dout,WF).

eventb_store_new_values([],_Store).

eventb_store_new_values([bind(Id,Value)|IRest],Store) :-
    (lookup_value(Id,Store,Res) -> StoreValue=Res
    ; add_internal_error('Cannot find Event-B identifier:',Id:Store),fail),
    equal_object(StoreValue,Value),
    eventb_store_new_values(IRest,Store).

eventtrace_add( Entry, desc(EN,D,[Entry|L]), desc(EN,D,L) ).

eventtrace_failure(Error,Desc) :-
    eventtrace_name(Desc,EventName),
    eventtrace_add(Error,Desc,D1),
    eventtrace_finalise(D1,D),
    %translate:explain_state_error(eventerror(EventName,Error,D),unknown,Out), format(user_error,'~s~n',[Out]),
    store_error_for_context_state(eventerror(EventName,Error,D),_Id),
    fail.

eventtrace_finalise(desc(_EN,D,[]),D).

eventtrace_init(EventName, desc(EventName,D,D), D).

eventtrace_name( desc(EN,_,_), EN).

eventtrace_store_event_error(Error,Din,Dout) :-
    eventtrace_name(Din, EventName),
    copy_term(Din,Dcopy),
    eventtrace_add(Error,Dcopy,Dc1),
    eventtrace_finalise(Dc1,D),
    store_error_for_context_state(eventerror(EventName,Error,D),Id),
    eventtrace_add(error(Error,Id),Din,Dout).

execute_abstract_events(Events,Params,PValues,IS,LS,OS,[event(Name,PValues)|Path],Din) :-
    if( select_event(Events,Params,PValues,IS,LS,Event,Name,Din,D1),
    execute_event_body(Event,IS,LS,OS,Path,D1),
    ( generate_simulation_error(Events,Error), eventtrace_failure(Error,Din) )).

execute_abstract_events_with_constraints(AbstractEvents,IS,LS,OS,Path,D,WF) :-
    % This introduces a choicepoint when there are more than one abstract event.
    % But the usual case is just one abstract event
    member(TEvent,AbstractEvents),
    get_texpr_expr(TEvent,Event),
    event_body_constraints(Event,IS,LS,OS,Path,D,WF).

execute_event_body(Event,InState,LS,OutState,AbstractPath,D) :-
    Event = rlevent(Name,_Section,Status,_Params,_Guard,Theorems,
    Actions,VWitnesses,PWitnesses,Unmodifiables,AbstractEvents),
    % for convergent/anticipated events: check if the variant is non-negative
    check_event_entry_status(Status,InState,LS,VariantValue,D,D2),
    % check if the theorems hold
    check_event_theorems(Theorems,Name,InState,LS,D2,D3),
    % execute the actions
    b_execute_eventb_actions(Actions,Name,InState,LS,OutState,D3,D4),
    % for convergent/anticipated events: check if the variant has decreased/not increased
    check_event_exit_status(VariantValue,Status,OutState,LS,D4,D5),
    check_if_invalid_vars_are_modified(Unmodifiables,InState,OutState,D5),
    go_for_abstract_events(Name,AbstractEvents,VWitnesses,PWitnesses,InState,LS,OutState,AbstractPath,D5).

execute_event_body_block(_,Event,InState,LS,OutState,AbstractPath,D) :-
    execute_event_body(Event,InState,LS,OutState,AbstractPath,D).

execute_event_body_wf(Event,InState,LS,OutState,AbstractPath,D,WF) :-
    get_enumeration_finished_wait_flag(WF,WFE), % TO DO: pass WF instead and possibly to b_execute_eventb_actions
    execute_event_body_block(WFE,Event,InState,LS,OutState,AbstractPath,D).

extract_event(Event,Name,Section,FullGuard,AdditionalPostCondition) :-
    Event = rlevent(Name,Section,_Status,_Params,Guard,_Thms,_Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents),
    !,
    extract_event_aux(Name,Guard,FullGuard,AdditionalPostCondition).

extract_event(Event,Name,Section,FullGuard,PostCond) :-
    add_internal_error('Illegal Event-B Event: ',extract_event(Event,Name,Section,FullGuard,PostCond)),fail.

extract_event_aux('INITIALISATION',Guard,FullGuard,AdditionalPostCondition) :- !, FullGuard=Guard,
    (bmachine:b_machine_temp_predicate(TempPred)
    % The guard is evaluated on the state before ! It should be executed on the state after ! %% TO DO
    -> AdditionalPostCondition = TempPred
    ; AdditionalPostCondition = b(truth,pred,[])).

extract_event_aux(_Name,Guard,FullGuard,b(truth,pred,[])) :-
    % check for user-defined additional guard
    full_guard(Guard,_,FullGuard).

extract_witness(Witness,TId,Id,Type,Predicate) :-
    get_texpr_expr(Witness,witness(TId,Predicate)),
    def_get_texpr_id(TId,Id),
    get_texpr_type(TId,Type).

full_guard(Guard,TempPred,FullGuard) :-
    bmachine:b_machine_temp_predicate(TempPred),!,
    conjunct_predicates([TempPred,Guard],FullGuard).

full_guard(Guard,b(truth,pred,[]),Guard).

generate_simulation_error(Events,simulation_error(FailedEvents)) :-
    generate_simulation_error2(Events,FailedEvents).

generate_simulation_error2([],[]).

generate_simulation_error2([TEvent|Erest],[event(Name,Section,Guard)|Srest]) :-
    get_texpr_expr(TEvent,Event),
    Event = rlevent(Name,Section,_Status,_Params,Guard,_Thms,_Actions,_VWitnesses,_PWitnesses,_Unmodifiables,_AbstractEvents),
    generate_simulation_error2(Erest,Srest).

go_for_abstract_events(_Name,[],_VWit,_PWit,_IS,_LS,_OS,[],D) :-
    % no more refined level exists, stop here
    !, eventtrace_finalise(D,_).

go_for_abstract_events(_Name,AbstractEvents,[],[],IS,LS,OS,AbstractPath,Din) :-
    !, % optimisation: If no witness has to be evaluated, do not copy primed variables
    execute_abstract_events(AbstractEvents,[],[],IS,LS,OS,AbstractPath,Din).

go_for_abstract_events(Name,AbstractEvents,VWitnesses,PWitnesses,IS,LS,OS,AbstractPath,Din) :-
    % copy a primed version of all values in the outstate into the local state
    copy_primed(OS,LS,NewLS),
    % evaluate witnesses for dropped abstract vars
    evaluate_witnesses_for_abstract_vars(VWitnesses,Name,IS,NewLS,OS,Din,D1),
    % evaluate witnesses for dropped parameters
    evaluate_witnesses_for_abstract_parameters(PWitnesses,Name,IS,NewLS,AbsLS,Params,PValues,D1,D2),
    % continue with the next refinement level
    execute_abstract_events(AbstractEvents,Params,PValues,IS,AbsLS,OS,AbstractPath,D2).

init_trace_of_event(Name,Section,Parameters,ParaValues,FullGuard,[event(Path),eventtrace(Trace)],RestPath,D2) :-
    Path = [event(Name,ParaValues)|RestPath],
    eventtrace_init(Name,Desc,Trace),
    eventtrace_add(event(Name,Section),Desc,D1),
    eventtrace_add(true_guard(Parameters,ParaValues,FullGuard),D1,D2).

select_event(Events,Params,PValues,IS,LS,Event,Name,Din,Dout) :-
    member(TEvent,Events),
    get_texpr_expr(TEvent,Event),
    Event = rlevent(Name,Section,_Status,_Params,Guard,_Thms,_Act,_VWit,_PWit,_Unmod,_Evt),
    b_test_boolean_expression_cs(Guard,LS,IS,'event guard',Name),
    eventtrace_add(event(Name,Section),Din,D1),
    eventtrace_add(true_guard(Params,PValues,Guard),D1,Dout).

setup_event_state(Parameters,ParaValues,NormalisedParaValues,ParamTypedVals,LS) :-
    empty_state(EmptyState),
    set_up_typed_localstate(Parameters,ParaValues,ParamTypedVals,EmptyState,LS,positive),
    store:l_expand_and_normalise_values(ParaValues,NormalisedParaValues,Parameters).

variant_condition(anticipated, integer, Pre, Post) :- !, less_than_equal(Post,Pre).

variant_condition(anticipated, set(_), Pre, Post) :- !, check_subset_of(Post,Pre).

variant_condition(convergent, integer, Pre, Post) :- !, less_than(Post,Pre).

variant_condition(convergent, set(_), Pre, Post) :- !, strict_subset_of(Post,Pre).

variant_is_not_negative(Variant,_CType,IS,LS,Value,Din,Dout) :-
    get_texpr_type(Variant, set(_)),!,
    % if variant is of type set, it cannot be negative
    % nevertheless, we compute its value here to check later if the set has been decreased
    if( b_compute_expression_nowf(Variant,LS,IS,Value,'variant (set)',0),
    % Daniel: why are LS & IS swapped ?
    Din=Dout,
    eventtrace_store_event_error(event_wd_error(Variant,variant),Din,Dout)).

variant_is_not_negative(Variant,CType,IS,LS,Value,Din,Dout) :-
    if( b_compute_expression_nowf(Variant,LS,IS,Value,'variant (not negative check)',0),
    % Daniel: why are LS & IS swapped ?
    ( less_than(Value, int(0)) ->
    eventtrace_store_event_error(variant_negative(CType,Variant,Value),Din,Dout)
    ; eventtrace_add(variant_checked_pre(CType,Variant,Value),Din,Dout)),
    eventtrace_store_event_error(event_wd_error(Variant,variant),Din,Dout)).

witness_substate(Witness,OrigLS,LS,TId,Value,Predicate,TypedVals,WitnessLS,ExtLS) :-
    extract_witness(Witness,TId,Id,_Type,Predicate),
    set_up_typed_localstate([TId],[Value],TypedVals,LS,ExtLS,positive),
    add_var_to_localstate(Id,Value,OrigLS,WitnessLS).