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