| 1 | :- module(user_interaction,[user_interaction/8, | |
| 2 | user_interaction_distinguishing_input/3, | |
| 3 | user_interaction_distinguishing_transition/4, | |
| 4 | user_interaction_add_missing_transition/4, | |
| 5 | user_interaction_intial_negative_inputs/2, | |
| 6 | user_interaction_affected_vars_if_condition/1, | |
| 7 | user_interaction_consider_if/1]). | |
| 8 | ||
| 9 | :- use_module(synthesis(synthesis_util)). | |
| 10 | :- use_module(probsrc(specfile),[expand_const_and_vars_to_full_store/2]). | |
| 11 | :- use_module(probsrc(bmachine),[b_get_machine_variables/1]). | |
| 12 | :- use_module(probsrc(translate),[translate_bexpression/2,translate_bvalue/2]). | |
| 13 | :- use_module(probsrc(bsyntaxtree),[add_texpr_infos/3]). | |
| 14 | :- use_module(library(lists),[append/2,maplist/3,is_list/1,nth0/3]). | |
| 15 | ||
| 16 | % general user interaction | |
| 17 | user_interaction(Vars,TExamplesAssumingNo,TExamplesAssumingYes,PositiveIn,NegativeIn,PositiveOut, | |
| 18 | NegativeOut,SynthesisType) :- | |
| 19 | format("Please select positive and negative examples~n~n",[]) , | |
| 20 | maplist(expand_const_and_vars_to_full_store,TExamplesAssumingNo,ExamplesAssumingNo) , | |
| 21 | maplist(expand_const_and_vars_to_full_store,TExamplesAssumingYes,ExamplesAssumingYes) , | |
| 22 | user_interaction_graduate_examples(Vars,ExamplesAssumingNo,no,TempPosIn1,TempNegIn1,TempPosOut1, | |
| 23 | TempNegOut1,Type1) , nl , | |
| 24 | user_interaction_graduate_examples(Vars,ExamplesAssumingYes,yes,TempPosIn2,TempNegIn2,TempPosOut2, | |
| 25 | TempNegOut2,Type2) , nl , | |
| 26 | user_interaction_add_further_examples(Vars,TempPosIn3,TempNegIn3,TempPosOut3,TempNegOut3) , | |
| 27 | % type is either action or a variable | |
| 28 | (nonvar(Type1) -> Type = Type1 ; Type = Type2) , | |
| 29 | append([TempPosIn1,TempPosIn2,TempPosIn3],PosInput) , | |
| 30 | append([TempNegIn1,TempNegIn2,TempNegIn3],NegInput) , | |
| 31 | append([TempPosOut1,TempPosOut2,TempPosOut3],PosOutput) , | |
| 32 | append([TempNegOut1,TempNegOut2,TempNegOut3],NegOutput) , | |
| 33 | check_examples_from_user(Vars,PosInput,NegInput,PosOutput,NegOutput,TPositiveIn,NegativeIn, | |
| 34 | TPositiveOut,NegativeOut) , | |
| 35 | user_interaction_aux(Type,Vars,ExamplesAssumingNo,TPositiveIn,NegativeIn,TPositiveOut, | |
| 36 | NegativeOut,PositiveIn,NegativeIn,PositiveOut,NegativeOut,SynthesisType). | |
| 37 | ||
| 38 | % when synthesizing an invariant or guard we have to delete all negative inputs from | |
| 39 | % the positive ones, because we replace outputs either by 'TRUE' or 'FALSE' transitions can be equal | |
| 40 | user_interaction_aux(Type,Vars,ExamplesAssumingNo,TTPositiveIn,NegativeIn,TTPositiveOut,NegativeOut, | |
| 41 | PositiveIn,NegativeIn,PositiveOut,NegativeOut,SynthesisType) :- | |
| 42 | var(Type) , ! , | |
| 43 | % either type is set during user_interaction (action) or we need to set it (guard or invariant) | |
| 44 | determine_synthesis_type(ExamplesAssumingNo,TTPositiveIn,TTPositiveOut,SynthesisType) , | |
| 45 | post_select_transitions(NegativeIn,TTPositiveIn,TTPositiveOut,TPositiveIn,TPositiveOut) , | |
| 46 | check_examples_from_user(Vars,TPositiveIn,NegativeIn,TPositiveOut,NegativeOut,PositiveIn, | |
| 47 | NegativeIn,PositiveOut,NegativeOut). | |
| 48 | user_interaction_aux(action,_,_,PositiveIn,NegativeIn,PositiveOut,NegativeOut,PositiveIn,NegativeIn, | |
| 49 | PositiveOut,NegativeOut,action). | |
| 50 | ||
| 51 | % before synthesizing an action we ask the user if knows whether we need an if-statement or not | |
| 52 | user_interaction_consider_if(Answer) :- | |
| 53 | format("Should we consider an if-statement? [yes/no]",[]) , | |
| 54 | read(Answer) , | |
| 55 | member(Answer,[yes,no]). | |
| 56 | ||
| 57 | user_interaction_intial_negative_inputs(VarNames,NegativeInputStates) :- | |
| 58 | user_interaction_intial_negative_inputs(VarNames,[],NegativeInputStates). | |
| 59 | user_interaction_intial_negative_inputs(VarNames,Acc,NegativeInputStates) :- | |
| 60 | format("Do you know some invalid input states?~n",[]) , | |
| 61 | read(InvalidInputState) , | |
| 62 | user_interaction_intial_negative_inputs_aux(VarNames,InvalidInputState,Acc,NegativeInputStates). | |
| 63 | user_interaction_intial_negative_inputs_aux(_,no,Acc,Acc). | |
| 64 | user_interaction_intial_negative_inputs_aux(VarNames,RawInputState,Acc,[InputNodes|NewAcc]) :- | |
| 65 | is_list(RawInputState) , | |
| 66 | synthesis_util:pretty_example_to_ast_nodes(RawInputState,VarNames,InputNodes) , | |
| 67 | user_interaction_intial_negative_inputs(VarNames,Acc,NewAcc). | |
| 68 | ||
| 69 | % when we detected an if-statement for the given examples we ask the user if he knows which | |
| 70 | % variables take part in the statement's condition | |
| 71 | user_interaction_affected_vars_if_condition(AffectedVars) :- | |
| 72 | format("Which variables are involved in the statement's condition?~n [list of varnames/skip]",[]) , | |
| 73 | read(AffectedVars). | |
| 74 | ||
| 75 | % if an example from model checking was edited by the user we synthesize actions | |
| 76 | determine_synthesis_type(_,_,_,Type) :- | |
| 77 | % so the type is already set | |
| 78 | Type == action , !. | |
| 79 | determine_synthesis_type(ExamplesAssumingNo,PosInput,PosOutput,Type) :- | |
| 80 | determine_synthesis_type_aux(ExamplesAssumingNo,NegInput,NegOutput) , | |
| 81 | % else if an example assumed no is graduated as valid by the user we synthesize invariants | |
| 82 | ( ((member(In,NegInput) , member(In,PosInput)) , | |
| 83 | (nth0(IndexNeg,NegInput,In) , nth0(IndexPos,PosInput,In) , | |
| 84 | nth0(IndexNeg,NegOutput,Out) , nth0(IndexPos,PosOutput,Out))) | |
| 85 | -> Type = invariant | |
| 86 | % else we synthesize guards | |
| 87 | ; Type = guard). | |
| 88 | ||
| 89 | determine_synthesis_type_aux([],[],[]). | |
| 90 | determine_synthesis_type_aux([(AssumingNoIn,AssumingNoOut)|T],[NegInput|NTIn],[NegOutput|NTOut]) :- | |
| 91 | findall(Node,(member(bind(_,Val),AssumingNoIn) , value_to_ast(Val,b(N,Type,_)) , | |
| 92 | Node = b(N,Type,_)),NegInput) , | |
| 93 | findall(Node,(member(bind(_,Val),AssumingNoOut) , value_to_ast(Val,b(N,Type,_)) , | |
| 94 | Node = b(N,Type,_)),NegOutput) , | |
| 95 | determine_synthesis_type_aux(T,NTIn,NTOut). | |
| 96 | ||
| 97 | % delete negative inputs from positive ones | |
| 98 | post_select_transitions(NegativeIn,TPositiveIn,TPositiveOut,PositiveIn,PositiveOut) :- | |
| 99 | findall(Pos,(member(Pos,TPositiveIn) , \+member(Pos,NegativeIn)),PositiveIn) , | |
| 100 | % get all matching outputs | |
| 101 | findall(Index,(member(Pos,PositiveIn) , nth0(Index,TPositiveIn,Pos)),Indices) , | |
| 102 | findall(PosOut,(member(PosOut,TPositiveOut) , nth0(Index,TPositiveOut,PosOut) , | |
| 103 | member(Index,Indices)),PositiveOut). | |
| 104 | ||
| 105 | % expect at least one positive example | |
| 106 | %check_examples_from_user(Vars,[],NegInput,[],NegOutput,[PosInput],NegInput,[PosOutput],NegOutput) :- | |
| 107 | % format("Add one positive example~n",[]) , | |
| 108 | % read(Example) , | |
| 109 | % Example = (TPosInput-->TPosOutput) , | |
| 110 | % synthesis_util:pretty_example_to_ast_nodes(TPosInput,Vars,PosInput) , | |
| 111 | % synthesis_util:pretty_example_to_ast_nodes(TPosOutput,Vars,PosOutput). | |
| 112 | check_examples_from_user(_,PosInput,NegInput,PosOutput,NegOutput,PosInput,NegInput,PosOutput,NegOutput). | |
| 113 | ||
| 114 | user_interaction_add_missing_transition(Vars,Input,Output,VarNodes) :- | |
| 115 | format("Do you want to add a transition? [example/no] ",[]) , | |
| 116 | read(Example) , | |
| 117 | Example = (TPosIn-->TPosOut) , ! , | |
| 118 | TPosIn \= [] , TPosOut \= [] , | |
| 119 | findall(VarName,member(b(identifier(VarName),_,_),Vars),TempVarNames) , | |
| 120 | b_get_machine_variables(MachineVars) , | |
| 121 | length(MachineVars,VarAmount) , | |
| 122 | length(TPosIn,L1) , length(TPosOut,L2) , | |
| 123 | ((L1 \= VarAmount ; L2 \= VarAmount) | |
| 124 | -> format("Please name the variables you refer to (list expected):",[]) , | |
| 125 | read(VarNames) , | |
| 126 | findall(b(identifier(VarName),Type,[]),(member(VarName,VarNames) , | |
| 127 | member(b(identifier(VarName),Type,_),MachineVars)),VarNodes) , | |
| 128 | length(VarNodes,L1) | |
| 129 | ; VarNodes = MachineVars , | |
| 130 | VarNames = TempVarNames) , | |
| 131 | synthesis_util:pretty_example_to_ast_nodes(TPosIn,VarNames,PosIn) , | |
| 132 | synthesis_util:pretty_example_to_ast_nodes(TPosOut,VarNames,PosOut) , | |
| 133 | user_interaction_add_missing_transition(Vars,FPosIn,FPosOut,_) , % same var nodes expected | |
| 134 | Input = [PosIn|FPosIn] , Output = [PosOut|FPosOut]. | |
| 135 | user_interaction_add_missing_transition(_,[],[],[]). | |
| 136 | ||
| 137 | % user interaction to optionally add further examples | |
| 138 | user_interaction_add_further_examples(Vars,PosIn,NegIn,PosOut,NegOut) :- | |
| 139 | format("Do you want to add any other example? [example/no] ",[]) , | |
| 140 | read(Example) , | |
| 141 | Example = (_-->_) , ! , | |
| 142 | user_interaction_graduate_examples(Vars,[Example],none,TempPosIn1,TempNegIn1,TempPosOut1,TempNegOut1,_) , | |
| 143 | user_interaction_add_further_examples(Vars,TempPosIn2,TempNegIn2,TempPosOut2,TempNegOut2) , | |
| 144 | append(TempPosIn1,TempPosIn2,PosIn) , | |
| 145 | append(TempNegIn1,TempNegIn2,NegIn) , | |
| 146 | append(TempPosOut1,TempPosOut2,PosOut) , | |
| 147 | append(TempNegOut1,TempNegOut2,NegOut). | |
| 148 | user_interaction_add_further_examples(_,[],[],[],[]). | |
| 149 | ||
| 150 | % user interaction to select positive and negative examples | |
| 151 | % Assuming is either 'yes'/'no' or 'none' if no information is given | |
| 152 | % if the user changes an example unify Type with action, else Type will stay a variable | |
| 153 | user_interaction_graduate_examples(_,[],_,[],[],[],[],_). | |
| 154 | user_interaction_graduate_examples(Vars,[Example|R],Assuming,PosIn,NegIn,PosOut,NegOut,Type) :- | |
| 155 | % examples can be bindings from the solver | |
| 156 | (Example = (In,Out) | |
| 157 | -> maplist(example_bindings_to_ast_nodes,[In,Out],[InputNodes,OutputNodes]) , | |
| 158 | maplist(translate_bexpression,InputNodes,RawInput) , | |
| 159 | maplist(translate_bexpression,OutputNodes,RawOutput) | |
| 160 | ; Example = (RawInput-->RawOutput) , | |
| 161 | findall(Name,member(b(identifier(Name),_,_),Vars),VarNames) , | |
| 162 | synthesis_util:pretty_example_to_ast_nodes(RawInput,VarNames,InputNodes) , | |
| 163 | synthesis_util:pretty_example_to_ast_nodes(RawOutput,VarNames,OutputNodes)) , | |
| 164 | % only give the opportunity to change output of examples from model checking, | |
| 165 | % if there is no assuming it's an example from the user | |
| 166 | (Assuming = none | |
| 167 | -> format("~nIs ~w-->~w a valid example? [yes/no] ",[RawInput,RawOutput]) | |
| 168 | ; format("~nIs ~w-->~w a valid example? (assuming ~w) [yes/no/edit] ",[RawInput,RawOutput,Assuming])) , | |
| 169 | read(Answer) , | |
| 170 | (Answer = edit | |
| 171 | -> Type = action , | |
| 172 | user_interaction_change_output(RawInput,RawOutput,TNewOutput) , | |
| 173 | synthesis_util:pretty_example_to_ast_nodes(TNewOutput,Vars,NewOutput) , | |
| 174 | user_interaction_graduate_examples_aux([InputNodes|OldPosIn],OldNegIn,[NewOutput|OldPosOut], | |
| 175 | OldNegOut,PosIn,NegIn,PosOut,NegOut) | |
| 176 | ; ((Answer = yes | |
| 177 | -> user_interaction_graduate_examples_aux([InputNodes|OldPosIn],OldNegIn, | |
| 178 | [OutputNodes|OldPosOut],OldNegOut,PosIn,NegIn,PosOut,NegOut) | |
| 179 | ; Answer = no , | |
| 180 | user_interaction_graduate_examples_aux(OldPosIn,[InputNodes|OldNegIn],OldPosOut, | |
| 181 | [OutputNodes|OldNegOut],PosIn,NegIn,PosOut,NegOut)))) , | |
| 182 | user_interaction_graduate_examples(Vars,R,Assuming,OldPosIn,OldNegIn,OldPosOut,OldNegOut,Type). | |
| 183 | ||
| 184 | % unify variables | |
| 185 | user_interaction_graduate_examples_aux(PosInput,NegInput,PosOutput,NegOutput,PosInput,NegInput,PosOutput,NegOutput). | |
| 186 | ||
| 187 | user_interaction_change_output(Input,Output,NewOutput) :- | |
| 188 | format("New output of ~w:~n",[Input]) , | |
| 189 | read(TempNewOutput) , | |
| 190 | ((length(Input,L) , length(TempNewOutput,L)) | |
| 191 | -> NewOutput = TempNewOutput | |
| 192 | ; format("Wrong amount of variables. Please try again",[]) , nl , | |
| 193 | user_interaction_change_output(Input,Output,NewOutput)). | |
| 194 | ||
| 195 | % user decides between to non-equivalent solutions by graduating a distinguishing | |
| 196 | % input/state | |
| 197 | user_interaction_distinguishing_input(Type,solution(Distinguishing),Answer) :- | |
| 198 | findall(Value,member(binding(_,Value,_),Distinguishing),Values) , | |
| 199 | maplist(translate_bvalue,Values,PrettyValues) , | |
| 200 | (Type = invariant | |
| 201 | -> format("~nIs ~w a valid state? [yes/no]",[PrettyValues]) | |
| 202 | ; format("~nIs ~w a valid input? [yes/no]",[PrettyValues])) , | |
| 203 | read(TAnswer) , | |
| 204 | (\+member(TAnswer,[yes,no]) | |
| 205 | -> user_interaction_distinguishing_input(Type,solution(Distinguishing),Answer) | |
| 206 | ; Answer = TAnswer). | |
| 207 | % or transition as valid or invalid | |
| 208 | user_interaction_distinguishing_transition(solution(Distinguishing),CurrentVars,Answer,OutputNodes) :- | |
| 209 | findall(Value,(member(binding(Var,Temp,_),Distinguishing) , \+bmachine_eventb:is_primed_id(Var) , | |
| 210 | translate_bvalue(Temp,Value)),In) , | |
| 211 | findall(Node,(member(binding(Var,Temp,_),Distinguishing) , bmachine_eventb:is_primed_id(Var) , | |
| 212 | value_to_ast(Temp,TNode) , | |
| 213 | add_texpr_infos(TNode,[synthesis(machinevar,Var)],Node)),TOutputNodes) , | |
| 214 | maplist(translate_bexpression,TOutputNodes,Out) , | |
| 215 | format("~nIs ~w-->~w a valid transition? [yes/no]",[In,Out]) , | |
| 216 | read(TAnswer) , | |
| 217 | (TAnswer = no | |
| 218 | -> user_interaction_distinguishing_transition_aux(CurrentVars,Answer,OutputNodes) | |
| 219 | ; Answer = yes , | |
| 220 | OutputNodes = TOutputNodes). | |
| 221 | user_interaction_distinguishing_transition_aux(CurrentVars,Answer,DistOut) :- | |
| 222 | format("Please give the desired output: [example/none]~n",[]) , | |
| 223 | read(Answer) , | |
| 224 | (Answer = none | |
| 225 | -> DistOut = none | |
| 226 | ; findall(Name,member(b(identifier(Name),_,_),CurrentVars),CurrentVarNames) , | |
| 227 | synthesis_util:pretty_example_to_ast_nodes(Answer,CurrentVarNames,DistOut)). |