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