1		% (c) 2014-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(enabling_predicates, [compute_enabling_predicate/5]).
6
7		/* Modules and Infos for the code coverage analysis */
8		:- use_module(probsrc(module_information)).
9		:- module_info(group,model_checker).
10		:- module_info(description,'This module provides predicates computing weakest preconditions without taking the preconditions of the substitutions into account').
11
12		% Standard SICSTUS prolog libraries
13		:- use_module(library(lists)).
14
15		% Classical B prolog modules
16		:- use_module(probsrc(bmachine),[b_get_machine_operation/4, b_get_invariant_from_machine/1]).
17		:- use_module(probsrc(bsyntaxtree),[conjunct_predicates/2, conjunction_to_list/2,
18		get_texpr_expr/2, create_texpr/4, %remove_all_infos/2,
19		create_exists/3, safe_create_texpr/3,
20		get_texpr_ids/2, some_id_occurs_in_expr/2]).
21		:- use_module(probsrc(bmachine_eventb), [prime_variables/2]).
22
23		% Predicates for calculating the weakest-precondition
24		:- use_module(probsrc(weakest_preconditions), [weakest_precondition/3]).
25
26		% POR modules
27		:- use_module(probporsrc(b_simplifier),[simplify_b_predicate/2]).
28
29		% Other ProB modules
30		:- use_module(probsrc(preferences),[get_preference/2]).
31		:- use_module(probsrc(translate),[translate_bexpression/2, translate_substitution/2]).
32		:- use_module(probsrc(debug), [debug_mode/1]).
33		:- use_module(probsrc(error_manager),[add_error/3]).
34
35
36		%enumeration_warning(enumerating(n),'INTEGER',1:sup,1:3,critical)
37		% TODO: After computing the weakest-precondition try to simplify the predicate
38		compute_enabling_predicate(OpName,OmitOpNameGuard,Pred,FindInvViolations,Res) :-
39		b_get_machine_operation(OpName,_Res,Par,Body),
40		(FindInvViolations==1 ->
41		b_get_invariant_from_machine(Inv),
42		conjunct_predicates([Inv,Pred],Pred1)
43		;otherwise ->
44		Pred1 = Pred
45		),
46		% TODO: add a case for Event-B
47		% compute wp when the source operation is deterministic
48		get_preference(enable_graph_depth,Depth),
49		(Depth==0 ->
50		WP = b(truth,pred,[])
51		%add_warning(weakest_precondition,'Weakest precondition cannot be computed: ',(body(Body),pred(Pred))),
52		%Res = invariant
53		; otherwise ->
54		create_event_body(OpName,Par,Body,NewBody),
55		compute_ep(NewBody,OmitOpNameGuard,Pred1,WP1),
56		%remove_all_infos(WP1,WP2), % consider to use remove_all_infos/2 (problem: all nodeid's will be replaced by a variable,
57		% this causes instatiations errors when using predicate simplifier.)
58		remove_nodeid_infos(WP1,WP)
59		),
60		print_weakest_precondition(OpName,Body,Pred,WP),
61		%% print(weakest_precondition(WP)),nl,
62		simplify_b_predicate(WP,Simplified),
63		print_b_expression(Simplified),
64		Res=predicate(Simplified).
65
66		create_event_body(OpName,Par,Body,Res) :-
67		create_event_body1(OpName,Par,Body,Res).
68
69		create_event_body1(_OpName,[],Body,Res) :- !,
70		Res = Body.
71		create_event_body1(OpName,Par,Body,Res) :-
72		is_list(Par),!,
73		get_texpr_expr(Body,Expr),
74		get_precondition_body(Expr,Par,OpName,InterimRes),
75		create_texpr(InterimRes,subst,[],Res).
76		create_event_body1(OpName,Par,Body,_Res) :-
77		add_error(create_event_body,'The Parameters should be wrapped in a prolog list: ', OpName:Par/Body),fail.
78
79		get_precondition_body(precondition(Condition,Action),Par,_OpName,Res) :- !,
80		Res = any(Par,Condition,Action).
81		get_precondition_body(Body,_Par,_OpName,Res) :-
82		functor(Body,rlevent,11),!,
83		Res = Body.
84		get_precondition_body(OpName,Stmt,_Pre,_InnerBody) :-
85		add_error(get_precondition_body,'Statement not covered yet: ', OpName:Stmt).
86
87		compute_ep(Body,OmitBodyGuard,Pred,WP) :-
88		(OmitBodyGuard==true ->
89		get_texpr_expr(Body,Expr),
90		compute_ep1(Expr,Pred,WP)
91		; otherwise ->
92		weakest_precondition(Body,Pred,WP)
93		).
94
95		compute_ep1(precondition(_Condition,Action),Pred,WP) :- !,
96		% here we do not add the Condition as a conjunct
97		weakest_precondition(Action,Pred,WP).
98		compute_ep1(select([When]),Pred,WP) :- !,
99		get_texpr_expr(When,select_when(_PreCond, Body)),
100		weakest_precondition(Body,Pred,WP).
101		%% compute_ep1(if([If]),Pred,WP) :- !,
102		%% get_texpr_expr(If,if_elsif(_Test,Body)),
103		%% weakest_precondition(Body,Pred,WP).
104		compute_ep1(any(Parameters,Guard,Action),Pred,WP) :- !,
105		remove_free_predicates(Parameters,Guard,NewGuard),
106		weakest_precondition(Action,Pred,InnerWP),
107		safe_create_texpr(conjunct(NewGuard,InnerWP),pred,UnquantifiedWP),
108		create_exists(Parameters,UnquantifiedWP,WP).
109		%% weakest_preconditions: weakest_precondition2(any(Parameters,NewGuard,Action),Pred,WP). % using weakest precondition as enabling predicate is not correct
110		compute_ep1(rlevent(_Name,_Section,_Stat,Parameters,Guard,_Thm,Act,_VWit,_PWit,_Unmod,_AbsEvents),Pred,EP) :- !,
111		%% debug:debug_println(9,rlevent(_Name,_Section,_Stat,Parameters,Guard,_Thm,Act,_VWit,_PWit,_Unmod,_AbsEvents)),
112		% we have "ANY t WHERE Q THEN T END" statement (here we need to add the guard to the WP)
113		% we can sort out the free predicates from Q (at the point of testing the WP we know that there is a representation of the non-deterministic event)
114		remove_free_predicates(Parameters,Guard,RestrictedGuard),
115		% we normalise each event for the case that there are non-deterministic assignments
116		(is_list(Act) ->
117		normalise_to_deterministic_actions_event(Act,NewBody,Parameters,NewParameters,RestrictedGuard,NewGuard)
118		; otherwise ->
119		normalise_to_deterministic_actions_event([Act],NewBody,Parameters,NewParameters,RestrictedGuard,NewGuard)
120		),
121		weakest_precondition(NewBody,Pred,WP),
122		(NewParameters = [] ->
123		EP = WP
124		; otherwise ->
125		safe_create_texpr(conjunct(NewGuard,WP),pred,UnquantifiedEP),
126		create_exists(NewParameters,UnquantifiedEP,EP)
127		).
128		compute_ep1(Body,Pred,EP) :-
129		create_texpr(Body,subst,[],WrappedBody),
130		weakest_precondition(WrappedBody,Pred,EP).
131
132		normalise_to_deterministic_actions_event(Acts,NewBody,Parameters,NewParameters,Guard,NewGuard) :-
133		normalise_nondeterministic_actions(Acts,PrimeParams,NewConjuncts,NewActs),
134		append(Parameters,PrimeParams,NewParameters),
135		conjunct_predicates([Guard|NewConjuncts],NewGuard),
136		create_texpr(parallel(NewActs),subst,[],NewBody).
137		%% safe_create_texpr(conjunct(Guard,NewConjuncts),pred,NewGuard).
138
139		:- use_module(probsrc(btypechecker),[prime_identifiers0/2]).
140		:- use_module(probsrc(bsyntaxtree),[rename_bt/3]).
141		normalise_nondeterministic_actions([],[],[],[]).
142		normalise_nondeterministic_actions([Act|Acts],Parameters,NewConjuncts,NewActs) :-
143		get_texpr_expr(Act,Expr),
144		(Expr = becomes_element_of(IDs,Set) ->
145		prime_variables(IDs,Params),
146		weakest_preconditions: create_members(Set,Params,SetCond),
147		create_texpr(assign(IDs,Parameters),subst,[],PrimeAssign),
148		append(Params,Parameters1,Parameters),
149		NewConjuncts=[SetCond|NewConjuncts1],
150		NewActs = [PrimeAssign|NewActs1]
151		; Expr = becomes_such(Vars,Condition) -> % x:| x<x$0 gets translated to any x$0 where x$0<x then x := x$0 end
152		% also see get_operation_enabling_condition2
153		sort(Vars,Vars1),
154		prime_identifiers0(Vars1,PrimedVars), % generate $0 versions for Vars
155		maplist(gen_rename,Vars1,PrimedVars,RenameList1), % id -> id$0
156		maplist(gen_rename,PrimedVars,Vars1,RenameList2), % id$0 -> id
157		append(RenameList1,RenameList2,RenameList),
158		rename_bt(Condition,RenameList,Condition1),
159		NewConjuncts=[Condition1|NewConjuncts1],
160		create_texpr(assign(Vars1,PrimedVars),subst,[],PrimeAssign),
161		append(PrimedVars,Parameters1,Parameters),
162		NewActs = [PrimeAssign|NewActs1]
163		; otherwise ->
164		NewConjuncts = NewConjuncts1,
165		NewActs = [Act|NewActs1],
166		Parameters = Parameters1
167		),
168		normalise_nondeterministic_actions(Acts,Parameters1,NewConjuncts1,NewActs1).
169
170		:- use_module(probsrc(bsyntaxtree),[def_get_texpr_id/2]).
171		gen_rename(TID1,TID2,rename(ID1,ID2)) :- def_get_texpr_id(TID1,ID1), def_get_texpr_id(TID2,ID2).
172
173
174		remove_free_predicates(Parameters,Guard,NewGuard) :-
175		conjunction_to_list(Guard,Conjuncts),
176		get_texpr_ids(Parameters,Ids),
177		filter_out_global_guards(Conjuncts,Ids,RestConjuncts),
178		conjunct_predicates(RestConjuncts,NewGuard),
179		%% bsyntaxtree:predicate_components_in_scope(Guard,Parameters,Res),
180		(debug_mode(on) ->
181		print('####### Remove global guards #######'),nl,
182		print('Identifiers: '),print(Ids),nl,
183		remove_nodeid_infos(Guard,GuardNoInfos),
184		print('Guard: '),translate:print_bexpr(GuardNoInfos),nl,
185		print('NewGuard: '),translate:print_bexpr(NewGuard),nl,
186		print('####################################'),nl
187		; otherwise -> true).
188
189		filter_out_global_guards([],_Ids,[]).
190		filter_out_global_guards([TExpr|TExprs],Ids,Res) :-
191		(some_id_occurs_in_expr(Ids,TExpr) ->
192		Res=[TExpr|Res1]
193		; otherwise ->
194		Res = Res1
195		), filter_out_global_guards(TExprs,Ids,Res1).
196
197		/* For debugging only */
198		print_weakest_precondition(Opname,Body,Guard,WP) :-
199		(debug_mode(on) ->
200		print('######### Weakest Precondition #########'),nl,
201		remove_nodeid_infos(Guard,GuardNoInfos),
202		translate_bexpression(GuardNoInfos,Guard_PP),
203		translate_bexpression(WP,WP_PP),
204		translate_substitution(Body,RealBody),
205		print('Operation/Event '),print(Opname),print(' :: '),nl,
206		print('['),print(RealBody),print(']'),
207		print('('),print(Guard_PP),print(')'),
208		print(' = '),print(WP_PP),nl,
209		print('########################################'),nl
210		;otherwise -> true).
211
212		print_b_expression(BExpr) :-
213		(debug_mode(on) ->
214		translate_bexpression(BExpr,String),
215		conjunction_to_list(BExpr,List),
216		print(String),nl,
217		print('Conjunctions list: [ '),print_conjunct_l(List)
218		; true).
219
220		print_conjunct_l([]) :-
221		print(' ]'),nl.
222		print_conjunct_l([Expr]) :- !,
223		translate_bexpression(Expr,String),
224		print(String),print(' ]'),nl.
225		print_conjunct_l([Expr|Exprs]) :-
226		translate_bexpression(Expr,String),
227		print(String),print(', '),
228		print_conjunct_l(Exprs).
229
230		remove_nodeid_infos(Expr,Res) :-
231		var(Expr),!,
232		Res=Expr.
233		remove_nodeid_infos(Expr,Res) :-
234		is_list(Expr),!,
235		maplist(remove_nodeid_infos,Expr,Res).
236		remove_nodeid_infos(Expr,Res) :-
237		Expr =.. [F|Args],
238		remove_nodeid_infos1(F,Args,Res).
239
240		remove_nodeid_infos1(nodeid,_Args,Res) :-
241		% ignore additional node infos
242		!, Res =.. [nodeid,none].
243		remove_nodeid_infos1(F,Args,Res) :-
244		maplist(remove_nodeid_infos,Args,ArgsRes),
245		Res =.. [F|ArgsRes].