1 :- module(location_vars_to_program,[location_vars_to_program/9]).
2
3 :- use_module(synthesis(synthesis_util)).
4 :- use_module(synthesis(logging)).
5
6 :- use_module(probsrc(btypechecker),[prime_identifier/2]).
7 :- use_module(probsrc(bsyntaxtree),[conjunct_predicates/2,get_texpr_info/2,add_texpr_infos/3]).
8 :- use_module(probsrc(module_information),[module_info/2]).
9
10 :- use_module(library(sets),[subset/2]).
11 :- use_module(library(lists),[append/2,remove_dups/2,maplist/3,delete/3]).
12
13 :- module_info(group,synthesis).
14 :- module_info(description,'This module defines the translation from a distribution of location variables to a B/Event-B AST.').
15
16 % Convert location values to a program represented as an ast.
17 % Collect all location variables that are part of the solution (no deadcode).
18 location_vars_to_program(Library,Type,CurrentVars,LocationVars,M1,Parameter,solution(Bindings),UsedLVars,AST) :-
19 % split by temporary input and output variables
20 findall(Out,(member(Out,LocationVars) , Out = b(identifier(Name),_,_) ,
21 atom_concat(lo,_,Name)),LocationVarsOut) ,
22 delete(LocationVars,LocationVarsOut,LocationVarsIn) ,
23 % get output location variable defined in the last program line
24 (location_vars_to_program_aux(Type,M1,Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,UsedLVars,AST)
25 -> true ; synthesis_log(location_vars_to_program_and_fail(Type,Library,LocationVarsIn,LocationVarsOut,Parameter,Bindings))) , !.
26 location_vars_to_program_aux(action,M1,Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,UsedLVars,AST) :-
27 length(CurrentVars,OutputAmount) ,
28 M0 is M1 - OutputAmount ,
29 % Translate the program of each output variable and conjunct them. For constraint solving we need
30 % conjunctions which are replaced with parallel executions after finding the final solution.
31 get_program_for_output_var(Library,M0,M1,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,TempUsedLVars,ASTList) ,
32 remove_dups(TempUsedLVars,UsedLVars) ,
33 conjunct_predicates(ASTList,AST).
34 location_vars_to_program_aux(Type,M1,Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,UsedLVars,AST) :-
35 Type \= action ,
36 % Output values of the program are also located to the last line (root), but we want to find the output
37 % location variable. Here, we just have one output whose location variable is named 'lo0'.
38 get_variable_value_from_bindings(Bindings, Root, ProBValue),
39 ProBValue = int(M1),
40 atom_concat(lo,Suffix,Root) , \+atom_concat(value,_,Suffix) ,
41 location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,Root,UsedLVars,AST).
42
43 % For synthesis of actions:
44 % If we have more than one output we need to collect the partial programs and insert
45 % assignments with primed variables.
46 get_program_for_output_var(_,M0,M0,_,_,_,_,_,[],[]).
47 get_program_for_output_var(Library,M0,ProgramLine,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,UsedLVars,[Assignment|T]) :-
48 get_variable_value_from_bindings(Bindings, Root, ProBValue),
49 ProBValue = int(ProgramLine),
50 atom_concat(lo,_,Root) ,
51 % get the output location mapped to this line of the program
52 get_location_var_node_by_info_term(LocationVarsOut,synthesis(program_line(ProgramLine)),RootNode) ,
53 % and get the corresponding machine var using the info term synthesis/2
54 get_texpr_info(RootNode,RootInfo) ,
55 member(synthesis(machinevar,MachineVar),RootInfo) ,
56 member(b(identifier(MachineVar),MachineVarType,MachineVarInfo),CurrentVars) ,
57 location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,Root,TempUsedLVars,AST) ,
58 prime_identifier(b(identifier(MachineVar),MachineVarType,MachineVarInfo),PrimedVar) ,
59 Assignment = b(equal(PrimedVar,AST),pred,[]) ,
60 NProgramLine is ProgramLine - 1 ,
61 get_program_for_output_var(Library,M0,NProgramLine,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,R,T) ,
62 append(TempUsedLVars,R,UsedLVars).
63
64 set_type(b(member(b(Elm,EType,EInfo),Set),NodeType,MInfo),b(member(b(Elm,EType,EInfo),NSet),NodeType,MInfo)) :-
65 set_type_aux(EType,Set,NSet).
66 set_type(b(Node,Type,Info),b(NewNode,Type,Info)) :-
67 Node =.. [Head,Arg] , Head \= identifier ,
68 set_type(Arg,NArg) ,
69 NewNode =.. [Head,NArg].
70 set_type(b(Node,Type,Info),b(NewNode,Type,Info)) :-
71 Node =.. [Head,Arg1,Arg2] ,
72 set_type(Arg1,NArg1) ,
73 set_type(Arg2,NArg2) ,
74 NewNode =.. [Head,NArg1,NArg2].
75 set_type(Node,Node).
76
77 set_type_aux(Type,b(set_extension(Set),_,SInfo),b(set_extension(NSet),set(Type),SInfo)) :-
78 maplist(set_type_aux(Type),Set,NSet).
79 set_type_aux(Type,b(Node,_,Info),b(Node,Type,Info)).
80
81 % if_then_else
82 location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,LocationVarName,[LocationVarNode|RUsedLVars],IfThenElseAst) :-
83 LocationVarNode = b(identifier(LocationVarName),_,Info) ,
84 member(LocationVarNode,LocationVarsOut) ,
85 subset([synthesis(type,Type),synthesis(Component,output)],Info) ,
86 atom_concat(if_then_else,_,Component) , ! ,
87 % find the location variable of the statement's condition
88 get_location_var_node_by_info_term(LocationVarsIn,synthesis(Component,condition),b(identifier(ConditionName),_,_)) ,
89 location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,ConditionName,ConditionUsedLVars,ConditionAst) ,
90 % find location variables for truth and falsity outputs of the if_then_else statement
91 get_location_var_node_by_info_term(LocationVarsIn,synthesis(Component,true_out),b(identifier(TrueOutName),_,_)) ,
92 location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,TrueOutName,TrueOutUsedLVars,TrueOutAst) ,
93 get_location_var_node_by_info_term(LocationVarsIn,synthesis(Component,false_out),b(identifier(FalseOutName),_,_)) ,
94 location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,FalseOutName,FalseOutUsedLVars,FalseOutAst) ,
95 append([ConditionUsedLVars,TrueOutUsedLVars,FalseOutUsedLVars],RUsedLVars) ,
96 IfThenElseAst = b(if_then_else(ConditionAst,TrueOutAst,FalseOutAst),Type,[]).
97 % machine constants or operation parameters
98 location_to_ast(_,_,_,LocationVarsOut,_,_,LocationVarName,[LocationVarNode],IdNode) :-
99 LocationVarNode = b(identifier(LocationVarName),_,Info) ,
100 member(LocationVarNode,LocationVarsOut) ,
101 (subset([synthesis(_,output),synthesis(machineconstant,IdNode)],Info) ;
102 subset([synthesis(_,output),synthesis(operationparameter,IdNode)],Info)) , !.
103 % constant sets like NATURAL or INTEGER
104 location_to_ast(_,_,_,LocationVarsOut,_,_,LocationVarName,[LocationVarNode],AST) :-
105 LocationVarNode = b(identifier(LocationVarName),_,Info) ,
106 member(LocationVarNode,LocationVarsOut) ,
107 subset([synthesis(ConstantName,output),synthesis(type,Type)],Info) ,
108 atom_concat(constant_set,_,ConstantName) , ! ,
109 % export as infinite set
110 get_single_constant_or_set_operator_id(Type,_,AST).
111 location_to_ast(_,_,_,LocationVarsOut,_,_,LocationVarName,[LocationVarNode],Node) :-
112 LocationVarNode = b(identifier(LocationVarName),_,Info) ,
113 member(LocationVarNode,LocationVarsOut) ,
114 member(synthesis(ConstantName,output),Info) ,
115 member(synthesis(ParamType,ParamName),Info) ,
116 (ParamType = param_single ; ParamType = param_set) ,
117 atom_concat(constant,_,ConstantName) , ! ,
118 member(synthesis(type,Type),Info) ,
119 (Type = set(global(Independent)) ; Type = global(Independent)) ,
120 (ParamType = param_set
121 -> Node = b(set_extension([b(identifier(ParamName),global(Independent),Info)]),set(global(Independent)),Info)
122 ; ParamType = param_single ,
123 Node = b(identifier(ParamName),global(Independent),Info)).
124 % synthesized constants that have been enumerated by the solver
125 location_to_ast(_,_,_,LocationVarsOut,_,Bindings,LocationVarName,[LocationVarNode],Node) :-
126 LocationVarNode = b(identifier(LocationVarName),_,Info) ,
127 member(LocationVarNode,LocationVarsOut) ,
128 member(synthesis(ConstantName,output),Info) ,
129 atom_concat(constant,_,ConstantName) , ! ,
130 % get constant solution, either integer or boolean
131 get_variable_value_from_bindings(Bindings, ConstantName, ProBValue),
132 member(synthesis(type,Type),Info) ,
133 Node = b(value(ProBValue),Type,Info).
134 % output
135 % one input parameter
136 location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,LocationVarName,[LocationVarNode|RUsedLVars],AstNode) :-
137 LocationVarNode = b(identifier(LocationVarName),_,InfoOut) ,
138 member(LocationVarNode,LocationVarsOut) ,
139 subset([synthesis(Component,output),synthesis(type,Type)],InfoOut) ,
140 synthesis_util:delete_numbers_from_atom(Component,ComponentName) ,
141 member(ComponentName,[negation,card,size,max,min,general_union,general_intersection,reverse,range,domain,skip,convert_bool,first,last]) , ! ,
142 % find input location variables
143 get_location_var_node_by_info_term(LocationVarsIn,synthesis(Component,input),b(identifier(InName),_,_)) ,
144 location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,InName,RUsedLVars,InputAST) ,
145 Node =.. [ComponentName,InputAST] ,
146 single_input_location_to_ast_aux(ComponentName,b(Node,Type,InfoOut),InputAST,AstNode).
147 % two input parameters
148 location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,LocationVarName,UsedLVars,AST) :-
149 LocationVarNode = b(identifier(LocationVarName),_Type,InfoOut) ,
150 member(LocationVarNode,LocationVarsOut) , ! ,
151 member(synthesis(Component,output),InfoOut) ,
152 % find input location variables
153 get_location_var_node_by_info_term(LocationVarsIn,synthesis(Component,left_input),b(identifier(InName1),_,_)) ,
154 get_location_var_node_by_info_term(LocationVarsIn,synthesis(Component,right_input),b(identifier(InName2),_,_)) ,
155 location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,InName1,
156 LeftUsedLVars,LeftInputAST) ,
157 location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,InName2,
158 RightUsedLVars,RightInputAST) ,
159 synthesis_util:delete_numbers_from_atom(Component,ComponentName) ,
160 % get the type from the output nodes information
161 member(synthesis(type,Type),InfoOut) ,
162 Node =.. [ComponentName,LeftInputAST,RightInputAST] ,
163 append([[LocationVarNode],LeftUsedLVars,RightUsedLVars],UsedLVars) ,
164 set_type(b(Node,Type,InfoOut),AST).
165 % Input values that are located in the first lines of a synthesized program, thus, the location is
166 % less than the parameter amount.
167 location_to_ast(_,CurrentVars,LocationVarsIn,_,Parameter,Bindings,LocationVarName,[],b(identifier(VarName),Type,Info)) :-
168 get_variable_value_from_bindings(Bindings, LocationVarName, ProBValue),
169 ProBValue = int(Value),
170 Value < Parameter , ! ,
171 get_varname_for_input_enumeration(LocationVarsIn,Value,VarName) ,
172 member(b(identifier(VarName),Type,Info),CurrentVars).
173 % An input location that is connected to another operator's output location.
174 location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,LocationVarName,UsedLVars,AST) :-
175 get_variable_value_from_bindings(Bindings, LocationVarName, ProBValue),
176 ProBValue = int(Value),
177 Value >= Parameter ,
178 % temporary output variable
179 LocationOut = b(identifier(LocationOutName),_,_) ,
180 % get output defined at corresponding location
181 get_variable_value_from_bindings(Bindings, LocationOutName, ProBValue),
182 ProBValue = int(Value),
183 LocationVarName \= LocationOutName ,
184 member(LocationOut,LocationVarsOut) ,
185 location_to_ast(Library,CurrentVars,LocationVarsIn,LocationVarsOut,Parameter,Bindings,
186 LocationOutName,UsedLVars,AST).
187
188 get_variable_value_from_bindings(Bindings, VarName, Value) :-
189 member(binding(VarName, Value, _), Bindings).
190 get_variable_value_from_bindings(Bindings, VarName, Value) :-
191 member(bind(VarName, Value), Bindings).
192
193 % The argument 'Value' defines the line for which we want to find the corresponding machine variable.
194 % When creating the behavioral constraint we mark those input location variables with the term synthesis(input(Value))
195 % so that we are now able to find a specific input variable and determine its name (also in the info: synthesis(machinevar,VarName))
196 % without assuming any order of the variables (!).
197 get_varname_for_input_enumeration([],_,_) :- fail.
198 get_varname_for_input_enumeration([LocationVar|_],Value,VarName) :-
199 LocationVar = b(_,_,Info) ,
200 member(synthesis(input(Value)),Info) ,
201 member(synthesis(machinevar,VarName),Info) , !.
202 get_varname_for_input_enumeration([_|T],Value,VarName) :-
203 get_varname_for_input_enumeration(T,Value,VarName).
204
205 % "skip" component is not translated explicitly, i.e. we just return the input parameter its input is mapped to but
206 % we need to add the skip component node's info to the parameter node
207 single_input_location_to_ast_aux(skip,b(_,_,Info),ComponentAstNode,ComponentAstNodeWithInfo) :-
208 add_texpr_infos(ComponentAstNode,Info,ComponentAstNodeWithInfo).
209 single_input_location_to_ast_aux(Component,AstNode,_,AstNode) :-
210 Component \= skip.