user_interaction

check_examples_from_user(_,PosInput,NegInput,PosOutput,NegOutput,PosInput,NegInput,PosOutput,NegOutput).

determine_synthesis_type(_,_,_,Type) :-
    % so the type is already set
    Type == action , !.

determine_synthesis_type(ExamplesAssumingNo,PosInput,PosOutput,Type) :-
    determine_synthesis_type_aux(ExamplesAssumingNo,NegInput,NegOutput) ,
    % else if an example assumed no is graduated as valid by the user we synthesize invariants
    ( ((member(In,NegInput) , member(In,PosInput)) ,
    (nth0(IndexNeg,NegInput,In) , nth0(IndexPos,PosInput,In) ,
    nth0(IndexNeg,NegOutput,Out) , nth0(IndexPos,PosOutput,Out)))
    -> Type = invariant
    % else we synthesize guards
    ; Type = guard).

determine_synthesis_type_aux([],[],[]).

determine_synthesis_type_aux([(AssumingNoIn,AssumingNoOut)|T],[NegInput|NTIn],[NegOutput|NTOut]) :-
    findall(Node,(member(bind(_,Val),AssumingNoIn) , value_to_ast(Val,b(N,Type,_)) ,
    Node = b(N,Type,_)),NegInput) ,
    findall(Node,(member(bind(_,Val),AssumingNoOut) , value_to_ast(Val,b(N,Type,_)) ,
    Node = b(N,Type,_)),NegOutput) ,
    determine_synthesis_type_aux(T,NTIn,NTOut).

post_select_transitions(NegativeIn,TPositiveIn,TPositiveOut,PositiveIn,PositiveOut) :-
    findall(Pos,(member(Pos,TPositiveIn) , \+member(Pos,NegativeIn)),PositiveIn) ,
    % get all matching outputs
    findall(Index,(member(Pos,PositiveIn) , nth0(Index,TPositiveIn,Pos)),Indices) ,
    findall(PosOut,(member(PosOut,TPositiveOut) , nth0(Index,TPositiveOut,PosOut) ,
    member(Index,Indices)),PositiveOut).

user_interaction(Vars,TExamplesAssumingNo,TExamplesAssumingYes,PositiveIn,NegativeIn,PositiveOut,
    NegativeOut,SynthesisType) :-
    format("Please select positive and negative examples~n~n",[]) ,
    maplist(expand_const_and_vars_to_full_store,TExamplesAssumingNo,ExamplesAssumingNo) ,
    maplist(expand_const_and_vars_to_full_store,TExamplesAssumingYes,ExamplesAssumingYes) ,
    user_interaction_graduate_examples(Vars,ExamplesAssumingNo,no,TempPosIn1,TempNegIn1,TempPosOut1,
    TempNegOut1,Type1) , nl ,
    user_interaction_graduate_examples(Vars,ExamplesAssumingYes,yes,TempPosIn2,TempNegIn2,TempPosOut2,
    TempNegOut2,Type2) , nl ,
    user_interaction_add_further_examples(Vars,TempPosIn3,TempNegIn3,TempPosOut3,TempNegOut3) ,
    % type is either action or a variable
    (nonvar(Type1) -> Type = Type1 ; Type = Type2) ,
    append([TempPosIn1,TempPosIn2,TempPosIn3],PosInput) ,
    append([TempNegIn1,TempNegIn2,TempNegIn3],NegInput) ,
    append([TempPosOut1,TempPosOut2,TempPosOut3],PosOutput) ,
    append([TempNegOut1,TempNegOut2,TempNegOut3],NegOutput) ,
    check_examples_from_user(Vars,PosInput,NegInput,PosOutput,NegOutput,TPositiveIn,NegativeIn,
    TPositiveOut,NegativeOut) ,
    user_interaction_aux(Type,Vars,ExamplesAssumingNo,TPositiveIn,NegativeIn,TPositiveOut,
    NegativeOut,PositiveIn,NegativeIn,PositiveOut,NegativeOut,SynthesisType).

user_interaction_add_further_examples(Vars,PosIn,NegIn,PosOut,NegOut) :-
    format("Do you want to add any other example? [example/no] ",[]) ,
    read(Example) ,
    Example = (_-->_) , ! ,
    user_interaction_graduate_examples(Vars,[Example],none,TempPosIn1,TempNegIn1,TempPosOut1,TempNegOut1,_) ,
    user_interaction_add_further_examples(Vars,TempPosIn2,TempNegIn2,TempPosOut2,TempNegOut2) ,
    append(TempPosIn1,TempPosIn2,PosIn) ,
    append(TempNegIn1,TempNegIn2,NegIn) ,
    append(TempPosOut1,TempPosOut2,PosOut) ,
    append(TempNegOut1,TempNegOut2,NegOut).

