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