1 | % (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | :- module(proz, [open_proz_file/2]). | |
6 | ||
7 | :- use_module(library(lists)). | |
8 | :- use_module(library(ordsets),[ord_union/3,ord_subtract/3]). | |
9 | ||
10 | :- use_module(probsrc(tools)). | |
11 | :- use_module(probsrc(debug)). | |
12 | :- use_module(probsrc(self_check)). | |
13 | :- use_module(probsrc(b_state_model_check)). | |
14 | :- use_module(probsrc(store)). | |
15 | :- use_module(probsrc(error_manager)). | |
16 | ||
17 | :- use_module(probsrc(bmachine_structure)). | |
18 | :- use_module(probsrc(bsyntaxtree)). | |
19 | :- use_module(probsrc(bsyntaxtree_quantifiers),[create_z_let/6]). | |
20 | :- use_module(probsrc(b_ast_cleanup),[clean_up/3,clean_up_l_wo_optimizations/4, clean_up_l_with_optimizations/4]). | |
21 | %:- use_module(probsrc(translate),[print_machine/1]). | |
22 | ||
23 | :- use_module(prozsrc(z_tools)). | |
24 | :- use_module(prozsrc(fuzzfile)). | |
25 | :- use_module(prozsrc(schemaexpansion)). | |
26 | :- use_module(prozsrc(dependence),[schema_dependence/2]). | |
27 | :- use_module(prozsrc(zenvironment)). | |
28 | :- use_module(prozsrc(z_typechecker)). | |
29 | :- use_module(prozsrc(ztransformations)). | |
30 | :- use_module(prozsrc(consistencycheck)). | |
31 | :- use_module(prozsrc(subexpressions)). | |
32 | ||
33 | :- use_module(probsrc(module_information)). | |
34 | :- module_info(group,proz). | |
35 | :- module_info(description,'This is the central ProZ module for translating Z specification into B.'). | |
36 | ||
37 | :- set_prolog_flag(double_quotes, codes). | |
38 | ||
39 | /* --------------- FUZZ ----------------- */ | |
40 | ||
41 | reset_proz :- | |
42 | reset_fuzzfile, | |
43 | retractall(unchanged_vars_for_partial_zoperation(_,_)). | |
44 | ||
45 | open_proz_file(File,BMachine) :- | |
46 | reset_proz, | |
47 | load_fuzzfile(File), | |
48 | get_z_filename(File,Filename), | |
49 | ? | init_fuzz_mode(Filename,BMachine). |
50 | % (translate:print_machine(BMachine) -> true ; write('pretty-printing the translated B machine failed.\n')). | |
51 | ||
52 | get_z_filename(File,Filename) :- | |
53 | get_tail_filename(File,Filename1), | |
54 | (split_filename(Filename1,Filename,_) -> true ; Filename1 = Filename). | |
55 | ||
56 | ||
57 | /* Initialize all basic types */ | |
58 | init_fuzz_mode(Filename,BMachine) :- | |
59 | ? | typed_specification(Dependencies,TypedSpecification), |
60 | ||
61 | /* initialise the z schemas */ | |
62 | ? | fuzzschemas(TypedSpecification,Schemas), |
63 | classify_schemas(Schemas, Dependencies, Classification), | |
64 | ||
65 | /* construct any statements for initialisation and operations */ | |
66 | construct_init(Schemas,Classification,InitAny), | |
67 | construct_operations(Schemas,Classification,Ops), | |
68 | ||
69 | optimize_anys(anys(InitAny,Ops),anys(InitAny2,Ops2)), | |
70 | ||
71 | get_proz_settings(Schemas,Classification,Filename,TypedSpecification,Settings), | |
72 | ||
73 | ? | create_z_machine(Filename,TypedSpecification,InitAny2,Ops2,Schemas,Classification,Settings,BMachine). |
74 | ||
75 | :- public fuzzschemas/2, classify_schemas/3, construct_init/3, construct_operations/3, | |
76 | optimize_anys/2, get_proz_settings/5. % because Spider cannot deal with ~~mnf | |
77 | ||
78 | typed_specification(Dependencies,TypedSpecification) :- | |
79 | get_z_definitions(InitialZSpec), | |
80 | ||
81 | schema_dependence(InitialZSpec,Dependencies), | |
82 | ||
83 | /* simplify without having type information */ | |
84 | ? | simplify_untyped(InitialZSpec,ZSpecification), |
85 | ||
86 | /* add type informations */ | |
87 | global_environment(ZSpecification,_,TypedSpecification1), | |
88 | ||
89 | /* simplify the specification */ | |
90 | simplify_typed(TypedSpecification1,TypedSpecification). | |
91 | ||
92 | create_z_machine(Filename, TypedSpecification, InitAny, Ops, Schemas, Classification, Settings, BMachine) :- | |
93 | create_machine(Filename,Empty), | |
94 | ||
95 | /* register new data types */ | |
96 | set_given_sets(TypedSpecification,Empty,MSets), | |
97 | ? | set_freetypes(TypedSpecification,MSets,MFreetypes), |
98 | ||
99 | /* register initialisation and operations */ | |
100 | ? | set_init(InitAny,MFreetypes,MInit), |
101 | ? | set_operations(Ops,MInit,MOps), |
102 | ||
103 | set_variables(Schemas,Classification,MOps,MVars), | |
104 | /* register_scope(Schemas,Classification), */ | |
105 | ? | set_constants(TypedSpecification,MVars,MConstants), |
106 | ||
107 | set_settings(Settings, MConstants, MSettings), | |
108 | ||
109 | b_global_sets:b_clear_global_set_type_definitions, % TO DO: do the full pre-compiling before cleaning up !?!? | |
110 | % cleanup will need to get deferred sets, ... | |
111 | ||
112 | clean_up_machine(MSettings,BMachine). | |
113 | ||
114 | :- public set_init/3, set_operations/3, set_given_sets/3, set_freetypes/3, | |
115 | set_variables/4, set_constants/3, set_settings/3, | |
116 | clean_up_machine/2. % because Spider does not deal with ~~mnf | |
117 | ||
118 | simplify_untyped --> | |
119 | zcheck('initial Z specification',[]), | |
120 | ||
121 | /* replace simple freetypes with named sets */ | |
122 | freetype2namedsets, zcheck('after replacing simple freetypes by named sets',[]), | |
123 | ||
124 | /* remove the declaration of the ignore pregen */ | |
125 | remove_ignore_decl, zcheck('after removing proz-ignore declarations',[]), | |
126 | ||
127 | /* exchanged simple references to schemas by SEXPR(sref(...)) */ | |
128 | clearsrefs, zcheck('after clearsrefs',[]), | |
129 | ||
130 | /* substitute references to abbreviations with their definition */ | |
131 | removeabbreviations, zcheck('after removal of abbreviations',[]), | |
132 | ||
133 | /* flatten the specification */ | |
134 | ? | sexpansion, zcheck('after schema expansion',[nlabel(scalc)]). |
135 | ||
136 | simplify_typed --> | |
137 | /* remove schema expressions */ | |
138 | removesexpr, ztcheck('after removing schema expressions',[nlabel(scalc)]), | |
139 | ||
140 | /* some general simplifications */ | |
141 | ggsimplify, ztcheck('after some general simplifications',[nlabel(scalc)]). | |
142 | ||
143 | zcheck(Msg,A,Z,Z) :- check_z_structure(Z,Msg,A). | |
144 | ztcheck(Msg,A,Z,Z) :- check_z_structuret(Z,Msg,A). | |
145 | ||
146 | %******************************************************************************* | |
147 | % optimization of ANY-statements | |
148 | optimize_anys --> | |
149 | exists_to_anys, | |
150 | optimize_global_predicates. | |
151 | ||
152 | optimize_global_predicates(anys(InitAny,OldOps),anys(InitAny,NewOps)) :- | |
153 | global_predicates(InitAny,OldOps,GlobalPredicates), | |
154 | remove_global_predicates(OldOps,GlobalPredicates,NewOps). | |
155 | ||
156 | % if the predicate is just of one exists predicate, we | |
157 | % merge any and exists. | |
158 | exists_to_anys(anys(OldInitAny,OldOps),anys(NewInitAny,NewOps)) :- | |
159 | exists_to_anys2(OldInitAny,NewInitAny), | |
160 | exists_to_anys_ops(OldOps,NewOps). | |
161 | exists_to_anys_ops([],[]). | |
162 | exists_to_anys_ops([op(Op,Params,Results,OldAny,ParaTypes,ResultTypes)|ORest], | |
163 | [op(Op,Params,Results,NewAny,ParaTypes,ResultTypes)|NRest]) :- | |
164 | exists_to_anys2(OldAny,NewAny), | |
165 | exists_to_anys_ops(ORest,NRest). | |
166 | exists_to_anys2(any(Vars,Types,[ti(exists(Body,Pred),bool)],LHS,RHS),NewAny) :- | |
167 | !,Body=ti(body(_,Wheres),set(schema(ZFields))), | |
168 | append(Wheres,[Pred],NPreds1), | |
169 | clean_wheret(NPreds1,NPreds), | |
170 | % todo: not safe with name clashes | |
171 | zfields2b(ZFields,EVars,ETypes), | |
172 | append(Vars,EVars,NVars), | |
173 | append(Types,ETypes,NTypes), | |
174 | exists_to_anys2(any(NVars,NTypes,NPreds,LHS,RHS),NewAny). | |
175 | exists_to_anys2(Any,Any). | |
176 | ||
177 | %******************************************************************************* | |
178 | /* extract constants, their types and properties from the specification */ | |
179 | set_constants(TypedDefs,In,Out) :- | |
180 | write_section(abstract_constants,TypedConstants,In,M), | |
181 | write_section(properties,Property,M,Out), | |
182 | ? | extract_constants2(TypedDefs, Constants, Types, Properties), |
183 | conjunct_predicates(Properties,Property), | |
184 | z_translate_typed_identifiers(Constants,Types,[],TypedConstants). | |
185 | ||
186 | extract_constants2([],[],[],[]). | |
187 | extract_constants2([Def|Rest], Constants, Types, Properties) :- | |
188 | ? | extract_constants3(Def, LocalConstants, LocalTypes, ZPropertiesTi), |
189 | !, | |
190 | ? | z_translate(ZPropertiesTi,LocalProperties), |
191 | append(LocalConstants, RestConstants, Constants), | |
192 | append(LocalTypes, RestTypes, Types), | |
193 | append(LocalProperties, RestProperties, Properties), | |
194 | ? | extract_constants2(Rest, RestConstants, RestTypes, RestProperties). |
195 | extract_constants2([_|Rest], Constants, Types, Properties) :- | |
196 | ? | extract_constants2(Rest, Constants, Types, Properties). |
197 | extract_constants3(Axdef, Constants, Types, Predicates) :- | |
198 | ti_expr(Axdef,axdef(BodyTi)),!, | |
199 | ? | extract_btypes(Axdef,Constants,Types), |
200 | ti_expr(BodyTi,body(_,Predicates)). | |
201 | extract_constants3(PredTi, [], [], [Predicate]) :- | |
202 | ti_expr(PredTi, pred(Predicate)). | |
203 | ||
204 | ||
205 | /* appends a decoration to the each variable name of the given list of | |
206 | variable names */ | |
207 | /* unused at the moment: | |
208 | decorate([],_,[]) :- !. | |
209 | decorate([Var|Vars], Deco, [Decorated|Rest]) :- | |
210 | !, | |
211 | decorate(Var, Deco, Decorated), | |
212 | decorate(Vars, Deco, Rest). | |
213 | decorate(Var, Deco, Decorated) :- | |
214 | z_translate_identifier(name(Var,Deco),Decorated). | |
215 | */ | |
216 | ||
217 | ||
218 | remove_vars(Orig,OrigTypes,[],Orig,OrigTypes) :- !. | |
219 | remove_vars(Orig,OrigTypes,[Var|Rest],ResVars,ResTypes) :- | |
220 | ? | remove_var(Orig,OrigTypes,Var,Vars,Types), |
221 | ? | remove_vars(Vars,Types,Rest,ResVars,ResTypes). |
222 | remove_var([],[],_,[],[]) :- !. | |
223 | remove_var([Var|Orig],[_|OrigTypes],Var,ResVars,ResTypes) :- | |
224 | remove_var(Orig,OrigTypes,Var,ResVars,ResTypes). | |
225 | remove_var([Var|Orig],[Type|OrigTypes],OtherVar,[Var|ResVars],[Type|ResTypes]) :- | |
226 | Var \= OtherVar, | |
227 | ? | remove_var(Orig,OrigTypes,OtherVar,ResVars,ResTypes). |
228 | ||
229 | /* Extract all schemas from the fuzz schema definitions */ | |
230 | fuzzschemas([],[]). | |
231 | fuzzschemas([Def|Rest],FSchemas) :- | |
232 | ( schema_id_body(Def,Id,Body) -> | |
233 | FSchemas = [fschema(Id, Body, Vars, Types)|FRest], | |
234 | ? | extract_btypes(Def,Vars,Types) |
235 | ; | |
236 | FSchemas = FRest), | |
237 | ? | fuzzschemas(Rest,FRest). |
238 | ||
239 | schema_id_body(Ti,Id,Body) :- ti_expr(Ti,Expr),schema_id_body2(Expr,Id,Body). | |
240 | schema_id_body2(sdef(shead(Id,[]),Body),Id,Body). | |
241 | schema_id_body2(defeq(shead(Id,[]),Body),Id,Body). | |
242 | ||
243 | %******************************************************************************* | |
244 | % Extract settings from specifications and put them into the meta data of | |
245 | % a machine | |
246 | get_proz_settings(Schemas,Classification,Filename,TypedSpecification,Settings) :- | |
247 | findall(Setting, | |
248 | get_proz_setting(Schemas,Classification,Filename,TypedSpecification,Setting), | |
249 | Settings). | |
250 | get_proz_setting(Schemas,Classification,_Filename,TypedSpecification,Setting) :- | |
251 | get_schema_by_class(settings,Classification,Schemas,ZDef,ZVars,ZTypes), | |
252 | get_proz_expr_setting(ZDef,ZVars,ZTypes,TypedSpecification,Setting). | |
253 | get_proz_setting(Schemas,Classification,_Filename,_TypedSpecification,goal(BGoal)) :- | |
254 | get_schema_by_class(goal,Classification,Schemas,ZDef,_,_), | |
255 | ti_expr(ZDef,body(_,ZGoals)), | |
256 | z_translate(ZGoals,BGoals1), | |
257 | clean_up_l_wo_optimizations(BGoals1,[],BGoals,schemas), | |
258 | conjunct_predicates(BGoals,BGoal). | |
259 | get_proz_setting(_Schemas,_Classification,_Filename,_TypedSpecification,[]). | |
260 | get_proz_expr_setting(ZDef,_ZVars,_ZTypes,TypedSpecification,animation_function(BAnim,BDefaultAnim,Images)) :- | |
261 | ( extract_def_by_equality(ZDef,'animation_function',AFType,BAnim) -> | |
262 | (extract_def_by_equality(ZDef,'animation_function_default',DFType,BDefaultAnim) -> true ; BDefaultAnim = none) | |
263 | ; extract_def_by_equality(ZDef,'animation_function_default',DFType,BDefaultAnim) -> | |
264 | BAnim = none), | |
265 | (AFType = DFType -> true ; add_error(proz,'animation_function and animation_function_default should be of the same type')), | |
266 | ( AFType = set(tuple([tuple([_,_]),ImageType])) -> | |
267 | ( extract_image_filenames(ImageType,TypedSpecification,Images) -> true | |
268 | ; add_error(proz,'Unable to map animation function to images')) | |
269 | ; | |
270 | add_error(proz,'Unexpected type of animation_function'),fail). | |
271 | ||
272 | extract_def_by_equality(ZDef,Name,Type,BExpr) :- | |
273 | get_equality(ZDef,ti(ref(name(Name,''),[]),Type),ZExpr), | |
274 | z_translate(ZExpr,BExpr1), | |
275 | clean_up(BExpr1,[],BExpr). | |
276 | get_equality(ti(body(_,ZWhere),_),Name,Equal) :- | |
277 | !,member(A,ZWhere),get_equality(A,Name,Equal),!. | |
278 | get_equality(ti(equal(X,Y),_),TName,Equal) :- | |
279 | ( X=TName -> Equal=Y | |
280 | ; Y=TName -> Equal=X). | |
281 | extract_image_filenames(given(IName),TypedSpecification,Images) :- | |
282 | memberchk(ti(namedset(IName,Elements),_),TypedSpecification), | |
283 | z_translate_identifiers(Elements,PImages), | |
284 | maplist(append_gif,PImages,Images). | |
285 | append_gif(Name,Gif) :- atom_concat(Name,'.gif',Gif). | |
286 | ||
287 | set_settings(Settings,In,Out) :- | |
288 | append_to_section(meta,[proz_settings(Settings)],In,Out). | |
289 | ||
290 | %******************************************************************************* | |
291 | % Schema classification | |
292 | ||
293 | /* Classifies each schema, i.e. assign a type (state, init, op, other) | |
294 | to each given schema */ | |
295 | classify_schemas(Schemas,Deps,[cls(init,Init),cls(state,State)|Operations]) :- | |
296 | ? | ( classify_init_state(Deps, Init, State) -> true |
297 | ; Deps= [] -> | |
298 | add_error(proz,'This Z specification has no schema and cannot be initialised.'),fail | |
299 | ; | |
300 | %debug:print_quoted(Deps),nl, | |
301 | ajoin(['Was not able to identify Z state schema.\n', | |
302 | 'Please check if there is a schema called Init that\n', | |
303 | 'references exactly one other schema (the state) in its\n', | |
304 | 'declaration part.'], Msg), | |
305 | add_error(proz,Msg),fail), | |
306 | classify_schemas(Schemas, Schemas, Deps, Init, State, Operations). | |
307 | ||
308 | :- use_module(library(lists),[sublist/5]). | |
309 | classify_init_state(Deps,'Init',State) :- | |
310 | findall(S,member(dep('Init',S),Deps),[State]). | |
311 | classify_init_state(Deps,SchemaName,State) :- | |
312 | % see if we can find another Schema with Init in its name, which references exactly one other atomic Schema | |
313 | ? | member(dep(SchemaName,_),Deps), |
314 | atom_codes(SchemaName,SCodes), | |
315 | atom_codes('Init',InitCodes1), atom_codes('init',InitCodes2), | |
316 | ? | (sublist(SCodes,InitCodes1,_,_,_) -> true ; sublist(SCodes,InitCodes2,_,_,_)), |
317 | findall(S,member(dep(SchemaName,S),Deps),[State]), % we should check that State is not Delta or Xi state schema | |
318 | add_message(proz,'Did not find Init Schema; assuming following schema to define the initialisation: ',SchemaName). | |
319 | ||
320 | classify_schemas([], _, _, _, _, []). | |
321 | classify_schemas([Schema|SRest], AllSchemas, Deps, Init, State, [cls(Class,Id)|CRest]) :- | |
322 | classify_schema(Schema, AllSchemas, Deps, Init, State, Class), | |
323 | !,Schema = fschema(Id,_,_,_), | |
324 | classify_schemas(SRest, AllSchemas, Deps, Init, State, CRest). | |
325 | classify_schemas([_|SRest], AllSchemas, Deps, Init, State, CRest) :- | |
326 | classify_schemas(SRest, AllSchemas, Deps, Init, State, CRest). | |
327 | ||
328 | classify_schema(fschema('Scope',_,ScopeVars,_), AllSchemas, _, _, State, scope) :- | |
329 | member(fschema(State,_,StateVars,_),AllSchemas), | |
330 | all_members(ScopeVars,StateVars),!. | |
331 | classify_schema(fschema('ProZ_Goal',_,ScopeVars,_), AllSchemas, _, _, State, goal) :- | |
332 | member(fschema(State,_,StateVars,_),AllSchemas), | |
333 | all_members(ScopeVars,StateVars),!. | |
334 | classify_schema(fschema('ProZ_Settings',_,_,_), _AllSchemas, _, _, _State, settings) :- !. | |
335 | classify_schema(fschema('Invariant',_,InvVars,_), AllSchemas, _, _, State, inv) :- | |
336 | ? | member(fschema(State,_,StateVars,_),AllSchemas), |
337 | all_members(InvVars,StateVars),!. | |
338 | classify_schema(Schema, AllSchemas, Deps, Init, State, op) :- | |
339 | Schema = fschema(Id,_,_,_), | |
340 | Id \= State, Id \= Init, | |
341 | is_operation(AllSchemas, Deps, Schema, State), | |
342 | !. | |
343 | ||
344 | :- dynamic unchanged_vars_for_partial_zoperation/2. | |
345 | :- use_module(library(ordsets),[list_to_ord_set/2,ord_member/2]). | |
346 | /* Is the given schema an operation? | |
347 | 1) It does include all variables of the state schema | |
348 | 2) It does include all variables of the after state | |
349 | 3) No other schema includes this schema */ | |
350 | is_operation(AllSchemas, Deps, fschema(Id,_,OpVars,_), State) :- | |
351 | ? | \+ member(dep(_,Id),Deps), % not included by other schema |
352 | %format('Try operation ~w with OpVars ~w and State schema is ~w~n',[Id,OpVars,State]), | |
353 | ? | member(fschema(State,_,StateVars,_),AllSchemas), % get the variables of the state schema |
354 | !, | |
355 | decorate_vars(StateVars,'\'',AfterStateVars), | |
356 | append(StateVars,AfterStateVars,NeededVars), | |
357 | (all_members(NeededVars,OpVars) -> true | |
358 | ; %format('~nSchema not recognised as operation: ~w over state variables ~w~n',[Id,StateVars]), | |
359 | OpVars \= [], | |
360 | list_to_ord_set(StateVars,SVS), | |
361 | list_to_ord_set(OpVars,OVS), | |
362 | primed_unprimed_ok(OVS,SVS), % check that all variables that are referenced occur with and without prime | |
363 | ord_subtract(SVS,OVS,Unchanged), | |
364 | formatsilent('Promoting Schema ~w to Z Operation by adding unchanged variables: ~w~n',[Id,Unchanged]), | |
365 | % TO DO: in test 1094 for System.fuzz the InitSystem operation is also recognised | |
366 | assertz(unchanged_vars_for_partial_zoperation(Id,Unchanged)) | |
367 | ). | |
368 | ||
369 | primed_unprimed_ok([],_). | |
370 | primed_unprimed_ok([name(ID,''),name(ID,'\'')|T],SVS) :- !,primed_unprimed_ok(T,SVS). | |
371 | primed_unprimed_ok([NAME|T],SVS) :- \+ ord_member(NAME,SVS),primed_unprimed_ok(T,SVS). | |
372 | ||
373 | /* unused: | |
374 | operation_variables([],[]). | |
375 | operation_variables([name(_,Deco)|Rest],NeededVars) :- | |
376 | member(Deco,['?','!']),!,operation_variables(Rest,NeededVars). | |
377 | operation_variables([Var|Rest],NeededVars) :- | |
378 | select(Var,NeededVars,RestVars), | |
379 | !,operation_variables(Rest,RestVars). | |
380 | */ | |
381 | ||
382 | get_schema_by_class(Cls,Classification,Schemas,Def,Vars,Types) :- | |
383 | memberchk(cls(Cls,Name),Classification), | |
384 | memberchk(fschema(Name,Def,Vars,Types),Schemas). | |
385 | ||
386 | %******************************************************************************* | |
387 | % Initialisation | |
388 | ||
389 | construct_init(Schemas,Classification,Any) :- | |
390 | ? | member(cls(init,Init),Classification), |
391 | ? | member(fschema(Init,Def,_,_),Schemas), |
392 | ||
393 | ? | member(cls(state,State),Classification), |
394 | ? | member(fschema(State,_,StateVars,StateTypes),Schemas),!, |
395 | ||
396 | (translate_initialisation(Def,StateVars,StateTypes,Any) -> true | |
397 | ; add_error(proz,'Internal error while translating initialisation'),fail). | |
398 | ||
399 | translate_initialisation(TDef,StateVars,StateTypes,Any) :- | |
400 | check_z_substructuret(TDef,body,'invalid Z structure in initialisation',[nlabel(scalc)]), | |
401 | findall(rename(name(Name,'\''),name(Name,'')), | |
402 | member(name(Name,''), StateVars), | |
403 | Renamings), | |
404 | rename_variablest(TDef,Renamings,TypedDef), | |
405 | ti_expr(TypedDef,body(_,TypedWhere)), | |
406 | ||
407 | decorate_vars(StateVars,'\'',ZAnyVars), | |
408 | z_translate_typed_identifiers(StateVars,StateTypes,[],Lhs), | |
409 | z_translate_typed_identifiers(ZAnyVars,StateTypes,[],Rhs), | |
410 | Any = any(ZAnyVars,StateTypes,TypedWhere,Lhs,Rhs). | |
411 | ||
412 | %create_ti(Name,Type,TI) :- ti_expr(TI,Name),ti_type(TI,Type). | |
413 | ||
414 | ||
415 | set_init(InitAny,In,Out) :- | |
416 | write_section(initialisation,Statement,In,Out), | |
417 | ? | construct_any(InitAny,[],Statement). |
418 | ||
419 | %******************************************************************************* | |
420 | % Variables and invariant | |
421 | ||
422 | set_variables(Schemas,Classification,In,Out) :- | |
423 | write_section(abstract_variables,Variables,In,M), | |
424 | write_section(invariant,Invariant,M,Out), | |
425 | ||
426 | ? | member(cls(state,State),Classification), |
427 | ? | member(fschema(State,_,ZVars,Types),Schemas),!, |
428 | ||
429 | z_translate_typed_identifiers(ZVars,Types,[],Variables), | |
430 | ||
431 | ( memberchk(cls(inv,Inv),Classification) -> | |
432 | memberchk(fschema(Inv,TypedDef,_,_),Schemas), | |
433 | println_silent('Z invariant found'), | |
434 | ti_expr(TypedDef,body(_,ZInvs)) | |
435 | ; | |
436 | ZInvs = []), | |
437 | ? | (z_translate(ZInvs,Invariants) -> true ; add_error(proz, 'Internal error while translating invariant')), |
438 | conjunct_predicates(Invariants,Invariant). | |
439 | ||
440 | ||
441 | %******************************************************************************* | |
442 | % Scope | |
443 | ||
444 | /* currently unused: | |
445 | register_scope(Schemas,Classification) :- | |
446 | ( memberchk(cls(scope,Scope),Classification) -> | |
447 | ( memberchk(fschema(Scope,TypedDef,_,_),Schemas),!, | |
448 | print('Z scope schema found'),nl, | |
449 | ti_expr(TypedDef,body(_,ZScope)), | |
450 | ( (z_translate(ZScope,ScopePredicates),conjunct_predicates(ScopePredicates,ScopePredicate)) -> | |
451 | true | |
452 | ; | |
453 | add_error(proz, 'Internal error while translating scope'),ScopePredicate=none | |
454 | ) | |
455 | ) | |
456 | ; | |
457 | ScopePredicate = none), | |
458 | set_scope_expression(ScopePredicate). | |
459 | */ | |
460 | ||
461 | %******************************************************************************* | |
462 | % Operations | |
463 | ||
464 | construct_operations(Schemas,Classification,Operations) :- | |
465 | ? | member(cls(state,State),Classification), |
466 | ? | member(fschema(State,_,StateVars,StateTypes),Schemas),!, |
467 | findall(Op,member(cls(op,Op),Classification),Ops), | |
468 | construct_operations2(Ops,Schemas,StateVars,StateTypes,Operations). | |
469 | construct_operations2([],_,_,_,[]). | |
470 | construct_operations2([Op|ORest],Schemas,StateVars,StateTypes,[Operation|OpRest]) :- | |
471 | ? | member(fschema(Op,Def,Vars,Types),Schemas),!, |
472 | ? | ( translate_operation(Op,Def,Vars,Types,StateVars,StateTypes,Params,ParaTypes,Results,ResultTypes,Any) -> |
473 | Operation = op(Op,Params,Results,Any,ParaTypes,ResultTypes), | |
474 | OpArgs =.. [Op|Params],printsilent('Z operation: '),printsilent(OpArgs),nls | |
475 | ; | |
476 | add_error(proz,'Internal error while translating operation', Op) | |
477 | ), | |
478 | construct_operations2(ORest,Schemas,StateVars,StateTypes,OpRest). | |
479 | ||
480 | set_operations(Ops,In,Out) :- | |
481 | write_section(promoted,Promoted,In,M), | |
482 | write_section(operation_bodies,Bodies,M,Out), | |
483 | ? | get_operations(Ops,Bodies,Promoted). |
484 | get_operations([],[],[]). | |
485 | get_operations([Operation|ORest],[BOperation|Brest],[Promoted|PromotedRest]) :- | |
486 | ? | get_operation(Operation,BOperation,Promoted), |
487 | ? | get_operations(ORest,Brest,PromotedRest). |
488 | get_operation(op(Op,Params,Results,Any,ParaTypes,ResultTypes),TOp,OpId) :- | |
489 | OpType = op(ResultTypes,ParaTypes), | |
490 | create_texpr(identifier(op(Op)),OpType,[],OpId), | |
491 | create_b_identifiers(Params,ParaTypes,BParams), | |
492 | create_b_identifiers(Results,ResultTypes,BResults), | |
493 | create_texpr(operation(OpId,BResults,BParams,Statement),OpType,OpInfo,TOp), % [] == Info ?? extract from Statement ?? | |
494 | add_locals([BParams,BResults],[],Locals), | |
495 | ? | construct_any(Any,Locals,Statement), |
496 | get_texpr_info(Statement,StmtInfo), | |
497 | include(is_operation_info,StmtInfo,OpInfo). | |
498 | create_b_identifiers([],[],[]). | |
499 | create_b_identifiers([Name|Nrest],[Type|Trest],[Id|Irest]) :- | |
500 | create_texpr(identifier(Name),Type,[],Id), | |
501 | create_b_identifiers(Nrest,Trest,Irest). | |
502 | ||
503 | is_operation_info(modifies(_)). | |
504 | is_operation_info(reads(_)). | |
505 | ||
506 | translate_operation(OpName,Def,Vars,Types,StateVars,StateTypes,Params,ParamTypes,Result,ResultTypes,Any) :- | |
507 | check_z_substructuret(Def,body,'invalid Z structure in operation',[nlabel(scalc)]), | |
508 | filter_vars_by_deco(Vars,Types,'?',ZParams,ParamTypes), | |
509 | filter_vars_by_deco(Vars,Types,'!',ZResult,ResultTypes), | |
510 | z_translate_identifiers(ZParams,Params), | |
511 | z_translate_identifiers(ZResult,Result), | |
512 | ||
513 | copy_result_vars(ZResult,ZAnyResults), | |
514 | ||
515 | find_unchanged(Def,UnchangedVars1,Def2), | |
516 | (unchanged_vars_for_partial_zoperation(OpName,AdditionalUnchanged) | |
517 | % check if we have an operation that does not talk about all variables, but we still classified it as an operation | |
518 | -> append(UnchangedVars1,AdditionalUnchanged,UnchangedVars) | |
519 | ; UnchangedVars = UnchangedVars1 | |
520 | ), | |
521 | findall(rename(name(Name,''),name(Name,'\'')), | |
522 | member(name(Name,''),UnchangedVars), | |
523 | Renamings1), | |
524 | findall(rename(name(Name,Deco),name(Name,'!')), | |
525 | member(name(Name,Deco),ZAnyResults), | |
526 | Renamings2), | |
527 | append(Renamings1,Renamings2,Renamings), | |
528 | ||
529 | rename_variablest(Def2,Renamings,TypedAnyPreconditions), | |
530 | ||
531 | ti_expr(TypedAnyPreconditions,body(_,TypedWheres)), | |
532 | ||
533 | append([ZParams,ZResult,UnchangedVars],NotAffectedVars), | |
534 | ? | remove_vars(StateVars,StateTypes,NotAffectedVars,ZChangedVars,ChangedVarTypes), |
535 | decorate_vars(ZChangedVars,'\'',ZChangedVarsPrimed), | |
536 | ||
537 | % extract other vars (neither input,output nor state variables) | |
538 | decorate_vars(StateVars,'\'',AfterStateVars), | |
539 | append([StateVars,AfterStateVars,ZParams,ZResult],InOutStateVars), | |
540 | ? | remove_vars(Vars,Types,InOutStateVars,ZOther,OtherTypes), |
541 | ||
542 | % Z Vars and their types in the ANY declaration | |
543 | append([ZChangedVarsPrimed,ZAnyResults,ZOther],ZAnyVars), | |
544 | append([ChangedVarTypes,ResultTypes,OtherTypes],AnyTypes), | |
545 | ||
546 | % References in the substitution | |
547 | append(ZChangedVarsPrimed,ZAnyResults,ZRightHandSubst), | |
548 | append(ZChangedVars,ZResult,ZLeftHandSubst), | |
549 | append(ChangedVarTypes,ResultTypes,LeftRightHandTypes), | |
550 | z_translate_typed_identifiers(ZLeftHandSubst,LeftRightHandTypes,[],Lhs), | |
551 | z_translate_typed_identifiers(ZRightHandSubst,LeftRightHandTypes,[],Rhs), | |
552 | ||
553 | Any = any(ZAnyVars,AnyTypes,TypedWheres,Lhs,Rhs). | |
554 | ||
555 | copy_result_vars([],[]). | |
556 | copy_result_vars([name(Name,Deco)|Rest],[name(Name,NewDeco)|NRest]) :- | |
557 | z_counter(Deco,NewDeco), | |
558 | copy_result_vars(Rest,NRest). | |
559 | ||
560 | filter_vars_by_deco([],[],_,[],[]). | |
561 | filter_vars_by_deco([V|VRest],[T|TRest],Deco,Param,ParamTypes) :- | |
562 | ( V = name(_,Deco) -> | |
563 | (Param,ParamTypes) = ([V|PRest],[T|PTRest]) | |
564 | ; | |
565 | (Param,ParamTypes) = (PRest, PTRest)), | |
566 | filter_vars_by_deco(VRest,TRest,Deco,PRest,PTRest). | |
567 | ||
568 | %******************************************************************************* | |
569 | % construction of B any statements from preformatted Z predicates and expressions | |
570 | construct_any(any(Vars,Types,ZConds,LHS,RHS),Locals1,TExpr) :- | |
571 | % Translate the guard to B: | |
572 | ? | z_translate(ZConds,BConds),conjunct_predicates(BConds,BCond), |
573 | % Translate local variables to B: | |
574 | z_translate_typed_identifiers(Vars,Types,[],Identifiers), | |
575 | add_locals([Identifiers],Locals1,Locals), | |
576 | % Determine which variables have been used by the guard: | |
577 | find_identifier_uses(BCond,Locals,GuardReads), | |
578 | % Construct inner substitution: | |
579 | construct_substitution(LHS,RHS,Locals,InnerSubst,Writes,SubstReads), | |
580 | % Construct ANY or SELECT: | |
581 | ord_union(GuardReads,SubstReads,AllReads), | |
582 | Info = [modifies(Writes),reads(AllReads)], | |
583 | construct_any_or_select(Identifiers,BCond,Info,InnerSubst,AnyOrSelect), | |
584 | create_texpr(AnyOrSelect,subst,Info,TExpr). | |
585 | construct_any_or_select([],BCond,Info,InnerSubst,select([When])) :- !, | |
586 | create_texpr(select_when(BCond,InnerSubst),subst,Info,When). | |
587 | construct_any_or_select(Identifiers,BCond,_Info,InnerSubst,any(Identifiers,BCond,InnerSubst)). | |
588 | ||
589 | construct_substitution(LHS,RHS,Locals,TExpr,Writes,Reads) :- | |
590 | create_texpr(Subst,subst,[modifies(Writes),reads(Reads)],TExpr), | |
591 | construct_substitution2(LHS,RHS,Locals,Subst,Writes,Reads). | |
592 | construct_substitution2([],[],_Locals,skip,[],[]) :- !. | |
593 | construct_substitution2(LHS,RHS,Locals,assign(LHS,RHS),Writes,Reads) :- | |
594 | get_texpr_ids(LHS,UWrites),sort(UWrites,Writes1), | |
595 | ord_subtract(Writes1,Locals,Writes), | |
596 | find_identifier_uses_l(RHS,Locals,Reads). | |
597 | ||
598 | add_locals(IdentifiersL,LocalsIn,LocalsOut) :- | |
599 | append(IdentifiersL,Identifiers), | |
600 | get_texpr_ids(Identifiers,UIds),sort(UIds,Ids), | |
601 | ord_union(LocalsIn,Ids,LocalsOut). | |
602 | ||
603 | %******************************************************************************* | |
604 | % identify predicates that are in the initialisation and in every operation | |
605 | % on the post-state | |
606 | global_predicates(InitAny,Ops,GlobalPreds) :- | |
607 | pred_init(InitAny,InitPreds), | |
608 | findall(OpAny,member(op(_,_,_,OpAny,_,_),Ops),OpAnies), | |
609 | pred_ops(OpAnies,InitPreds,GlobalPreds). | |
610 | pred_init(any(_,_,Preds,Lhs,Rhs),GPreds) :- | |
611 | create_renamings(Lhs,Rhs,Renamings), | |
612 | rename_variablest(Preds,Renamings,GPreds). | |
613 | pred_ops([],GPreds,GPreds). | |
614 | pred_ops([any(_,_,OpPreds,Lhs,Rhs)|ORest],OldPreds,GPreds) :- | |
615 | create_renamings(Rhs,Lhs,Renamings), | |
616 | filter_preds(OldPreds,OpPreds,Renamings,NewPreds), | |
617 | pred_ops(ORest,NewPreds,GPreds). | |
618 | filter_preds([],_,_,[]). | |
619 | filter_preds([Old|ORest],OpPreds,Renamings,NewPreds) :- | |
620 | rename_variablest(Old,Renamings,Comparable), | |
621 | (exists_equalt(OpPreds,Comparable) -> | |
622 | NewPreds = [Old|PRest]; | |
623 | NewPreds = PRest), | |
624 | filter_preds(ORest,OpPreds,Renamings,PRest). | |
625 | create_renamings([],[],[]). | |
626 | create_renamings([L|LRest],[R|RRest],[rename(name(LN,LD),name(RN,RD))|Rest]) :- | |
627 | get_texpr_info(L,LInfos),member(zname(LN,LD),LInfos), | |
628 | get_texpr_info(R,RInfos),member(zname(RN,RD),RInfos),!, | |
629 | create_renamings(LRest,RRest,Rest). | |
630 | ||
631 | %******************************************************************************* | |
632 | % remove global predicates from operations | |
633 | remove_global_predicates(Ops,[],Ops) :- !. | |
634 | remove_global_predicates(Ops,GlobalPredicates,NewOps) :- | |
635 | remove_globalpreds(Ops,GlobalPredicates,NewOps). | |
636 | remove_globalpreds([],_,[]). | |
637 | remove_globalpreds([op(Op,Param,Results,Any,ParaTypes,ResultTypes)|ORest],GlobalPredicates, | |
638 | [op(Op,Param,Results,NewAny,ParaTypes,ResultTypes)|NRest]) :- | |
639 | remove_globalpreds2(Any,GlobalPredicates,NewAny), | |
640 | remove_globalpreds(ORest,GlobalPredicates,NRest). | |
641 | remove_globalpreds2(any(Vars,Types,Old,LHS,RHS),GlobalPredicates, | |
642 | any(Vars,Types,New,LHS,RHS)) :- | |
643 | remove_globalpreds3(Old,GlobalPredicates,New). | |
644 | remove_globalpreds3([],_,[]). | |
645 | remove_globalpreds3([Pred|ORest],GlobalPredicates,New) :- | |
646 | ( exists_equalt(GlobalPredicates,Pred) -> | |
647 | New = NRest | |
648 | ; | |
649 | New = [Pred|NRest]), | |
650 | remove_globalpreds3(ORest,GlobalPredicates,NRest). | |
651 | ||
652 | %********************************************************************** | |
653 | % Dies und das | |
654 | ||
655 | all_members([],_). | |
656 | all_members([FirstMember|Members], List) :- | |
657 | ? | member(FirstMember, List),!, |
658 | all_members(Members, List). | |
659 | ||
660 | %******************************************************************************* | |
661 | % Z to ProB translation | |
662 | ||
663 | z_translate([],[]) :- !. | |
664 | z_translate([ZExpr|ZRest],[BExpr|BRest]) :- | |
665 | !, | |
666 | ? | z_translate(ZExpr,BExpr),z_translate(ZRest,BRest). |
667 | z_translate(ti(ZExpr,ZType),BTExpr) :- | |
668 | ? | internal2b(ZType,BType), |
669 | ? | z_translate1(ZExpr,ZType,BExpr), |
670 | create_typed_bexpr(BExpr,BType,BTExpr). | |
671 | ||
672 | create_typed_bexpr(symbolic_comprehension_set(Ids, Lhs),BType,Res) :- !, | |
673 | Res = b(comprehension_set(Ids, Lhs),BType,[prob_annotation('SYMBOLIC')]). | |
674 | create_typed_bexpr(BExpr,BType,b(BExpr,BType,[])). | |
675 | ||
676 | z_translate1(mu(Body,Computation), ZType, mu(BSet)) :- | |
677 | !, ZSet = ti(comp(Body,Computation),set(ZType)), | |
678 | ? | z_translate(ZSet,BSet). |
679 | z_translate1(ZExpr,_ZType,BExpr) :- | |
680 | ? | z_translate2(ZExpr,BExpr). |
681 | ||
682 | z_translate2(falsity, falsity) :- !. | |
683 | z_translate2(truth, truth) :- !. | |
684 | z_translate2(forall(BodyTi, ZConsequent), forall(Ids, Lhs, Rhs)) :- | |
685 | ? | !, schema_to_typed_identifiers(BodyTi,Ids,Lhs), |
686 | ? | z_translate(ZConsequent,Rhs). |
687 | z_translate2(exists(BodyTi, ZCondition), exists(Ids, BCondition)) :- | |
688 | ? | !, schema_to_typed_identifiers(BodyTi,Ids,Condition1), |
689 | ? | z_translate(ZCondition,Rhs), |
690 | conjunct_predicates([Condition1,Rhs],BCondition). | |
691 | z_translate2(lambda(BodyTi, ZExpr), lambda(Ids, Lhs, Rhs)) :- | |
692 | !, schema_to_typed_identifiers(BodyTi,Ids,Lhs), | |
693 | ? | z_translate(ZExpr,Rhs). |
694 | z_translate2(ref(name('\\emptyset',''),[]),empty_set) :- !. | |
695 | %z_translate2(ref(name('\\emptyset',''),[_TypeArg]),empty_set) :- !. % support constructs like \emptyset[\nat] ; currently argument removed in typing phase | |
696 | z_translate2(ref(name('\\nat',''),[]),integer_set('NATURAL')) :- !. | |
697 | z_translate2(ref(name('\\nat','_1'),[]),integer_set('NATURAL1')) :- !. | |
698 | z_translate2(ref(name('\\num',''),[]),integer_set('INTEGER')) :- !. | |
699 | /* In some special cases Schemas are refered just by ref(name(..)..), not by SEXPR(..) */ | |
700 | %z_translate2(ref(name(Name,Deco),Params), Env, BExpr) :- | |
701 | % named_schema(Env,Name),!, | |
702 | % z_translate(sexpr(sref(Name,Deco,Params,[])),BExpr). | |
703 | %z_translate2(ref(FreetypeName,[]), Env, 'FreetypeSet'(Id)) :- | |
704 | % zlookup(Env,data(FreetypeName,_)), | |
705 | % !,z_translate_identifier(FreetypeName,Id). | |
706 | z_translate2(ref(Name,[]), identifier(Id)) :- | |
707 | !,z_translate_identifier(Name, Id). | |
708 | z_translate2(inop(name('\\extract',''), Za, Zb), compaction(DomRes)) :- | |
709 | !, create_texpr(domain_restriction(Ba,Bb),BType,[],DomRes), | |
710 | ? | z_translate(Za,Ba),z_translate(Zb,Bb), |
711 | get_texpr_type(Bb,BType). | |
712 | z_translate2(inop(name('\\filter',''), Za, Zb), compaction(RanRes)) :- | |
713 | !, create_texpr(range_restriction(Ba,Bb),BType,[],RanRes), | |
714 | ? | z_translate(Za,Ba),z_translate(Zb,Bb), |
715 | get_texpr_type(Ba,BType). | |
716 | z_translate2(apply(Iteration,ZRel), Result) :- | |
717 | % iteration of relations. The problem of this operator is that | |
718 | % it can have negative arguments in Z but not in B | |
719 | ti_expr(Iteration, apply(Ref,ZN)), | |
720 | ti_expr(Ref, ref(name(iter,''),[])), | |
721 | ? | !, z_translate(ZN,BN), z_translate(ZRel,BRel), |
722 | get_texpr_type(BRel,BRelType), | |
723 | create_texpr(reverse(BRel),BRelType,[],Inverse), | |
724 | ( is_a_number(ZN,Value), Value >= 0 -> | |
725 | % R^x, where x is a non-negative number, we can use it directly | |
726 | Result = iteration(BRel,BN) | |
727 | ; is_a_negative_number(ZN,Value), Value >= 0 -> | |
728 | % R^-x, where x is a non-negative number, we can rewrite it into (R~)^x | |
729 | create_texpr(integer(Value),integer,[],Negation), | |
730 | Result = iteration(Inverse,Negation) | |
731 | ; | |
732 | % R^x, where x is an arbitrary expression, we surround it by if-then-else | |
733 | % to negate the x if necessary | |
734 | create_texpr(integer(0),integer,[],Zero), | |
735 | create_texpr(less_equal(Zero,BN),pred,[],NonNegative), | |
736 | create_texpr(iteration(BRel,BN),BRelType,[],Then), | |
737 | create_texpr(unary_minus(BN),integer,[],Negation), | |
738 | create_texpr(iteration(Inverse,Negation),BRelType,[],Else), | |
739 | Result = if_then_else(NonNegative,Then,Else)). | |
740 | z_translate2(inop(ZopName, Za, Zb), BBinOp) :- | |
741 | z_translate_identifier(ZopName,Zop), | |
742 | is_binary_op(Zop),!, | |
743 | ? | z_translate_binary_op(Zop,Za,Zb,BBinOp). |
744 | z_translate2(inrel(ZopName, Za, Zb), BBinOp) :- | |
745 | z_translate_identifier(ZopName,Zop), | |
746 | is_binary_op(Zop),!, | |
747 | ? | z_translate_binary_op(Zop,Za,Zb,BBinOp). |
748 | z_translate2(ingen(ZopName, Za, Zb), BBinOp) :- | |
749 | z_translate_identifier(ZopName,Zop), | |
750 | is_binary_op(Zop),!, | |
751 | ? | z_translate_binary_op(Zop,Za,Zb,BBinOp). |
752 | z_translate2(number(Value), integer(Value)) :- !. | |
753 | z_translate2(ext(ZEntities), set_extension(BEntities)) :- | |
754 | ? | !, z_translate(ZEntities, BEntities). |
755 | z_translate2(seq(ZEntities), sequence_extension(BEntities)) :- | |
756 | ? | !, z_translate(ZEntities, BEntities). |
757 | z_translate2(apply(Items,ZExpr), bag_items(BExpr)) :- | |
758 | ti_expr(Items,ref(name('items',''),[])),!, | |
759 | ? | z_translate(ZExpr,BExpr). |
760 | z_translate2(apply(ZFun, Zarg), BExpr) :- | |
761 | ti_expr(ZFun,ref(Name,[])), | |
762 | z_translate_identifier(Name,Op), | |
763 | is_unary_op(Op),!, | |
764 | ? | z_translate_unary_op(Op,Zarg,BExpr). |
765 | z_translate2(apply(ZFun, ZArg), function(BFun,BArg)) :- | |
766 | ? | !, z_translate(ZFun,BFun), z_translate(ZArg,BArg). |
767 | z_translate2(postop(Name, Zarg), BExpr) :- | |
768 | z_translate_identifier(Name,Op), | |
769 | is_unary_op(Op),!, | |
770 | ? | z_translate_unary_op(Op,Zarg,BExpr). |
771 | z_translate2(prerel(Name, Zarg), BExpr) :- | |
772 | z_translate_identifier(Name,Op), | |
773 | is_unary_op(Op),!, | |
774 | z_translate_unary_op(Op,Zarg,BExpr). | |
775 | z_translate2(pregen(Name, Zarg), BExpr) :- | |
776 | z_translate_identifier(Name,Op), | |
777 | is_unary_op(Op),!, | |
778 | ? | z_translate_unary_op(Op,Zarg,BExpr). |
779 | z_translate2(inrel(name('\\prefix',''), Za, Zb), BExpr) :- | |
780 | ? | !,z_translate(Za,Ba),z_translate(Zb,Bb), |
781 | get_texpr_type(Ba,SeqType), | |
782 | create_texpr(size(Ba),integer,[],SizeA), | |
783 | create_texpr(size(Bb),integer,[],SizeB), | |
784 | create_texpr(greater_equal(SizeB,SizeA),pred,[],GreaterEqual), | |
785 | create_texpr(restrict_front(Bb,SizeA),SeqType,[],Prefix), | |
786 | create_texpr(equal(Ba,Prefix),pred,[],Equal), | |
787 | conjunct_predicates([GreaterEqual,Equal],TypedBExpr), | |
788 | get_texpr_expr(TypedBExpr,BExpr). | |
789 | z_translate2(inrel(name('\\suffix',''), Za, Zb), BExpr) :- | |
790 | ? | !,z_translate(Za,Ba),z_translate(Zb,Bb), |
791 | get_texpr_type(Ba,SeqType), | |
792 | create_texpr(size(Ba),integer,[],SizeA), | |
793 | create_texpr(size(Bb),integer,[],SizeB), | |
794 | create_texpr(greater_equal(SizeB,SizeA),pred,[],GreaterEqual), | |
795 | create_texpr(minus(SizeB,SizeA),integer,[],Diff), | |
796 | create_texpr(restrict_tail(Bb,Diff),SeqType,[],Suffix), | |
797 | create_texpr(equal(Ba,Suffix),pred,[],Equal), | |
798 | conjunct_predicates([GreaterEqual,Equal],TypedBExpr), | |
799 | get_texpr_expr(TypedBExpr,BExpr). | |
800 | z_translate2(inrel(name('\\inseq',''), Za, Zb), BExpr) :- | |
801 | ? | !, create_in_sequence(Za,Zb,BExpr). |
802 | z_translate2(prerel(name('\\disjoint',''), Z), BExpr) :- | |
803 | ? | !, z_translate(Z,B), create_disjoint(B,BExpr). |
804 | z_translate2(inrel(name('\\partition',''), Za, Zb), partition(BSet,BSeq)) :- | |
805 | ti_expr(Za,seq(ZSeq)),!, | |
806 | z_translate(Zb,BSet), | |
807 | z_translate(ZSeq,BSeq). | |
808 | z_translate2(inrel(name('\\partition',''), Za, Zb), BExpr) :- | |
809 | ? | !, create_partition(Za,Zb,BExpr). |
810 | z_translate2(select(ZRecord, ZField), record_field(BRecord, FieldIdentifier)) :- | |
811 | ? | !, z_translate(ZRecord, BRecord), |
812 | z_translate_identifier(ZField, FieldIdentifier). | |
813 | /* Comprehension set without expression */ | |
814 | z_translate2(comp(Body, Nothing),Res) :- | |
815 | !, | |
816 | ( ti_expr(Nothing,nothing) -> true | |
817 | ; | |
818 | add_error(proz,'Encountered comprehension set with expression in translation. Should have been replaced.'), | |
819 | fail), | |
820 | ti_expr(Body,body(Decls,ZWheres)), | |
821 | ? | varlist_of_expanded_decls(Decls, Vars, Types), |
822 | z_translate_typed_identifiers(Vars,Types,[],Ids), | |
823 | ? | z_translate(ZWheres,Wheres), |
824 | conjunct_predicates(Wheres,Lhs), | |
825 | %print(comp(Ids,Lhs)),nl, | |
826 | (is_symbolic_set_comprehension(Ids,Lhs) | |
827 | -> Res = symbolic_comprehension_set(Ids, Lhs) %,print(symbolic(Ids)),nl | |
828 | ; Res = comprehension_set(Ids, Lhs)). | |
829 | z_translate2(cross([Za,Zb]), cartesian_product(Ba,Bb)) :- | |
830 | ? | !, z_translate(Za,Ba), z_translate(Zb,Bb). |
831 | z_translate2(cross([ZExpr|ZRest]), cartesian_product(BExpr,TBRest)) :- | |
832 | !, z_translate(ZExpr,BExpr), z_translate2(cross(ZRest),BRest), | |
833 | BRest=cartesian_product(BL,BR),get_texpr_type(BL,set(LType)),get_texpr_type(BR,set(RType)), | |
834 | create_texpr(BRest,set(couple(LType,RType)),[],TBRest). | |
835 | z_translate2(tuple([Za,Zb]), couple(Ba,Bb)) :- | |
836 | ? | !, z_translate(Za,Ba), z_translate(Zb,Bb). |
837 | z_translate2(tuple([ZExpr|ZRest]), couple(BExpr,TBRest)) :- | |
838 | !, z_translate(ZExpr,BExpr), z_translate2(tuple(ZRest),BRest), | |
839 | BRest=couple(BL,BR),get_texpr_type(BL,LType),get_texpr_type(BR,RType), | |
840 | create_texpr(BRest,couple(LType,RType),[],TBRest). | |
841 | z_translate2(letexpr(ZLets,ZExpr), Result) :- %let_expression(Bids,BAssignments,BExpr)) :- | |
842 | ? | !, translate_lets(ZLets,Bids,BAssignments), |
843 | z_translate(ZExpr,BExpr), | |
844 | create_z_let(expr,Bids,BAssignments,BExpr,[],b(Result,_,_)). | |
845 | z_translate2(letpred(ZLets,ZExpr), Result) :- %let_predicate(Bids,BAssignments,BExpr)) :- | |
846 | ? | !, translate_lets(ZLets,Bids,BAssignments), |
847 | ? | z_translate(ZExpr,BExpr), |
848 | ? | create_z_let(pred,Bids,BAssignments,BExpr,[],b(Result,_,_)). |
849 | z_translate2(if(ZPred,ZIf,ZElse), if_then_else(BPred,BIf,BElse)) :- | |
850 | ? | !, z_translate(ZPred,BPred), |
851 | ? | z_translate(ZIf,BIf), z_translate(ZElse,BElse). |
852 | z_translate2(inrel(Name,Za,Zb), member(Couple,Relation)) :- | |
853 | !,z_translate(Za,Ba),z_translate(Zb,Bb), | |
854 | z_translate_identifier(Name,Id), | |
855 | get_texpr_type(Ba,TypeA), get_texpr_type(Bb,TypeB), | |
856 | create_texpr(couple(Ba,Bb),couple(TypeA,TypeB),[],Couple), | |
857 | create_texpr(identifier(Id),set(couple(TypeA,TypeB)),[],Relation). | |
858 | ||
859 | % Internal constructs | |
860 | z_translate2(binding(Bindings), rec(Fields)) :- | |
861 | !, create_fields_for_binding(Bindings,Fields). | |
862 | z_translate2(ftconstant(Freetype,Case),value(freeval(FreetypeId,ConstId,term(ConstId)))) :- | |
863 | !,z_translate_identifier(Freetype,FreetypeId), | |
864 | z_translate_identifier(Case,ConstId). | |
865 | z_translate2(ftconstructor(Freetype,Case,ZExpr), | |
866 | freetype_constructor(FreetypeId,CaseId,BExpr)) :- | |
867 | ? | !,z_translate(ZExpr,BExpr), |
868 | z_translate_identifier(Freetype,FreetypeId), | |
869 | z_translate_identifier(Case,CaseId). | |
870 | z_translate2(ftdestructor(Freetype,Case,ZExpr), | |
871 | freetype_destructor(FreetypeId,CaseId,BExpr)) :- | |
872 | ? | !,z_translate(ZExpr,BExpr), |
873 | z_translate_identifier(Freetype,FreetypeId), | |
874 | z_translate_identifier(Case,CaseId). | |
875 | z_translate2(ftcase(Freetype,Case,ZExpr), | |
876 | freetype_case(FreetypeId,CaseId,BExpr)) :- | |
877 | ? | !,z_translate(ZExpr,BExpr), |
878 | z_translate_identifier(Freetype,FreetypeId), | |
879 | z_translate_identifier(Case,CaseId). | |
880 | ||
881 | z_translate2(basetype(set(Type)), Expr) :- | |
882 | !,translate_basetype2(Type,Expr). | |
883 | ||
884 | z_translate2(reclet(ZId,ZSet), recursive_let(BId,BSet) ) :- | |
885 | !,z_translate(ZId,BId), | |
886 | % TODO: recursive_let accepts only comprehension sets as argument, | |
887 | % maybe this should be checked here (lambda should be ok, too, because | |
888 | % it's converted to a comprehension set | |
889 | ? | z_translate(ZSet,BSet1), |
890 | add_texpr_infos(BSet1,[prob_annotation('SYMBOLIC')],BSet). | |
891 | ||
892 | z_translate2(ZBinOp, BBinOp) :- | |
893 | functor(ZBinOp,ZopName,2), | |
894 | is_binary_op(ZopName),!, | |
895 | arg(1,ZBinOp,Za), arg(2,ZBinOp,Zb), | |
896 | ? | z_translate_binary_op(ZopName,Za,Zb,BBinOp). |
897 | z_translate2(ZUnOp, BUnOp) :- | |
898 | functor(ZUnOp,ZopName,1), | |
899 | is_unary_op(ZopName),!, | |
900 | arg(1,ZUnOp,Zarg), | |
901 | ? | z_translate_unary_op(ZopName,Zarg,BUnOp). |
902 | ||
903 | z_translate2(ZExpr,_) :- | |
904 | add_error(proz,'Unmatched Z expression',ZExpr), | |
905 | fail. | |
906 | ||
907 | % added by Leuschel to mark certain set comprehensions as symbolic | |
908 | % TO DO: look with Daniel Plagge whether rec__ should always be symbolic, and whether other sets should be put symbolic | |
909 | is_symbolic_set_comprehension([TID],_) :- | |
910 | get_texpr_id(TID,ID), | |
911 | atom_codes(ID,C), | |
912 | append("rec__",_,C). % rec__ are special variables introduced in ztransformations:removesexpr2 for Schema fields | |
913 | ||
914 | is_a_negative_number(ZExpr,N) :- | |
915 | ti_expr(ZExpr,apply(Ref,Num)), | |
916 | ti_expr(Ref,ref(name('(-)',''),[])), | |
917 | is_a_number(Num,N). | |
918 | is_a_number(ZExpr,N) :- | |
919 | ti_expr(ZExpr,number(N)). | |
920 | ||
921 | z_translate_binary_op(ZopName,Za,Zb,Bop) :- | |
922 | z_binary_op(ZopName,BopName),!, | |
923 | ? | z_translate(Za,Ba),z_translate(Zb,Bb), |
924 | Bop =.. [BopName,Ba,Bb]. | |
925 | ||
926 | z_translate_unary_op(ZopName,Zarg,Bop) :- | |
927 | z_unary_operator(ZopName, BopName),!, | |
928 | ? | z_translate(Zarg, Barg), |
929 | Bop =.. [BopName, Barg]. | |
930 | ||
931 | translate_basetype(Type,TExpr) :- | |
932 | create_texpr(BExpr,set(BType),[],TExpr), | |
933 | internal2b(Type,BType), | |
934 | translate_basetype2(Type,BExpr). | |
935 | ||
936 | translate_basetype2(num,integer_set('INTEGER')). | |
937 | translate_basetype2(given(Name), value(global_set(Id))) :- z_translate_identifier(Name,Id). | |
938 | translate_basetype2(freetype(Name), freetype_set(Id)) :- z_translate_identifier(Name,Id). | |
939 | translate_basetype2(set(T), pow_subset(B)) :- translate_basetype(T,B). | |
940 | translate_basetype2(tuple([A,B]), cartesian_product(TA,TB)) :- | |
941 | !,translate_basetype(A,TA), | |
942 | translate_basetype(B,TB). | |
943 | translate_basetype2(tuple([A,B,C|Rest]), cartesian_product(TA,TBRest)) :- | |
944 | translate_basetype(A,TA), | |
945 | translate_basetype(tuple([B,C|Rest]),BRest), | |
946 | BRest = cartesian_product(BL,BR), | |
947 | get_texpr_type(BL,set(LType)),get_texpr_type(BR,set(RType)), | |
948 | create_texpr(BRest,set(couple(LType,RType)),[],TBRest). | |
949 | translate_basetype2(schema(ZFields),struct(Rec)) :- | |
950 | translate_bt_fields(ZFields,BFields,FieldTypes), | |
951 | create_texpr(rec(BFields),record(FieldTypes),[],Rec). | |
952 | translate_bt_fields([],[],[]). | |
953 | translate_bt_fields([ZField|ZRest],[BField|BRest],[FieldType|TRest]) :- | |
954 | translate_bt_field(ZField,BField,FieldType), | |
955 | translate_bt_fields(ZRest,BRest,TRest). | |
956 | translate_bt_field(field(Name,T),field(FieldId,B),field(FieldId,set(BType))) :- | |
957 | internal2b(T,BType), | |
958 | z_translate_identifier(Name,FieldId), | |
959 | translate_basetype(T,B). | |
960 | ||
961 | schema_to_typed_identifiers(BodyTi,Ids,Condition) :- | |
962 | ti_type(BodyTi,set(schema(ZFields))), | |
963 | ? | zfields2b(ZFields,Vars,Types), |
964 | z_translate_typed_identifiers(Vars,Types,[],Ids), | |
965 | ||
966 | ti_expr(BodyTi,body(_,WhereTi)), | |
967 | ? | z_translate(WhereTi,Wheres), |
968 | conjunct_predicates(Wheres,Condition). | |
969 | ||
970 | create_in_sequence(Za,Zb,BExpr) :- | |
971 | ? | z_translate(Za,Ba),z_translate(Zb,Bb), |
972 | get_texpr_type(Ba,BSeqType), BSeqType = set(couple(integer,BElemType)), | |
973 | ti_type(Za,ZSeqType), ZSeqType = set(tuple([num,ZElemType])), | |
974 | translate_basetype(ZElemType,BaseSet), | |
975 | create_texpr(identifier('__card'),integer,[],C), | |
976 | create_texpr(identifier('__i'),integer,[],I), | |
977 | create_texpr(identifier('__la'),BSeqType,[],La), | |
978 | create_texpr(identifier('__lb'),BSeqType,[],Lb), | |
979 | create_texpr(identifier('__offset'),integer,[],Offset), | |
980 | create_texpr(let_predicate([La,Lb],[Ba,Bb],Conjunction),pred,[],TypedBExpr), | |
981 | create_texpr(seq(BaseSet),set(BSeqType),[],Sequences), | |
982 | create_texpr(member(La,Sequences),pred,[],Asequence), | |
983 | create_texpr(member(Lb,Sequences),pred,[],Bsequence), | |
984 | create_texpr(card(La),integer,[],CardA), | |
985 | create_texpr(card(Lb),integer,[],CardB), | |
986 | create_texpr(minus(CardB,CardA),integer,[],Diff), | |
987 | create_texpr(let_predicate([C],[Diff],Exists),pred,[],Let), | |
988 | create_texpr(integer(0),integer,[],Zero), | |
989 | create_texpr(interval(Zero,Diff),integer,[],Interval), | |
990 | create_texpr(member(Offset,Interval),pred,[],InInterval), | |
991 | create_texpr(conjunct(InInterval,Forall),pred,[],Pred), | |
992 | create_texpr(forall([I],InDomain,Equal),pred,[],Forall), | |
993 | create_texpr(domain(Ba),integer,[],Domain), | |
994 | create_texpr(member(I,Domain),pred,[],InDomain), | |
995 | create_texpr(equal(ElemA,ElemB),pred,[],Equal), | |
996 | create_texpr(function(Ba,I),BElemType,[],ElemA), | |
997 | create_texpr(add(I,Offset),integer,[],I2), | |
998 | create_texpr(function(Bb,I2),BElemType,[],ElemB), | |
999 | create_exists([Offset],Pred,Exists), | |
1000 | conjunct_predicates([Asequence,Bsequence,Let],Conjunction), | |
1001 | get_texpr_expr(TypedBExpr,BExpr). | |
1002 | ||
1003 | create_disjoint(B, let_predicate([D],[Domain],Forall)) :- | |
1004 | get_texpr_type(B,set(couple(integer,set(ElemType)))), | |
1005 | create_texpr(identifier('__d'),set(integer),[],D), | |
1006 | create_texpr(identifier('__i'),integer,[],I), | |
1007 | create_texpr(identifier('__j'),integer,[],J), | |
1008 | create_texpr(domain(B),set(integer),[],Domain), | |
1009 | create_texpr(forall([I,J],Pre,IsDisjunct),pred,[],Forall), | |
1010 | create_texpr(member(I,D),pred,[],M1), | |
1011 | create_texpr(member(J,D),pred,[],M2), | |
1012 | create_texpr(less(I,J),pred,[],Less), | |
1013 | conjunct_predicates([M1,M2,Less],Pre), | |
1014 | create_texpr(function(B,I),set(ElemType),[],SetA), | |
1015 | create_texpr(function(B,J),set(ElemType),[],SetB), | |
1016 | create_texpr(intersection(SetA,SetB),set(ElemType),[],Intersection), | |
1017 | create_texpr(empty_set,set(ElemType),[],Empty), | |
1018 | create_texpr(equal(Intersection,Empty),pred,[],IsDisjunct). | |
1019 | ||
1020 | % maybe we could in some cases use the new partition operator from Event-B (if Ba is known?) ; or maybe provide better constraint propagation support | |
1021 | create_partition(Za,Zb,let_predicate([Seq],[Ba],Conjunct)) :- | |
1022 | ? | z_translate(Za,Ba), |
1023 | z_translate(Zb,Bb), | |
1024 | % print('Z Partition : '), translate:print_bexpr(Ba),nl, translate:print_bexpr(Bb),nl, | |
1025 | get_texpr_type(Ba,SeqType), | |
1026 | get_texpr_type(Bb,set(Type)), | |
1027 | create_texpr(identifier('__sets'),SeqType,[],Seq), | |
1028 | create_disjoint(Seq,Disjoint1), create_texpr(Disjoint1,pred,[],Disjoint), | |
1029 | create_texpr(general_union(Range),set(Type),[],Union), | |
1030 | create_texpr(range(Seq),set(Type),[],Range), | |
1031 | create_texpr(equal(Union,Bb),pred,[],Unification), | |
1032 | create_texpr(conjunct(Disjoint, Unification),pred,[],Conjunct). | |
1033 | % ,print('PARTITION: '), translate:print_bexpr(b(let_predicate([Seq],[Ba],Conjunct),pred,[])),nl. | |
1034 | ||
1035 | is_binary_op(OpName) :- z_binary_op(OpName,_). | |
1036 | is_unary_op(OpName) :- z_unary_operator(OpName,_). | |
1037 | ||
1038 | /* Boolean binary operators */ | |
1039 | z_binary_op(and, conjunct). | |
1040 | z_binary_op(or, disjunct). | |
1041 | z_binary_op(implies, implication). | |
1042 | z_binary_op(equiv, equivalence). | |
1043 | /* Generic equals */ | |
1044 | z_binary_op(equal, equal). | |
1045 | z_binary_op('\\neq', not_equal). | |
1046 | /* Set binary operators */ | |
1047 | z_binary_op(member, member). | |
1048 | z_binary_op('\\notin', not_member). | |
1049 | z_binary_op('\\cup', union). | |
1050 | z_binary_op('\\cap', intersection). | |
1051 | z_binary_op('\\subseteq', subset). | |
1052 | z_binary_op('\\subset', subset_strict). | |
1053 | z_binary_op('\\setminus', set_subtraction). | |
1054 | /* Arithmetic binary operators */ | |
1055 | z_binary_op('+', add). | |
1056 | z_binary_op('-', minus). | |
1057 | z_binary_op('*', multiplication). | |
1058 | z_binary_op('\\div', floored_div). % not div; B and Z semantics differ | |
1059 | z_binary_op('\\mod', modulo). | |
1060 | z_binary_op('\\upto', interval). | |
1061 | z_binary_op('<', less). | |
1062 | z_binary_op('\\leq', less_equal). | |
1063 | z_binary_op('\\geq', greater_equal). | |
1064 | z_binary_op('>', greater). | |
1065 | /* Relations and functions */ | |
1066 | z_binary_op('\\rel', relations). | |
1067 | z_binary_op('\\pfun', partial_function). | |
1068 | z_binary_op('\\fun', total_function). | |
1069 | z_binary_op('\\pinj', partial_injection). | |
1070 | z_binary_op('\\inj', total_injection). | |
1071 | z_binary_op('\\psurj', partial_surjection). | |
1072 | z_binary_op('\\surj', total_surjection). | |
1073 | z_binary_op('\\bij', total_bijection). | |
1074 | z_binary_op('\\ffun', partial_function). | |
1075 | z_binary_op('\\finj', partial_injection). | |
1076 | z_binary_op('\\mapsto', couple). | |
1077 | z_binary_op('\\comp', composition). | |
1078 | z_binary_op('\\dres', domain_restriction). | |
1079 | z_binary_op('\\ndres', domain_subtraction). | |
1080 | z_binary_op('\\rres', range_restriction). | |
1081 | z_binary_op('\\nrres', range_subtraction). | |
1082 | z_binary_op('_(|_|)', image). | |
1083 | z_binary_op('\\oplus', overwrite). | |
1084 | /* Sequences */ | |
1085 | z_binary_op('\\cat', concat). | |
1086 | ||
1087 | z_unary_operator('(-)', unary_minus). | |
1088 | z_unary_operator('\\dom', domain). | |
1089 | z_unary_operator('\\ran', range). | |
1090 | z_unary_operator(power, pow_subset). | |
1091 | z_unary_operator('\\power_1', pow1_subset). | |
1092 | /* In ProB all sets are treated as finite, so we use here the same as above */ | |
1093 | z_unary_operator('\\finset', fin_subset). | |
1094 | z_unary_operator('\\finset_1', fin1_subset). | |
1095 | z_unary_operator('\\bigcup', general_union). | |
1096 | z_unary_operator('\\bigcap', general_intersection). | |
1097 | z_unary_operator('\\dcat', general_concat). | |
1098 | ||
1099 | z_unary_operator(not, negation). | |
1100 | z_unary_operator('\\id', identity). | |
1101 | z_unary_operator('\\inv', reverse). | |
1102 | ||
1103 | z_unary_operator('\\plus', closure). | |
1104 | ||
1105 | z_unary_operator('\\#', card). | |
1106 | z_unary_operator('min', min). | |
1107 | z_unary_operator('max', max). | |
1108 | ||
1109 | z_unary_operator('\\seq', seq). | |
1110 | z_unary_operator('\\seq_1', seq1). | |
1111 | z_unary_operator('\\iseq', iseq). | |
1112 | z_unary_operator('rev', rev). | |
1113 | z_unary_operator('head', first). | |
1114 | z_unary_operator('last', last). | |
1115 | z_unary_operator('tail', tail). | |
1116 | z_unary_operator('front', front). | |
1117 | z_unary_operator('squash', compaction). | |
1118 | ||
1119 | z_unary_operator('first', first_of_pair). | |
1120 | z_unary_operator('second', second_of_pair). | |
1121 | ||
1122 | ||
1123 | translate_lets([],[],[]). | |
1124 | translate_lets([LetdefTi|ZRest],[Bid|IdRest],[BExpr|BRest]) :- | |
1125 | ti_expr(LetdefTi,letdef(ZName,ZExpr)), | |
1126 | ? | ti_type(ZExpr,ZType),internal2b(ZType,BType), |
1127 | z_translate_typed_identifier(ZName,BType,[],Bid), | |
1128 | ? | z_translate(ZExpr,BExpr), |
1129 | translate_lets(ZRest,IdRest,BRest). | |
1130 | ||
1131 | create_fields_for_binding([],[]). | |
1132 | create_fields_for_binding([BindingTi|ZRest], | |
1133 | [field(BField,BExpr)|BRest]) :- | |
1134 | ti_expr(BindingTi,bindfield(Name,ZExpr)), | |
1135 | z_translate_identifier(Name,BField), | |
1136 | z_translate(ZExpr,BExpr), | |
1137 | create_fields_for_binding(ZRest,BRest). | |
1138 | ||
1139 | :- public varlist_of_expanded_decls/3. % because Spider cannot deal with ~~mnf | |
1140 | varlist_of_expanded_decls([],[],[]). | |
1141 | varlist_of_expanded_decls([TDecl|Drest],Vars,Types) :- | |
1142 | ti_expr(TDecl,decl(Names,TypeDecl)), | |
1143 | ti_type(TypeDecl,set(ZType)), | |
1144 | ? | internal2b(ZType,BType), |
1145 | varlist_of_expanded_decl(Names,BType,LTypes), | |
1146 | append(Names,Vrest,Vars), | |
1147 | append(LTypes,Trest,Types), | |
1148 | varlist_of_expanded_decls(Drest,Vrest,Trest). | |
1149 | varlist_of_expanded_decl([],_,[]). | |
1150 | varlist_of_expanded_decl([_|Nrest],Type,[Type|Trest]) :- | |
1151 | varlist_of_expanded_decl(Nrest,Type,Trest). | |
1152 | ||
1153 | ||
1154 | ||
1155 | ||
1156 | ||
1157 | ||
1158 | ||
1159 | %******************************************************************************* | |
1160 | % register_given_sets/1: registers all given sets in the specification | |
1161 | % The specification must not include type information | |
1162 | ||
1163 | set_given_sets(Spec,In,Out) :- | |
1164 | findall(namedset(Name,Members),member(ti(namedset(Name,Members),_),Spec),NamedSets), | |
1165 | findall(Sets,member(ti(given(Sets),_),Spec),ListOfSetsTmp), | |
1166 | append(ListOfSetsTmp,ListOfSets), | |
1167 | get_given_sets(ListOfSets,ListOfDeferredSets), | |
1168 | get_named_sets(NamedSets,BNamedSets,BEnumeratedElems), | |
1169 | write_section(deferred_sets,ListOfDeferredSets,In,MDsets), | |
1170 | write_section(enumerated_sets,BNamedSets,MDsets,MEnums), | |
1171 | write_section(enumerated_elements,BEnumeratedElems,MEnums,Out). | |
1172 | ||
1173 | get_given_sets([],[]). | |
1174 | get_given_sets([Setname|Rest],[BSet|Brest]) :- | |
1175 | z_translate_identifier(Setname, Setid), | |
1176 | print_message(given_set(Setid)), | |
1177 | create_texpr(identifier(Setid),set(global(Setid)),[given_set],BSet), | |
1178 | get_given_sets(Rest,Brest). | |
1179 | get_named_sets([],[],[]). | |
1180 | get_named_sets([namedset(Setname,Members)|Rest],[BSet|BSetRest],Enumerated) :- | |
1181 | z_translate_identifier(Setname,Setid), | |
1182 | create_texpr(identifier(Setid),set(global(Setid)),[given_set],BSet), | |
1183 | z_translate_identifiers(Members,Memberids), | |
1184 | create_enum_elements(Memberids,global(Setid),LocalEnumerated), | |
1185 | append(LocalEnumerated,RestEnumerated,Enumerated), | |
1186 | get_named_sets(Rest,BSetRest,RestEnumerated). | |
1187 | create_enum_elements([],_,[]). | |
1188 | create_enum_elements([Id|IRest],Type,[TId|TRest]) :- | |
1189 | create_texpr(identifier(Id),Type,[enumerated_set_element],TId ), | |
1190 | create_enum_elements(IRest,Type,TRest). | |
1191 | ||
1192 | %******************************************************************************* | |
1193 | % register_freetypes/2: Registers the freetypes of the given specification. | |
1194 | % The specification must be given with type informations. | |
1195 | ||
1196 | set_freetypes(Spec,In,Out) :- | |
1197 | write_section(freetypes,Freetypes,In,Out), | |
1198 | ? | get_freetypes(Spec,Freetypes). |
1199 | get_freetypes([],[]). | |
1200 | get_freetypes([ExprTi|Rest],Freetypes) :- | |
1201 | ( ti_expr(ExprTi,data(Freetype,Arms)) -> | |
1202 | ? | get_freetype(Freetype,Arms,BFreetype), |
1203 | Freetypes = [BFreetype|FRest] | |
1204 | ; | |
1205 | Freetypes = FRest), | |
1206 | ? | get_freetypes(Rest,FRest). |
1207 | get_freetype(Freetype,ArmsTi,freetype(FreetypeId,Cases)) :- | |
1208 | ? | extract_cases_from_arms(ArmsTi,Cases), |
1209 | z_translate_identifier(Freetype,FreetypeId), | |
1210 | print_message(freetype(FreetypeId)). | |
1211 | extract_cases_from_arms([],[]). | |
1212 | extract_cases_from_arms([ArmTi|RestArms],[case(CaseId,Type)|RestCases]) :- | |
1213 | ti_expr(ArmTi,arm(Case,SwitchTi)), | |
1214 | z_translate_identifier(Case,CaseId), | |
1215 | ti_expr(SwitchTi,Switch), | |
1216 | ( Switch = just(ExprTi) -> | |
1217 | ? | ti_type(ExprTi,set(ZType)),internal2b(ZType,Type) |
1218 | ; | |
1219 | Type = constant([CaseId]) | |
1220 | ), | |
1221 | ? | extract_cases_from_arms(RestArms,RestCases). |
1222 | ||
1223 | %******************************************************************************* | |
1224 | % clean up the machine | |
1225 | clean_up_machine(Machine,Clean) :- | |
1226 | clean_up_sections([concrete_constants,properties, | |
1227 | abstract_variables,invariant, | |
1228 | promoted,initialisation,operation_bodies], | |
1229 | Machine,Clean). | |
1230 | clean_up_sections([],M,M). | |
1231 | clean_up_sections([Section|Rest],In,Out) :- | |
1232 | clean_up_section(Section,In,M), | |
1233 | clean_up_sections(Rest,M,Out). | |
1234 | clean_up_section(Section,In,Out) :- | |
1235 | select_section_texprs(Section,Old,New,In,Out), | |
1236 | clean_up_l_with_optimizations(Old,[],New,Section). | |
1237 | ||
1238 | %******************************************************************************* | |
1239 | % test the conversion of specifications | |
1240 | :- public startzconversiontests/0. | |
1241 | startzconversiontests :- | |
1242 | startzconversiontest('Z/Daniel/testcases.fuzz'). | |
1243 | ||
1244 | :- use_module(library(system),[environ/2]). | |
1245 | startzconversiontest(Testfile) :- | |
1246 | environ('PROB_EX_DIR',Dir), | |
1247 | atom_concat(Dir,'/',Dir2), | |
1248 | atom_concat(Dir2,Testfile,Fullpath), | |
1249 | testconversion(Fullpath). | |
1250 | ||
1251 | testconversion(File) :- | |
1252 | ( proz:load_and_simplify(File,Tests,Specification) -> true | |
1253 | ; add_error(proz,'Failed to load and simplify Z conversion test file: ',File)), | |
1254 | runtests(Tests,Specification,Errors), | |
1255 | (Errors = [] -> true ; add_errors(Errors), fail). | |
1256 | ||
1257 | add_errors([]). | |
1258 | add_errors([T|Rest]) :- | |
1259 | add_error(proz,'Z conversion testcase failed: ', T), | |
1260 | add_errors(Rest). | |
1261 | ||
1262 | load_and_simplify(File,Tests,Specification) :- | |
1263 | load_fuzzfile(File), | |
1264 | get_z_definitions(Z), | |
1265 | findtests(Z,Tests), | |
1266 | simplify_untyped(Z,Z2),!, | |
1267 | global_environment(Z2,_,Z3),!, | |
1268 | simplify_typed(Z3,Specification). | |
1269 | ||
1270 | findtests(Z,Tests) :- | |
1271 | findall(Name,getschema(Z,Name,_),Schemas), | |
1272 | findall(test(N,T),(member(T,Schemas),testmark(T,N),member(N,Schemas)),Tests). | |
1273 | ||
1274 | getschema(Z,Name,Def) :- member(sdef(shead(Name,[]),Def),Z). | |
1275 | getschema(Z,Name,Def) :- member(defeq(shead(Name,[]),Def),Z). | |
1276 | getschemat(Z,Name,Def) :- member(ti(sdef(shead(Name,[]),Def),_),Z). | |
1277 | getschemat(Z,Name,Def) :- member(ti(defeq(shead(Name,[]),Def),_),Z). | |
1278 | ||
1279 | testmark(Name,UName) :- append("Test",Rest,Complete),atom_codes(Name,Complete),atom_codes(UName,Rest). | |
1280 | ||
1281 | runtests([],_,[]). | |
1282 | runtests([test(N,T)|Rest],Z,Errors) :- | |
1283 | getschemat(Z,N,Def1), | |
1284 | getschemat(Z,T,Def2), | |
1285 | !, | |
1286 | write('Z transformation test '),write(N),write(': '), | |
1287 | ( equal_expressiont(Def1,Def2) -> | |
1288 | write(ok), | |
1289 | Errors = RestErrors | |
1290 | ; | |
1291 | write(failed), | |
1292 | Errors = [T|RestErrors]), | |
1293 | !, | |
1294 | nl, | |
1295 | runtests(Rest,Z,RestErrors). | |
1296 | ||
1297 | % -------------------------------- | |
1298 | ||
1299 |