user_interaction_add_further_examples(_,[],[],[],[]).

user_interaction_add_missing_transition(Vars,Input,Output,VarNodes) :-
    format("Do you want to add a transition? [example/no] ",[]) ,
    read(Example) ,
    Example = (TPosIn-->TPosOut) , ! ,
    TPosIn \= [] , TPosOut \= [] ,
    findall(VarName,member(b(identifier(VarName),_,_),Vars),TempVarNames) ,
    b_get_machine_variables(MachineVars) ,
    length(MachineVars,VarAmount) ,
    length(TPosIn,L1) , length(TPosOut,L2) ,
    ((L1 \= VarAmount ; L2 \= VarAmount)
    -> format("Please name the variables you refer to (list expected):",[]) ,
    read(VarNames) ,
    findall(b(identifier(VarName),Type,[]),(member(VarName,VarNames) ,
    member(b(identifier(VarName),Type,_),MachineVars)),VarNodes) ,
    length(VarNodes,L1)
    ; VarNodes = MachineVars ,
    VarNames = TempVarNames) ,
    synthesis_util:pretty_example_to_ast_nodes(TPosIn,VarNames,PosIn) ,
    synthesis_util:pretty_example_to_ast_nodes(TPosOut,VarNames,PosOut) ,
    user_interaction_add_missing_transition(Vars,FPosIn,FPosOut,_) , % same var nodes expected
    Input = [PosIn|FPosIn] , Output = [PosOut|FPosOut].

user_interaction_add_missing_transition(_,[],[],[]).

user_interaction_affected_vars_if_condition(AffectedVars) :-
    format("Which variables are involved in the statement's condition?~n [list of varnames/skip]",[]) ,
    read(AffectedVars).

user_interaction_aux(Type,Vars,ExamplesAssumingNo,TTPositiveIn,NegativeIn,TTPositiveOut,NegativeOut,
    PositiveIn,NegativeIn,PositiveOut,NegativeOut,SynthesisType) :-
    var(Type) , ! ,
    % either type is set during user_interaction (action) or we need to set it (guard or invariant)
    determine_synthesis_type(ExamplesAssumingNo,TTPositiveIn,TTPositiveOut,SynthesisType) ,
    post_select_transitions(NegativeIn,TTPositiveIn,TTPositiveOut,TPositiveIn,TPositiveOut) ,
    check_examples_from_user(Vars,TPositiveIn,NegativeIn,TPositiveOut,NegativeOut,PositiveIn,
    NegativeIn,PositiveOut,NegativeOut).

user_interaction_aux(action,_,_,PositiveIn,NegativeIn,PositiveOut,NegativeOut,PositiveIn,NegativeIn,
    PositiveOut,NegativeOut,action).

user_interaction_change_output(Input,Output,NewOutput) :-
    format("New output of ~w:~n",[Input]) ,
    read(TempNewOutput) ,
    ((length(Input,L) , length(TempNewOutput,L))
    -> NewOutput = TempNewOutput
    ; format("Wrong amount of variables. Please try again",[]) , nl ,
    user_interaction_change_output(Input,Output,NewOutput)).

user_interaction_consider_if(Answer) :-
    format("Should we consider an if-statement? [yes/no]",[]) ,
    read(Answer) ,
    member(Answer,[yes,no]).

user_interaction_distinguishing_input(Type,solution(Distinguishing),Answer) :-
    findall(Value,member(binding(_,Value,_),Distinguishing),Values) ,
    maplist(translate_bvalue,Values,PrettyValues) ,
    (Type = invariant
    -> format("~nIs ~w a valid state? [yes/no]",[PrettyValues])
    ; format("~nIs ~w a valid input? [yes/no]",[PrettyValues])) ,
    read(TAnswer) ,
    (\+member(TAnswer,[yes,no])
    -> user_interaction_distinguishing_input(Type,solution(Distinguishing),Answer)
    ; Answer = TAnswer).

