1		% (c) 2009-2026 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		%write(z(ZExpr)),nl,translate:print_bexpr(BTExpr),nl, bsyntaxtree:check_ast(BTExpr),nl.
672
673		create_typed_bexpr(symbolic_comprehension_set(Ids, Lhs),BType,Res) :- !,
674		Res = b(comprehension_set(Ids, Lhs),BType,[prob_annotation('SYMBOLIC')]).
675		create_typed_bexpr(BExpr,BType,b(BExpr,BType,[])).
676
677		z_translate1(mu(Body,Computation), ZType, mu(BSet)) :-
678		!, ZSet = ti(comp(Body,Computation),set(ZType)),
679	?	z_translate(ZSet,BSet).
680		z_translate1(ZExpr,_ZType,BExpr) :-
681	?	z_translate2(ZExpr,BExpr).
682
683		z_translate2(falsity, falsity) :- !.
684		z_translate2(truth, truth) :- !.
685		z_translate2(forall(BodyTi, ZConsequent), forall(Ids, Lhs, Rhs)) :-
686	?	!, schema_to_typed_identifiers(BodyTi,Ids,Lhs),
687	?	z_translate(ZConsequent,Rhs).
688		z_translate2(exists(BodyTi, ZCondition), exists(Ids, BCondition)) :-
689	?	!, schema_to_typed_identifiers(BodyTi,Ids,Condition1),
690	?	z_translate(ZCondition,Rhs),
691		conjunct_predicates([Condition1,Rhs],BCondition).
692		z_translate2(lambda(BodyTi, ZExpr), lambda(Ids, Lhs, Rhs)) :-
693	?	!, schema_to_typed_identifiers(BodyTi,Ids,Lhs),
694	?	z_translate(ZExpr,Rhs).
695		z_translate2(ref(name('\\emptyset',''),[]),empty_set) :- !.
696		%z_translate2(ref(name('\\emptyset',''),[_TypeArg]),empty_set) :- !. % support constructs like \emptyset[\nat] ; currently argument removed in typing phase
697		z_translate2(ref(name('\\nat',''),[]),integer_set('NATURAL')) :- !.
698		z_translate2(ref(name('\\nat','_1'),[]),integer_set('NATURAL1')) :- !.
699		z_translate2(ref(name('\\num',''),[]),integer_set('INTEGER')) :- !.
700		/* In some special cases Schemas are refered just by ref(name(..)..), not by SEXPR(..) */
701		%z_translate2(ref(name(Name,Deco),Params), Env, BExpr) :-
702		% named_schema(Env,Name),!,
703		% z_translate(sexpr(sref(Name,Deco,Params,[])),BExpr).
704		%z_translate2(ref(FreetypeName,[]), Env, 'FreetypeSet'(Id)) :-
705		% zlookup(Env,data(FreetypeName,_)),
706		% !,z_translate_identifier(FreetypeName,Id).
707		z_translate2(ref(Name,[]), identifier(Id)) :-
708		!,z_translate_identifier(Name, Id).
709		z_translate2(inop(name('\\extract',''), Za, Zb), compaction(DomRes)) :-
710		!, create_texpr(domain_restriction(Ba,Bb),BType,[],DomRes),
711	?	z_translate(Za,Ba),z_translate(Zb,Bb),
712		get_texpr_type(Bb,BType).
713		z_translate2(inop(name('\\filter',''), Za, Zb), compaction(RanRes)) :-
714		!, create_texpr(range_restriction(Ba,Bb),BType,[],RanRes),
715	?	z_translate(Za,Ba),z_translate(Zb,Bb),
716		get_texpr_type(Ba,BType).
717		z_translate2(apply(Iteration,ZRel), Result) :-
718		% iteration of relations. The problem of this operator is that
719		% it can have negative arguments in Z but not in B
720		ti_expr(Iteration, apply(Ref,ZN)),
721		ti_expr(Ref, ref(name(iter,''),[])),
722	?	!, z_translate(ZN,BN), z_translate(ZRel,BRel),
723		get_texpr_type(BRel,BRelType),
724		create_texpr(reverse(BRel),BRelType,[],Inverse),
725		( is_a_number(ZN,Value), Value >= 0 ->
726		% R^x, where x is a non-negative number, we can use it directly
727		Result = iteration(BRel,BN)
728		; is_a_negative_number(ZN,Value), Value >= 0 ->
729		% R^-x, where x is a non-negative number, we can rewrite it into (R~)^x
730		create_texpr(integer(Value),integer,[],Negation),
731		Result = iteration(Inverse,Negation)
732		;
733		% R^x, where x is an arbitrary expression, we surround it by if-then-else
734		% to negate the x if necessary
735		create_texpr(integer(0),integer,[],Zero),
736		create_texpr(less_equal(Zero,BN),pred,[],NonNegative),
737		create_texpr(iteration(BRel,BN),BRelType,[],Then),
738		create_texpr(unary_minus(BN),integer,[],Negation),
739		create_texpr(iteration(Inverse,Negation),BRelType,[],Else),
740		Result = if_then_else(NonNegative,Then,Else)).
741		z_translate2(inop(ZopName, Za, Zb), BBinOp) :-
742		z_translate_identifier(ZopName,Zop),
743		is_binary_op(Zop),!,
744	?	z_translate_binary_op(Zop,Za,Zb,BBinOp).
745		z_translate2(inrel(ZopName, Za, Zb), BBinOp) :-
746		z_translate_identifier(ZopName,Zop),
747		is_binary_op(Zop),!,
748	?	z_translate_binary_op(Zop,Za,Zb,BBinOp).
749		z_translate2(ingen(ZopName, Za, Zb), BBinOp) :-
750		z_translate_identifier(ZopName,Zop),
751		is_binary_op(Zop),!,
752	?	z_translate_binary_op(Zop,Za,Zb,BBinOp).
753		z_translate2(number(Value), integer(Value)) :- !.
754		z_translate2(ext(ZEntities), set_extension(BEntities)) :-
755	?	!, z_translate(ZEntities, BEntities).
756		z_translate2(seq(ZEntities), sequence_extension(BEntities)) :-
757	?	!, z_translate(ZEntities, BEntities).
758		z_translate2(apply(Items,ZExpr), bag_items(BExpr)) :-
759		ti_expr(Items,ref(name('items',''),[])),!,
760	?	z_translate(ZExpr,BExpr).
761		z_translate2(apply(ZFun, Zarg), BExpr) :-
762		ti_expr(ZFun,ref(Name,[])),
763		z_translate_identifier(Name,Op),
764		is_unary_op(Op),!,
765	?	z_translate_unary_op(Op,Zarg,BExpr).
766		z_translate2(apply(ZFun, ZArg), function(BFun,BArg)) :-
767	?	!, z_translate(ZFun,BFun), z_translate(ZArg,BArg).
768		z_translate2(postop(Name, Zarg), BExpr) :-
769		z_translate_identifier(Name,Op),
770		is_unary_op(Op),!,
771	?	z_translate_unary_op(Op,Zarg,BExpr).
772		z_translate2(prerel(Name, Zarg), BExpr) :-
773		z_translate_identifier(Name,Op),
774		is_unary_op(Op),!,
775		z_translate_unary_op(Op,Zarg,BExpr).
776		z_translate2(pregen(Name, Zarg), BExpr) :-
777		z_translate_identifier(Name,Op),
778		is_unary_op(Op),!,
779	?	z_translate_unary_op(Op,Zarg,BExpr).
780		z_translate2(inrel(name('\\prefix',''), Za, Zb), BExpr) :-
781	?	!,z_translate(Za,Ba),z_translate(Zb,Bb),
782		get_texpr_type(Ba,SeqType),
783		create_texpr(size(Ba),integer,[],SizeA),
784		create_texpr(size(Bb),integer,[],SizeB),
785		create_texpr(greater_equal(SizeB,SizeA),pred,[],GreaterEqual),
786		create_texpr(restrict_front(Bb,SizeA),SeqType,[],Prefix),
787		create_texpr(equal(Ba,Prefix),pred,[],Equal),
788		conjunct_predicates([GreaterEqual,Equal],TypedBExpr),
789		get_texpr_expr(TypedBExpr,BExpr).
790		z_translate2(inrel(name('\\suffix',''), Za, Zb), BExpr) :-
791	?	!,z_translate(Za,Ba),z_translate(Zb,Bb),
792		get_texpr_type(Ba,SeqType),
793		create_texpr(size(Ba),integer,[],SizeA),
794		create_texpr(size(Bb),integer,[],SizeB),
795		create_texpr(greater_equal(SizeB,SizeA),pred,[],GreaterEqual),
796		create_texpr(minus(SizeB,SizeA),integer,[],Diff),
797		create_texpr(restrict_tail(Bb,Diff),SeqType,[],Suffix),
798		create_texpr(equal(Ba,Suffix),pred,[],Equal),
799		conjunct_predicates([GreaterEqual,Equal],TypedBExpr),
800		get_texpr_expr(TypedBExpr,BExpr).
801		z_translate2(inrel(name('\\inseq',''), Za, Zb), BExpr) :-
802	?	!, create_in_sequence(Za,Zb,BExpr).
803		z_translate2(prerel(name('\\disjoint',''), Z), BExpr) :-
804	?	!, z_translate(Z,B), create_disjoint(B,BExpr).
805		z_translate2(inrel(name('\\partition',''), Za, Zb), partition(BSet,BSeq)) :-
806		ti_expr(Za,seq(ZSeq)),!,
807		z_translate(Zb,BSet),
808		z_translate(ZSeq,BSeq).
809		z_translate2(inrel(name('\\partition',''), Za, Zb), BExpr) :-
810	?	!, create_partition(Za,Zb,BExpr).
811		z_translate2(select(ZRecord, ZField), record_field(BRecord, FieldIdentifier)) :-
812	?	!, z_translate(ZRecord, BRecord),
813		z_translate_identifier(ZField, FieldIdentifier).
814		/* Comprehension set without expression */
815		z_translate2(comp(Body, Nothing),Res) :-
816		!,
817		( ti_expr(Nothing,nothing) -> true
818		;
819		add_error(proz,'Encountered comprehension set with expression in translation. Should have been replaced.'),
820		fail),
821		ti_expr(Body,body(Decls,ZWheres)),
822	?	varlist_of_expanded_decls(Decls, Vars, Types),
823		z_translate_typed_identifiers(Vars,Types,[],Ids),
824	?	z_translate(ZWheres,Wheres),
825		conjunct_predicates(Wheres,Lhs),
826		%print(comp(Ids,Lhs)),nl,
827		(is_symbolic_set_comprehension(Ids,Lhs)
828		-> Res = symbolic_comprehension_set(Ids, Lhs) %,print(symbolic(Ids)),nl
829		; Res = comprehension_set(Ids, Lhs)).
830		z_translate2(cross([Za,Zb]), cartesian_product(Ba,Bb)) :-
831	?	!, z_translate(Za,Ba), z_translate(Zb,Bb).
832		z_translate2(cross([ZExpr|ZRest]), cartesian_product(BExpr,TBRest)) :-
833		!, z_translate(ZExpr,BExpr), z_translate2(cross(ZRest),BRest),
834		BRest=cartesian_product(BL,BR),get_texpr_type(BL,set(LType)),get_texpr_type(BR,set(RType)),
835		create_texpr(BRest,set(couple(LType,RType)),[],TBRest).
836		z_translate2(tuple([Za,Zb]), couple(Ba,Bb)) :-
837	?	!, z_translate(Za,Ba), z_translate(Zb,Bb).
838		z_translate2(tuple([ZExpr|ZRest]), couple(BExpr,TBRest)) :-
839		!, z_translate(ZExpr,BExpr), z_translate2(tuple(ZRest),BRest),
840		BRest=couple(BL,BR),get_texpr_type(BL,LType),get_texpr_type(BR,RType),
841		create_texpr(BRest,couple(LType,RType),[],TBRest).
842		z_translate2(letexpr(ZLets,ZExpr), Result) :- %let_expression(Bids,BAssignments,BExpr)) :-
843	?	!, translate_lets(ZLets,Bids,BAssignments),
844		z_translate(ZExpr,BExpr),
845		create_z_let(expr,Bids,BAssignments,BExpr,[],b(Result,_,_)).
846		z_translate2(letpred(ZLets,ZExpr), Result) :- %let_predicate(Bids,BAssignments,BExpr)) :-
847	?	!, translate_lets(ZLets,Bids,BAssignments),
848	?	z_translate(ZExpr,BExpr),
849	?	create_z_let(pred,Bids,BAssignments,BExpr,[],b(Result,_,_)).
850		z_translate2(if(ZPred,ZIf,ZElse), if_then_else(BPred,BIf,BElse)) :-
851	?	!, z_translate(ZPred,BPred),
852	?	z_translate(ZIf,BIf), z_translate(ZElse,BElse).
853		z_translate2(inrel(Name,Za,Zb), member(Couple,Relation)) :-
854		!,z_translate(Za,Ba),z_translate(Zb,Bb),
855		z_translate_identifier(Name,Id),
856		get_texpr_type(Ba,TypeA), get_texpr_type(Bb,TypeB),
857		create_texpr(couple(Ba,Bb),couple(TypeA,TypeB),[],Couple),
858		create_texpr(identifier(Id),set(couple(TypeA,TypeB)),[],Relation).
859
860		% Internal constructs
861		z_translate2(binding(Bindings), rec(Fields)) :-
862		!, create_fields_for_binding(Bindings,Fields).
863		z_translate2(ftconstant(Freetype,Case),value(freeval(FreetypeId,ConstId,term(ConstId)))) :-
864		!,z_translate_identifier(Freetype,FreetypeId),
865		z_translate_identifier(Case,ConstId).
866		z_translate2(ftconstructor(Freetype,Case,ZExpr),
867		freetype_constructor(FreetypeId,CaseId,BExpr)) :-
868	?	!,z_translate(ZExpr,BExpr),
869		z_translate_identifier(Freetype,FreetypeId),
870		z_translate_identifier(Case,CaseId).
871		z_translate2(ftdestructor(Freetype,Case,ZExpr),
872		freetype_destructor(FreetypeId,CaseId,BExpr)) :-
873	?	!,z_translate(ZExpr,BExpr),
874		z_translate_identifier(Freetype,FreetypeId),
875		z_translate_identifier(Case,CaseId).
876		z_translate2(ftcase(Freetype,Case,ZExpr),
877		freetype_case(FreetypeId,CaseId,BExpr)) :-
878	?	!,z_translate(ZExpr,BExpr),
879		z_translate_identifier(Freetype,FreetypeId),
880		z_translate_identifier(Case,CaseId).
881
882		z_translate2(basetype(set(Type)), Expr) :-
883	?	!,translate_basetype2(Type,Expr).
884
885		z_translate2(reclet(ZId,ZSet), recursive_let(BId,BSet) ) :-
886		!,z_translate(ZId,BId),
887		% TODO: recursive_let accepts only comprehension sets as argument,
888		% maybe this should be checked here (lambda should be ok, too, because
889		% it's converted to a comprehension set
890	?	z_translate(ZSet,BSet1),
891		add_texpr_infos(BSet1,[prob_annotation('SYMBOLIC')],BSet).
892
893		z_translate2(ZBinOp, BBinOp) :-
894		functor(ZBinOp,ZopName,2),
895		is_binary_op(ZopName),!,
896		arg(1,ZBinOp,Za), arg(2,ZBinOp,Zb),
897	?	z_translate_binary_op(ZopName,Za,Zb,BBinOp).
898		z_translate2(ZUnOp, BUnOp) :-
899		functor(ZUnOp,ZopName,1),
900		is_unary_op(ZopName),!,
901		arg(1,ZUnOp,Zarg),
902	?	z_translate_unary_op(ZopName,Zarg,BUnOp).
903
904		z_translate2(ZExpr,_) :-
905		add_error(proz,'Unmatched Z expression',ZExpr),
906		fail.
907
908		% added by Leuschel to mark certain set comprehensions as symbolic
909		% TO DO: look with Daniel Plagge whether rec__ should always be symbolic, and whether other sets should be put symbolic
910		is_symbolic_set_comprehension([TID],_) :-
911		get_texpr_id(TID,ID),
912		atom_codes(ID,C),
913		append("rec__",_,C). % rec__ are special variables introduced in ztransformations:removesexpr2 for Schema fields
914
915		is_a_negative_number(ZExpr,N) :-
916		ti_expr(ZExpr,apply(Ref,Num)),
917		ti_expr(Ref,ref(name('(-)',''),[])),
918		is_a_number(Num,N).
919		is_a_number(ZExpr,N) :-
920		ti_expr(ZExpr,number(N)).
921
922		z_translate_binary_op(ZopName,Za,Zb,Bop) :-
923		z_binary_op(ZopName,BopName),!,
924	?	z_translate(Za,Ba),z_translate(Zb,Bb),
925		Bop =.. [BopName,Ba,Bb].
926
927		z_translate_unary_op(ZopName,Zarg,Bop) :-
928		z_unary_operator(ZopName, BopName),!,
929	?	z_translate(Zarg, Barg),
930		Bop =.. [BopName, Barg].
931
932		translate_basetype(Type,TExpr) :-
933		create_texpr(BExpr,set(BType),[],TExpr),
934	?	internal2b(Type,BType),
935	?	translate_basetype2(Type,BExpr).
936
937		translate_basetype2(num,integer_set('INTEGER')).
938		translate_basetype2(given(Name), value(global_set(Id))) :- z_translate_identifier(Name,Id).
939		translate_basetype2(freetype(Name), freetype_set(Id)) :- z_translate_identifier(Name,Id).
940	?	translate_basetype2(set(T), pow_subset(B)) :- translate_basetype(T,B).
941		translate_basetype2(tuple([A,B]), cartesian_product(TA,TB)) :-
942	?	!,translate_basetype(A,TA),
943	?	translate_basetype(B,TB).
944		translate_basetype2(tuple([A,B,C|Rest]), cartesian_product(TA,TBRest)) :-
945		translate_basetype(A,TA),
946		translate_basetype(tuple([B,C|Rest]),BRest),
947		BRest = cartesian_product(BL,BR),
948		get_texpr_type(BL,set(LType)),get_texpr_type(BR,set(RType)),
949		create_texpr(BRest,set(couple(LType,RType)),[],TBRest).
950		translate_basetype2(schema(ZFields),struct(Rec)) :-
951		translate_bt_fields(ZFields,BFields,FieldTypes),
952		create_texpr(rec(BFields),record(FieldTypes),[],Rec).
953		translate_bt_fields([],[],[]).
954		translate_bt_fields([ZField|ZRest],[BField|BRest],[FieldType|TRest]) :-
955		translate_bt_field(ZField,BField,FieldType),
956		translate_bt_fields(ZRest,BRest,TRest).
957		translate_bt_field(field(Name,T),field(FieldId,B),field(FieldId,set(BType))) :-
958		internal2b(T,BType),
959		z_translate_identifier(Name,FieldId),
960		translate_basetype(T,B).
961
962		schema_to_typed_identifiers(BodyTi,Ids,Condition) :-
963		ti_type(BodyTi,set(schema(ZFields))),
964	?	zfields2b(ZFields,Vars,Types),
965		z_translate_typed_identifiers(Vars,Types,[],Ids),
966
967		ti_expr(BodyTi,body(_,WhereTi)),
968	?	z_translate(WhereTi,Wheres),
969		conjunct_predicates(Wheres,Condition).
970
971		create_in_sequence(Za,Zb,BExpr) :-
972	?	z_translate(Za,Ba),z_translate(Zb,Bb),
973		get_texpr_type(Ba,BSeqType), BSeqType = set(couple(integer,BElemType)),
974		ti_type(Za,ZSeqType), ZSeqType = set(tuple([num,ZElemType])),
975		translate_basetype(ZElemType,BaseSet),
976		create_texpr(identifier('__card'),integer,[],C),
977		create_texpr(identifier('__i'),integer,[],I),
978		create_texpr(identifier('__la'),BSeqType,[],La),
979		create_texpr(identifier('__lb'),BSeqType,[],Lb),
980		create_texpr(identifier('__offset'),integer,[],Offset),
981		create_texpr(let_predicate([La,Lb],[Ba,Bb],Conjunction),pred,[],TypedBExpr),
982		create_texpr(seq(BaseSet),set(BSeqType),[],Sequences),
983		create_texpr(member(La,Sequences),pred,[],Asequence),
984		create_texpr(member(Lb,Sequences),pred,[],Bsequence),
985		create_texpr(card(La),integer,[],CardA),
986		create_texpr(card(Lb),integer,[],CardB),
987		create_texpr(minus(CardB,CardA),integer,[],Diff),
988		create_texpr(let_predicate([C],[Diff],Exists),pred,[],Let),
989		create_texpr(integer(0),integer,[],Zero),
990		create_texpr(interval(Zero,Diff),integer,[],Interval),
991		create_texpr(member(Offset,Interval),pred,[],InInterval),
992		create_texpr(conjunct(InInterval,Forall),pred,[],Pred),
993		create_texpr(forall([I],InDomain,Equal),pred,[],Forall),
994		create_texpr(domain(Ba),integer,[],Domain),
995		create_texpr(member(I,Domain),pred,[],InDomain),
996		create_texpr(equal(ElemA,ElemB),pred,[],Equal),
997		create_texpr(function(Ba,I),BElemType,[],ElemA),
998		create_texpr(add(I,Offset),integer,[],I2),
999		create_texpr(function(Bb,I2),BElemType,[],ElemB),
1000		create_exists([Offset],Pred,Exists),
1001		conjunct_predicates([Asequence,Bsequence,Let],Conjunction),
1002		get_texpr_expr(TypedBExpr,BExpr).
1003
1004		create_disjoint(B, let_predicate([D],[Domain],Forall)) :-
1005		get_texpr_type(B,set(couple(integer,set(ElemType)))),
1006		create_texpr(identifier('__d'),set(integer),[],D),
1007		create_texpr(identifier('__i'),integer,[],I),
1008		create_texpr(identifier('__j'),integer,[],J),
1009		create_texpr(domain(B),set(integer),[],Domain),
1010		create_texpr(forall([I,J],Pre,IsDisjunct),pred,[],Forall),
1011		create_texpr(member(I,D),pred,[],M1),
1012		create_texpr(member(J,D),pred,[],M2),
1013		create_texpr(less(I,J),pred,[],Less),
1014		conjunct_predicates([M1,M2,Less],Pre),
1015		create_texpr(function(B,I),set(ElemType),[],SetA),
1016		create_texpr(function(B,J),set(ElemType),[],SetB),
1017		create_texpr(intersection(SetA,SetB),set(ElemType),[],Intersection),
1018		create_texpr(empty_set,set(ElemType),[],Empty),
1019		create_texpr(equal(Intersection,Empty),pred,[],IsDisjunct).
1020
1021		% 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
1022		create_partition(Za,Zb,let_predicate([Seq],[Ba],Conjunct)) :-
1023	?	z_translate(Za,Ba),
1024		z_translate(Zb,Bb),
1025		% print('Z Partition : '), translate:print_bexpr(Ba),nl, translate:print_bexpr(Bb),nl,
1026		get_texpr_type(Ba,SeqType),
1027		get_texpr_type(Bb,set(Type)),
1028		create_texpr(identifier('__sets'),SeqType,[],Seq),
1029		create_disjoint(Seq,Disjoint1), create_texpr(Disjoint1,pred,[],Disjoint),
1030		create_texpr(general_union(Range),set(Type),[],Union),
1031		create_texpr(range(Seq),set(set(Type)),[],Range),
1032		create_texpr(equal(Union,Bb),pred,[],Unification),
1033		create_texpr(conjunct(Disjoint, Unification),pred,[],Conjunct).
1034		% ,print('PARTITION: '), translate:print_bexpr(b(let_predicate([Seq],[Ba],Conjunct),pred,[])),nl.
1035
1036		is_binary_op(OpName) :- z_binary_op(OpName,_).
1037		is_unary_op(OpName) :- z_unary_operator(OpName,_).
1038
1039		/* Boolean binary operators */
1040		z_binary_op(and, conjunct).
1041		z_binary_op(or, disjunct).
1042		z_binary_op(implies, implication).
1043		z_binary_op(equiv, equivalence).
1044		/* Generic equals */
1045		z_binary_op(equal, equal).
1046		z_binary_op('\\neq', not_equal).
1047		/* Set binary operators */
1048		z_binary_op(member, member).
1049		z_binary_op('\\notin', not_member).
1050		z_binary_op('\\cup', union).
1051		z_binary_op('\\cap', intersection).
1052		z_binary_op('\\subseteq', subset).
1053		z_binary_op('\\subset', subset_strict).
1054		z_binary_op('\\setminus', set_subtraction).
1055		/* Arithmetic binary operators */
1056		z_binary_op('+', add).
1057		z_binary_op('-', minus).
1058		z_binary_op('*', multiplication).
1059		z_binary_op('\\div', floored_div). % not div; B and Z semantics differ
1060		z_binary_op('\\mod', modulo).
1061		z_binary_op('\\upto', interval).
1062		z_binary_op('<', less).
1063		z_binary_op('\\leq', less_equal).
1064		z_binary_op('\\geq', greater_equal).
1065		z_binary_op('>', greater).
1066		/* Relations and functions */
1067		z_binary_op('\\rel', relations).
1068		z_binary_op('\\pfun', partial_function).
1069		z_binary_op('\\fun', total_function).
1070		z_binary_op('\\pinj', partial_injection).
1071		z_binary_op('\\inj', total_injection).
1072		z_binary_op('\\psurj', partial_surjection).
1073		z_binary_op('\\surj', total_surjection).
1074		z_binary_op('\\bij', total_bijection).
1075		z_binary_op('\\ffun', partial_function).
1076		z_binary_op('\\finj', partial_injection).
1077		z_binary_op('\\mapsto', couple).
1078		z_binary_op('\\comp', composition).
1079		z_binary_op('\\dres', domain_restriction).
1080		z_binary_op('\\ndres', domain_subtraction).
1081		z_binary_op('\\rres', range_restriction).
1082		z_binary_op('\\nrres', range_subtraction).
1083		z_binary_op('_(|_|)', image).
1084		z_binary_op('\\oplus', overwrite).
1085		/* Sequences */
1086		z_binary_op('\\cat', concat).
1087
1088		z_unary_operator('(-)', unary_minus).
1089		z_unary_operator('\\dom', domain).
1090		z_unary_operator('\\ran', range).
1091		z_unary_operator(power, pow_subset).
1092		z_unary_operator('\\power_1', pow1_subset).
1093		/* In ProB all sets are treated as finite, so we use here the same as above */
1094		z_unary_operator('\\finset', fin_subset).
1095		z_unary_operator('\\finset_1', fin1_subset).
1096		z_unary_operator('\\bigcup', general_union).
1097		z_unary_operator('\\bigcap', general_intersection).
1098		z_unary_operator('\\dcat', general_concat).
1099
1100		z_unary_operator(not, negation).
1101		z_unary_operator('\\id', identity).
1102		z_unary_operator('\\inv', reverse).
1103
1104		z_unary_operator('\\plus', closure).
1105
1106		z_unary_operator('\\#', card).
1107		z_unary_operator('min', min).
1108		z_unary_operator('max', max).
1109
1110		z_unary_operator('\\seq', seq).
1111		z_unary_operator('\\seq_1', seq1).
1112		z_unary_operator('\\iseq', iseq).
1113		z_unary_operator('rev', rev).
1114		z_unary_operator('head', first).
1115		z_unary_operator('last', last).
1116		z_unary_operator('tail', tail).
1117		z_unary_operator('front', front).
1118		z_unary_operator('squash', compaction).
1119
1120		z_unary_operator('first', first_of_pair).
1121		z_unary_operator('second', second_of_pair).
1122
1123
1124		translate_lets([],[],[]).
1125		translate_lets([LetdefTi|ZRest],[Bid|IdRest],[BExpr|BRest]) :-
1126		ti_expr(LetdefTi,letdef(ZName,ZExpr)),
1127	?	ti_type(ZExpr,ZType),internal2b(ZType,BType),
1128		z_translate_typed_identifier(ZName,BType,[],Bid),
1129	?	z_translate(ZExpr,BExpr),
1130		translate_lets(ZRest,IdRest,BRest).
1131
1132		create_fields_for_binding([],[]).
1133		create_fields_for_binding([BindingTi|ZRest],
1134		[field(BField,BExpr)|BRest]) :-
1135		ti_expr(BindingTi,bindfield(Name,ZExpr)),
1136		z_translate_identifier(Name,BField),
1137		z_translate(ZExpr,BExpr),
1138		create_fields_for_binding(ZRest,BRest).
1139
1140		:- public varlist_of_expanded_decls/3. % because Spider cannot deal with ~~mnf
1141		varlist_of_expanded_decls([],[],[]).
1142		varlist_of_expanded_decls([TDecl|Drest],Vars,Types) :-
1143		ti_expr(TDecl,decl(Names,TypeDecl)),
1144		ti_type(TypeDecl,set(ZType)),
1145	?	internal2b(ZType,BType),
1146		varlist_of_expanded_decl(Names,BType,LTypes),
1147		append(Names,Vrest,Vars),
1148		append(LTypes,Trest,Types),
1149		varlist_of_expanded_decls(Drest,Vrest,Trest).
1150		varlist_of_expanded_decl([],_,[]).
1151		varlist_of_expanded_decl([_|Nrest],Type,[Type|Trest]) :-
1152		varlist_of_expanded_decl(Nrest,Type,Trest).
1153
1154
1155
1156
1157
1158
1159
1160		%*******************************************************************************
1161		% register_given_sets/1: registers all given sets in the specification
1162		% The specification must not include type information
1163
1164		set_given_sets(Spec,In,Out) :-
1165		findall(namedset(Name,Members),member(ti(namedset(Name,Members),_),Spec),NamedSets),
1166		findall(Sets,member(ti(given(Sets),_),Spec),ListOfSetsTmp),
1167		append(ListOfSetsTmp,ListOfSets),
1168		get_given_sets(ListOfSets,ListOfDeferredSets),
1169		get_named_sets(NamedSets,BNamedSets,BEnumeratedElems),
1170		write_section(deferred_sets,ListOfDeferredSets,In,MDsets),
1171		write_section(enumerated_sets,BNamedSets,MDsets,MEnums),
1172		write_section(enumerated_elements,BEnumeratedElems,MEnums,Out).
1173
1174		get_given_sets([],[]).
1175		get_given_sets([Setname|Rest],[BSet|Brest]) :-
1176		z_translate_identifier(Setname, Setid),
1177		debug_println(19,given_set(Setid)),
1178		create_texpr(identifier(Setid),set(global(Setid)),[given_set],BSet),
1179		get_given_sets(Rest,Brest).
1180		get_named_sets([],[],[]).
1181		get_named_sets([namedset(Setname,Members)|Rest],[BSet|BSetRest],Enumerated) :-
1182		z_translate_identifier(Setname,Setid),
1183		create_texpr(identifier(Setid),set(global(Setid)),[given_set],BSet),
1184		z_translate_identifiers(Members,Memberids),
1185		create_enum_elements(Memberids,global(Setid),LocalEnumerated),
1186		append(LocalEnumerated,RestEnumerated,Enumerated),
1187		get_named_sets(Rest,BSetRest,RestEnumerated).
1188		create_enum_elements([],_,[]).
1189		create_enum_elements([Id|IRest],Type,[TId|TRest]) :-
1190		create_texpr(identifier(Id),Type,[enumerated_set_element],TId ),
1191		create_enum_elements(IRest,Type,TRest).
1192
1193		%*******************************************************************************
1194		% register_freetypes/2: Registers the freetypes of the given specification.
1195		% The specification must be given with type informations.
1196
1197		set_freetypes(Spec,In,Out) :-
1198		write_section(freetypes,Freetypes,In,Out),
1199	?	get_freetypes(Spec,Freetypes).
1200		get_freetypes([],[]).
1201		get_freetypes([ExprTi|Rest],Freetypes) :-
1202		( ti_expr(ExprTi,data(Freetype,Arms)) ->
1203	?	get_freetype(Freetype,Arms,BFreetype),
1204		Freetypes = [BFreetype|FRest]
1205		;
1206		Freetypes = FRest),
1207	?	get_freetypes(Rest,FRest).
1208		get_freetype(Freetype,ArmsTi,freetype(FreetypeId,Cases)) :-
1209	?	extract_cases_from_arms(ArmsTi,Cases),
1210		z_translate_identifier(Freetype,FreetypeId),
1211		debug_println(19,freetype(FreetypeId)).
1212		extract_cases_from_arms([],[]).
1213		extract_cases_from_arms([ArmTi|RestArms],[case(CaseId,Type)|RestCases]) :-
1214		ti_expr(ArmTi,arm(Case,SwitchTi)),
1215		z_translate_identifier(Case,CaseId),
1216		ti_expr(SwitchTi,Switch),
1217		( Switch = just(ExprTi) ->
1218	?	ti_type(ExprTi,set(ZType)),internal2b(ZType,Type)
1219		;
1220		Type = constant([CaseId])
1221		),
1222	?	extract_cases_from_arms(RestArms,RestCases).
1223
1224		%*******************************************************************************
1225		% clean up the machine
1226		clean_up_machine(Machine,Clean) :-
1227		clean_up_sections([concrete_constants,properties,
1228		abstract_variables,invariant,
1229		promoted,initialisation,operation_bodies],
1230		Machine,Clean).
1231		clean_up_sections([],M,M).
1232		clean_up_sections([Section|Rest],In,Out) :-
1233		clean_up_section(Section,In,M),
1234		clean_up_sections(Rest,M,Out).
1235		clean_up_section(Section,In,Out) :-
1236		select_section_texprs(Section,Old,New,In,Out),
1237		clean_up_l_with_optimizations(Old,[],New,Section).
1238
1239		%*******************************************************************************
1240		% test the conversion of specifications
1241		:- public startzconversiontests/0.
1242		startzconversiontests :-
1243		startzconversiontest('Z/Daniel/testcases.fuzz').
1244
1245		:- use_module(library(system),[environ/2]).
1246		startzconversiontest(Testfile) :-
1247		environ('PROB_EX_DIR',Dir),
1248		atom_concat(Dir,'/',Dir2),
1249		atom_concat(Dir2,Testfile,Fullpath),
1250		testconversion(Fullpath).
1251
1252		testconversion(File) :-
1253		( proz:load_and_simplify(File,Tests,Specification) -> true
1254		; add_error(proz,'Failed to load and simplify Z conversion test file: ',File)),
1255		runtests(Tests,Specification,Errors),
1256		(Errors = [] -> true ; add_errors(Errors), fail).
1257
1258		add_errors([]).
1259		add_errors([T|Rest]) :-
1260		add_error(proz,'Z conversion testcase failed: ', T),
1261		add_errors(Rest).
1262
1263		load_and_simplify(File,Tests,Specification) :-
1264		load_fuzzfile(File),
1265		get_z_definitions(Z),
1266		findtests(Z,Tests),
1267		simplify_untyped(Z,Z2),!,
1268		global_environment(Z2,_,Z3),!,
1269		simplify_typed(Z3,Specification).
1270
1271		findtests(Z,Tests) :-
1272		findall(Name,getschema(Z,Name,_),Schemas),
1273		findall(test(N,T),(member(T,Schemas),testmark(T,N),member(N,Schemas)),Tests).
1274
1275		getschema(Z,Name,Def) :- member(sdef(shead(Name,[]),Def),Z).
1276		getschema(Z,Name,Def) :- member(defeq(shead(Name,[]),Def),Z).
1277		getschemat(Z,Name,Def) :- member(ti(sdef(shead(Name,[]),Def),_),Z).
1278		getschemat(Z,Name,Def) :- member(ti(defeq(shead(Name,[]),Def),_),Z).
1279
1280		testmark(Name,UName) :- append("Test",Rest,Complete),atom_codes(Name,Complete),atom_codes(UName,Rest).
1281
1282		runtests([],_,[]).
1283		runtests([test(N,T)|Rest],Z,Errors) :-
1284		getschemat(Z,N,Def1),
1285		getschemat(Z,T,Def2),
1286		!,
1287		write('Z transformation test '),write(N),write(': '),
1288		( equal_expressiont(Def1,Def2) ->
1289		write(ok),
1290		Errors = RestErrors
1291		;
1292		write(failed),
1293		Errors = [T|RestErrors]),
1294		!,
1295		nl,
1296		runtests(Rest,Z,RestErrors).
1297
1298		% --------------------------------
1299
1300