user_interaction_distinguishing_transition(solution(Distinguishing),CurrentVars,Answer,OutputNodes) :-
    findall(Value,(member(binding(Var,Temp,_),Distinguishing) , \+bmachine_eventb:is_primed_id(Var) ,
    translate_bvalue(Temp,Value)),In) ,
    findall(Node,(member(binding(Var,Temp,_),Distinguishing) , bmachine_eventb:is_primed_id(Var) ,
    value_to_ast(Temp,TNode) ,
    add_texpr_infos(TNode,[synthesis(machinevar,Var)],Node)),TOutputNodes) ,
    maplist(translate_bexpression,TOutputNodes,Out) ,
    format("~nIs ~w-->~w a valid transition? [yes/no]",[In,Out]) ,
    read(TAnswer) ,
    (TAnswer = no
    -> user_interaction_distinguishing_transition_aux(CurrentVars,Answer,OutputNodes)
    ; Answer = yes ,
    OutputNodes = TOutputNodes).

user_interaction_distinguishing_transition_aux(CurrentVars,Answer,DistOut) :-
    format("Please give the desired output: [example/none]~n",[]) ,
    read(Answer) ,
    (Answer = none
    -> DistOut = none
    ; findall(Name,member(b(identifier(Name),_,_),CurrentVars),CurrentVarNames) ,
    synthesis_util:pretty_example_to_ast_nodes(Answer,CurrentVarNames,DistOut)).

user_interaction_graduate_examples(_,[],_,[],[],[],[],_).

user_interaction_graduate_examples(Vars,[Example|R],Assuming,PosIn,NegIn,PosOut,NegOut,Type) :-
    % examples can be bindings from the solver
    (Example = (In,Out)
    -> maplist(example_bindings_to_ast_nodes,[In,Out],[InputNodes,OutputNodes]) ,
    maplist(translate_bexpression,InputNodes,RawInput) ,
    maplist(translate_bexpression,OutputNodes,RawOutput)
    ; Example = (RawInput-->RawOutput) ,
    findall(Name,member(b(identifier(Name),_,_),Vars),VarNames) ,
    synthesis_util:pretty_example_to_ast_nodes(RawInput,VarNames,InputNodes) ,
    synthesis_util:pretty_example_to_ast_nodes(RawOutput,VarNames,OutputNodes)) ,
    % only give the opportunity to change output of examples from model checking,
    % if there is no assuming it's an example from the user
    (Assuming = none
    -> format("~nIs ~w-->~w a valid example? [yes/no] ",[RawInput,RawOutput])
    ; format("~nIs ~w-->~w a valid example? (assuming ~w) [yes/no/edit] ",[RawInput,RawOutput,Assuming])) ,
    read(Answer) ,
    (Answer = edit
    -> Type = action ,
    user_interaction_change_output(RawInput,RawOutput,TNewOutput) ,
    synthesis_util:pretty_example_to_ast_nodes(TNewOutput,Vars,NewOutput) ,
    user_interaction_graduate_examples_aux([InputNodes|OldPosIn],OldNegIn,[NewOutput|OldPosOut],
    OldNegOut,PosIn,NegIn,PosOut,NegOut)
    ; ((Answer = yes
    -> user_interaction_graduate_examples_aux([InputNodes|OldPosIn],OldNegIn,
    [OutputNodes|OldPosOut],OldNegOut,PosIn,NegIn,PosOut,NegOut)
    ; Answer = no ,
    user_interaction_graduate_examples_aux(OldPosIn,[InputNodes|OldNegIn],OldPosOut,
    [OutputNodes|OldNegOut],PosIn,NegIn,PosOut,NegOut)))) ,
    user_interaction_graduate_examples(Vars,R,Assuming,OldPosIn,OldNegIn,OldPosOut,OldNegOut,Type).

user_interaction_graduate_examples_aux(PosInput,NegInput,PosOutput,NegOutput,PosInput,NegInput,PosOutput,NegOutput).

user_interaction_intial_negative_inputs(VarNames,NegativeInputStates) :-
    user_interaction_intial_negative_inputs(VarNames,[],NegativeInputStates).

user_interaction_intial_negative_inputs(VarNames,Acc,NegativeInputStates) :-
    format("Do you know some invalid input states?~n",[]) ,
    read(InvalidInputState) ,
    user_interaction_intial_negative_inputs_aux(VarNames,InvalidInputState,Acc,NegativeInputStates).

user_interaction_intial_negative_inputs_aux(_,no,Acc,Acc).

user_interaction_intial_negative_inputs_aux(VarNames,RawInputState,Acc,[InputNodes|NewAcc]) :-
    is_list(RawInputState) ,
    synthesis_util:pretty_example_to_ast_nodes(RawInputState,VarNames,InputNodes) ,
    user_interaction_intial_negative_inputs(VarNames,Acc,NewAcc).