1		% (c) 2015-2022 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(pge_algo, [
6		%%%% Static Analysis Predicates %%%%
7		tcltk_disabling_analysis/1,
8		%%%% Model Checker predicates %%%%
9		compute_transitions_pge/2,
10		%%%% INFO %%%%
11		disabled_operations_stats/1,
12		is_pge_opt_on/0,
13		is_pge_opt_on/1,
14		compute_and_update_disabled_enabled_operations/3,
15		compute_operation_relations_for_pge/1,
16		compute_operation_relations_for_pge_if_necessary/2
17		]).
18
19		/* SICSTUS Libraries */
20		:- use_module(library(ordsets)).
21		:- use_module(library(lists)).
22		%% :- use_module(library(timeout)).
23
24		/* B module sources */
25		:- use_module(probsrc(bmachine),[b_top_level_operation/1,b_machine_has_constants_or_properties/0]).
26		:- use_module(probsrc(b_state_model_check), [get_guard/2,get_negated_guard/3]).
27		:- use_module(probsrc(state_space),[clear_context_state/0]).
28		:- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2,create_negation/2]).
29		:- use_module(probporsrc(static_analysis), [
30		get_conj_inv_predicate/3,
31		catch_and_ignore_well_definedness_error/2,
32		test_path_non_failing/6]).
33		:- use_module(cbcsrc(enabling_analysis), [init_or_op/1, print_enable_table/1]).
34		:- use_module(probsrc(b_read_write_info),[b_get_read_write/3,b_get_operation_read_guard_vars/4]).
35
36		/* Importing predicates for handling the states of a respective B/Event-B machine */
37		:- use_module(probsrc(eventhandling),[register_event_listener/3]).
38		:- use_module(probsrc(specfile),[specfile_possible_trans_name_for_successors/2,
39		prepare_state_for_specfile_trans/3,animation_mode/1]).
40		:- use_module(probsrc(state_space),[ %visited_expression/2,
41		assert_time_out_for_node/3,
42		use_no_timeout/1,assert_max_reached_for_node/1]).
43		:- use_module(probsrc(value_persistance), [save_constants/1,add_new_transitions_to_cache/1]).
44		:- use_module(probsrc(succeed_max),[reset_max_reached/0,max_reached/0]).
45		:- use_module(probsrc(preferences),[get_preference/2]).
46		:- use_module(probsrc(error_manager),[enter_new_error_scope/1, exit_error_scope/3,specific_event_occurred_at_level/2,clear_all_errors_in_error_scope/1,
47		is_time_out_result/1,set_error_context/1,clear_error_context/0,time_out_with_enum_warning_for_findall/3,
48		add_warning/3, add_error_fail/3]).
49		:- use_module(probsrc(tools),[cputime/1,print_message/1]).
50		:- use_module(probsrc(debug)).
51		:- use_module(probsrc(state_space),[find_initialised_states/1]).
52
53		/* Modules and Infos for the code coverage analysis */
54		:- use_module(probsrc(module_information)).
55		:- module_info(group,model_checker).
56		:- module_info(description,'This module contains predictes for model checking B and Event-B models using the partial guard evaluation optimisastion. Only applicable in B mode.').
57
58		%------------------------------------
59
60		%%%%%% Dynamic predicates used for: saving the enabling relations, number of skipped guard evaluations,
61		%%%%%% and sets of enabled and disabled events at the various states. %%%%%
62
63		% for the PGE analysis
64		:- dynamic disables/2, enables/2, keeps/2.
65		%%% enabling_relations(Op1,Op2,Enable,KeepEnabled,Disable,KeepDisabled)
66		:- dynamic enabling_relations/6.
67		:- dynamic pge_predicates_computed/0.
68
69		% for the state space exploration by means of PGE
70		:- dynamic disabled_operations/3.
71
72		% for keeping track of the skipped guard evaluations
73		:- dynamic nr_skipped_guard_evaluations/1.
74
75		:- register_event_listener(clear_specification,clear_dynamic_predicates_for_pge,
76		'Partial Guard Evaluation.').
77
78		clear_dynamic_predicates_for_pge :-
79		retractall(keeps(_,_)),
80		retractall(disables(_,_)),
81		retractall(disabled_operations(_,_,_)),
82		retractall(pge_predicates_computed),
83		retractall(nr_skipped_guard_evaluations(_)),
84		retractall(enabling_relations(_,_,_,_,_,_)).
85
86		disabled_operations_stats(ResPGE) :-
87		is_pge_opt_on,
88		animation_mode(b),!,
89		nr_skipped_guard_evaluations(NrSkippedEvaluations),
90		ResPGE = ['SKIPPED_GUARD_EVALUATIONS: ',NrSkippedEvaluations].
91		disabled_operations_stats(ResPGE) :- % otherwise no information is available
92		ResPGE = [].
93
94		is_pge_opt_on :-
95		get_preference(pge,Pref),
96		is_pge_opt_on(Pref).
97
98		is_pge_opt_on(off) :- !,fail.
99		is_pge_opt_on(Pref) :-
100		member(Pref,[disabled,disabled2,enabled,enabled2,full,full2]),!.
101		is_pge_opt_on(Pref) :-
102		add_error_fail(pge,'Unknown Partial Guard Evaluation (PGE) preference: ', Pref).
103
104		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
105		%%%%%%%%%%%%%%%%% PGE Analysis %%%%%%%%%%%%%%%%%
106		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
107
108		compute_operation_relations_for_pge_if_necessary(off,_FindInvViolations).
109		compute_operation_relations_for_pge_if_necessary(PGEPref,FindInvViolations) :-
110		is_pge_opt_on(PGEPref),!,
111		compute_operation_relations_for_pge(FindInvViolations).
112		compute_operation_relations_for_pge_if_necessary(_PGEPref,_FindInvViolations).
113
114		compute_operation_relations_for_pge(FindInvViolations) :-
115		(pge_predicates_computed
116		-> true
117		; debug_println(19,'********** START PGE ANALYSIS *************'),
118		get_preference(timeout_cbc_analysis,Timeout),
119		cputime(T1),
120		enter_new_error_scope(ScopeID),
121		get_preference(pge,Pref),
122		(member(Pref,[disabled,enabled,full]) ->
123		call_cleanup(compute_impossible_keep_guaranteed(FindInvViolations,Timeout,Pref),
124		my_exit_error_scope(ScopeID))
125		; member(Pref,[disabled2,enabled2,full2]) -> % now used for experimental issues
126		call_cleanup(compute_enabling_relations(FindInvViolations,Timeout,Pref),
127		my_exit_error_scope(ScopeID))
128		;
129		add_warning(pge,'Unknown PGE preference: ',Pref)
130		),
131		assert_disabled_ops_to_init_states_if_necessary,
132		cputime(T2),
133		debug_println(19,'********** PGE ANALYSIS FINISHED **********'),
134		D is T2-T1,
135		formatsilent('PGE Analysis Checking Time: ~w ms.~n',[D]),
136		assertz(pge_predicates_computed),
137		assertz(nr_skipped_guard_evaluations(0)),
138		!
139		).
140
141		%%%%%%%% Analysis for the enabling relations: keep, guaranteed, and impossible (in case 'pge' is set to 'enabled', 'disabled', or 'full') %%%%%%%%%%
142		% failure loop
143		compute_impossible_keep_guaranteed(FindInvViolations,Timeout,Pref) :-
144		init_or_op(OpName1),
145		b_get_read_write(OpName1,_Reads1,Writes1),
146		b_top_level_operation(OpName2),
147		b_get_operation_read_guard_vars(OpName2,true,GReads2,_Precise),
148		(OpName1\='INITIALISATION',\+ord_intersect(Writes1,GReads2) ->
149		assertz(keeps(OpName1,OpName2)),
150		debug_println(9,keeps(OpName1, OpName2))
151		; (Pref\=enabled, disables(OpName1,OpName2,FindInvViolations,Timeout)) ->
152		assertz(disables(OpName1,OpName2)),
153		debug_println(9,disables(OpName1,OpName2))
154		; (Pref\=disabled, enables(OpName1,OpName2,FindInvViolations,Timeout)) ->
155		assertz(enables(OpName1,OpName2)),
156		debug_println(9,enables(OpName1,OpName2))
157		; true
158		),fail.
159		compute_impossible_keep_guaranteed(_FindInvViolations,_Timeout,_Pref).
160
161		:- use_module(cbcsrc(cbc_path_solver), [testcase_path_timeout/9]).
162		disables('INITIALISATION',OpName2,FindInvViolations,Timeout) :-
163		get_goal_predicate(OpName2,FindInvViolations,no,GoalPred),
164		(catch_and_ignore_well_definedness_error(
165		cbc_path_solver:testcase_path_timeout(init,Timeout,[],GoalPred,_,_,_,_,_R),_Result) -> fail; true).
166		disables(OpName1, OpName2, FindInvViolations, Timeout) :-
167		get_start_predicate(OpName1,FindInvViolations,StartPred),
168		get_goal_predicate(OpName2,FindInvViolations,no,GoalPred),
169		(catch_and_ignore_well_definedness_error(
170		cbc_path_solver:testcase_path_timeout(StartPred,Timeout,[OpName1],GoalPred,_,_,_,_,_R),_Result) ->fail; true).
171
172		enables('INITIALISATION',OpName2,FindInvViolations,Timeout) :-
173		get_goal_predicate(OpName2,FindInvViolations,yes,GoalPred),
174		(catch_and_ignore_well_definedness_error(
175		cbc_path_solver:testcase_path_timeout(init,Timeout,[],GoalPred,_,_,_,_,_R),_Result) ->fail; true).
176		enables(OpName1, OpName2, FindInvViolations, Timeout) :-
177		get_start_predicate(OpName1,FindInvViolations,StartPred),
178		get_goal_predicate(OpName2,FindInvViolations,yes,GoalPred),
179		(catch_and_ignore_well_definedness_error(
180		cbc_path_solver:testcase_path_timeout(StartPred,Timeout,[OpName1],GoalPred,_,_,_,_,_R),_Result) ->fail; true).
181
182		get_start_predicate(OpName,FindInvViolations,StartPred) :-
183		get_guard(OpName,PosGuard),
184		(FindInvViolations=1 -> StartPred = pred(PosGuard); StartPred=typing(PosGuard)).
185
186		get_goal_predicate(OpName,FindInvViolations,Negated,GoalPred) :-
187		get_negated_guard(OpName,PosGuard,NegGuard),
188		(Negated = yes -> GuardPred = NegGuard; GuardPred = PosGuard),
189		get_conj_inv_predicate([GuardPred],FindInvViolations,GoalPred). % add invariant if we perform invariant checking
190
191		%%%%%%%% Analysis for the enabling relations: ER(e1,e2) (in case 'pge' is set to 'enabled2', 'disabled2', or 'full2') %%%%%%%%%%
192		% failure loop
193		compute_enabling_relations(FindInvViolations,Timeout,Pref) :-
194		init_or_op(OpName1),
195		b_top_level_operation(OpName2),
196		b_get_read_write(OpName1,_Reads1,Writes1),
197		b_get_operation_read_guard_vars(OpName2,true,GReads2,_Precise),
198		(OpName1='INITIALISATION' ->
199		true % we do not predict the enabling status of the events in the init state, for now...
200		;
201		((\+ord_intersect(Writes1,GReads2)) ->
202		assertz(enabling_relations(OpName1,OpName2,false,ok,false,ok)),
203		debug_println(9,enabling_relations(OpName1,OpName2,false,ok,false,ok))
204		;
205		compute_cbc_enabling_relation_and_assert(OpName1,OpName2,FindInvViolations,Timeout,Pref)
206		)),fail.
207		compute_enabling_relations(_FindInvViolations,_Timeout,_Pref).
208
209		compute_cbc_enabling_relation_and_assert(OpName1,OpName2,FindInvViolations,Timeout,Pref) :-
210		b_get_read_write(OpName1,_Reads1_,Writes1),
211		get_negated_guard(OpName2,PosGuard2,NegGuard2),
212		enabling_analysis: partition_predicate(PosGuard2,Writes1,FilteredPosGuard2,StaticPosGuard2),
213		create_negation(FilteredPosGuard2,FilteredNegGuard2),
214		(OpName1==OpName2 ->
215		KeepDisabled=false, Enable=false,
216		(Pref=enabled2 ->
217		test_path_non_failing(PosGuard2,[OpName1],FilteredNegGuard2,FindInvViolations,Timeout,Disable),
218		KeepEnabled = unknown
219		;Pref=disabled2 ->
220		translate: print_bexpr(PosGuard2),
221		translate: print_bexpr(FilteredPosGuard2),
222		test_path_non_failing(PosGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,KeepEnabled),
223		Disable = unknown
224		;
225		test_path_non_failing(PosGuard2,[OpName1],FilteredNegGuard2,FindInvViolations,Timeout,Disable),
226		test_path_non_failing(PosGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,KeepEnabled)
227		)
228		;
229		conjunct_predicates([StaticPosGuard2,FilteredNegGuard2],NegEnableGuard2),
230		(Pref=enabled2 -> % need to known just Disable and KeepDisabled
231		Enable = unknown, KeepEnabled = unknown,
232		test_path_non_failing(PosGuard2,[OpName1],FilteredNegGuard2,FindInvViolations,Timeout,Disable),
233		test_path_non_failing(NegGuard2,[OpName1],NegGuard2,FindInvViolations,Timeout,KeepDisabled)
234		;Pref=disabled2 -> % need to known just Enable and KeepEnabled
235		test_path_non_failing(NegEnableGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,Enable),
236		test_path_non_failing(PosGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,KeepEnabled),
237		Disable = unknown, KeepDisabled = unknown
238		; % we have full2
239		test_path_non_failing(NegEnableGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,Enable),
240		test_path_non_failing(PosGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,KeepEnabled),
241		test_path_non_failing(PosGuard2,[OpName1],FilteredNegGuard2,FindInvViolations,Timeout,Disable),
242		test_path_non_failing(NegGuard2,[OpName1],NegGuard2,FindInvViolations,Timeout,KeepDisabled)
243		)
244		),
245		prove_and_assert_enabling_relation(OpName1,OpName2,Enable,KeepEnabled,Disable,KeepDisabled),
246		debug_println(9,enabling_relations(OpName1,OpName2,Enable,KeepEnabled,Disable,KeepDisabled)).
247
248		prove_and_assert_enabling_relation(OpName1,OpName2,Enable,KeepEnabled,Disable,KeepDisabled) :-
249		(maplist(nonvar,[Enable,KeepEnabled,Disable,KeepDisabled]) ->
250		assertz(enabling_relations(OpName1,OpName2,Enable,KeepEnabled,Disable,KeepDisabled))
251		; add_warning(cbc_enabling_relation,'A variable result occurred for one of the enabling relations result',
252		[Enable,KeepEnabled,Disable,KeepDisabled])).
253
254
255		my_exit_error_scope(ScopeID) :-
256		(specific_event_occurred_at_level(ScopeID,Event) ->
257		format('### ERROR/ENUMERATION WARING OCCURED : ~w !~n',[Event])),fail.
258		my_exit_error_scope(ScopeID) :- %error_manager:print_error_scopes,
259		clear_all_errors_in_error_scope(ScopeID),
260		exit_error_scope(ScopeID,_,my_exit_error_scope).
261
262		% TODO: consider if we need this at all
263		tcltk_disabling_analysis(list([list(['Origin'|Ops])|Result])) :-
264		get_preference(timeout_cbc_analysis,Timeout),
265		findall(Op, b_top_level_operation(Op), Ops),
266		findall(list([OpName1|DisableList]),
267		(init_or_op(OpName1),
268		findall(Disables,(b_top_level_operation(OpName2),(disables(OpName1,OpName2,1,Timeout) -> Disables=yes; Disables=no)),DisableList)),
269		Result),
270		print_enable_table([list(['Origin'|Ops])|Result]).
271
272		%----------------- Auxiliary predicates for the Partial Guard Evaluation implementation
273
274		:- use_module(probsrc(tcltk_interface),[add_transition/4]).
275		add_transition_timeout(CurID,CurTO,CurState,ActionName,NewId) :-
276		set_error_context(operation(ActionName,CurID)),
277		(CurTO > 0
278		-> time_out_with_enum_warning_for_findall(tcltk_interface:add_transition(CurID,CurState,ActionName,NewId),CurTO,TimeOutRes),
279		check_timeout_result(CurID,ActionName,CurTO,TimeOutRes)
280		; add_transition(CurID,CurState,ActionName,NewId)
281		).
282
283		check_timeout_result(CurID,ActionName,CurTO,TimeOutRes) :-
284		(is_time_out_result(TimeOutRes)
285		->
286		( TimeOutRes = virtual_time_out(_) ->
287		true
288		; print_message('TIME OUT: '), print_message(CurID), print_message(CurTO),
289		print_message(ActionName)
290		),
291		(var(ActionName)
292		-> assert_time_out_for_node(CurID,'unspecified_operation',TimeOutRes)
293		; assert_time_out_for_node(CurID,ActionName,TimeOutRes))
294		; true
295		).
296
297		setup_constants_state1(csp_and_b_root) :- !.
298		setup_constants_state1(CurState) :-
299		setup_constants_state(CurState).
300
301		setup_constants_state(concrete_constants(_)).
302		setup_constants_state(const_and_vars(_,_)).
303
304		% failure loop
305		assert_disabled_ops_to_init_states_if_necessary :-
306		\+b_machine_has_constants_or_properties, % we do not want to explore states prior to firing the model checker
307		findall(Op,disables('INITIALISATION',Op),DisabledOps),
308		findall(Op,enables('INITIALISATION',Op),EnabledOps),
309		% init states finds exactly the initial states of the checked machine
310		find_initialised_states(Init),
311		member(I,Init),
312		assertz(disabled_operations(I,DisabledOps,EnabledOps)),
313		fail.
314		assert_disabled_ops_to_init_states_if_necessary.
315
316
317		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
318		%%%%%%%%%%%%%%%%%% State Exploration by means of PGE %%%%%%%%%%%%%%%%%%%%%%%
319		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
320
321		:- use_module(probsrc(tcltk_interface),[catch_clpfd_overflow_call_for_state/4]).
322		compute_transitions_pge(CurID,CurState) :-
323		catch_clpfd_overflow_call_for_state(CurID,'computing transitions for PGE',
324		pge_algo:compute_transitions_pge2(CurID,CurState),
325		clear_context_state).
326		:- public compute_transitions_pge2/2.
327		compute_transitions_pge2(CurID,CurState) :-
328		reset_max_reached,
329		prepare_state_for_specfile_trans(CurState,CurID,PreparedCurState),
330		(use_no_timeout(CurID) ->
331		add_transitions_pge(CurID,PreparedCurState,0)
332		;
333		preferences: preference(time_out,CurTO),
334		add_transitions_pge(CurID,PreparedCurState,CurTO)
335		),
336		(setup_constants_state1(CurState) -> true ; retractall(disabled_operations(CurID,_,_))),
337		debug_println(9,state_has_been_explored(CurID,CurState)),
338		clear_error_context,
339		(max_reached -> assert_max_reached_for_node(CurID),MaxReached=true ; MaxReached=false),
340		(CurID==root -> save_constants(MaxReached) ; add_new_transitions_to_cache(CurID)).
341
342
343		add_transitions_pge(CurID,CurState,CurTO) :-
344		% PossiblyEnActionNames contains all possible actions that are not recognised to be disabled and need to be tested for enabledness
345		get_possible_enabled_trans_names(CurID,CurState,DisabledOperations,EnabledOperations,PossiblyEnActionNames),
346		explore_current_state_pge(PossiblyEnActionNames,CurID,CurState,CurTO,EnabledOperations,Transitions,DisabledActionsNew),
347		list_to_ord_set(DisabledActionsNew,DisabledActionsNewSet),
348		ord_union(DisabledOperations,DisabledActionsNewSet,DisabledActionsAtCurState),
349		maplist(get_first_argument,Transitions,EnabledActions),
350		list_to_ord_set(EnabledActions,EnabledActionsAtCurState),
351		compute_and_update_disabled_enabled_operations(Transitions,DisabledActionsAtCurState,EnabledActionsAtCurState).
352
353		get_possible_enabled_trans_names(CurID,CurState,DisabledOperations,EnabledOperations,PossiblyEnActionNames) :-
354		(disabled_operations(CurID,DisabledOperations,EnabledOperations) -> true; DisabledOperations = [], EnabledOperations = []),
355		get_possible_enabled_trans_names_aux(CurID,CurState,DisabledOperations,PossiblyEnActionNames).
356
357		get_possible_enabled_trans_names_aux(CurID,CurState,DisabledOperations,PossiblyEnActionNames) :-
358		findall(PossibleEnActionName,
359		(specfile_possible_trans_name_for_successors(CurState,PossibleEnActionName),
360		not_a_member_of_disabled(PossibleEnActionName,DisabledOperations)),
361		PossiblyEnActionNames),
362		debug_println(9,skipped_guard_evaluations_at_state(CurID,DisabledOperations)).
363
364		not_a_member_of_disabled(ActionName,DisabledOperations) :-
365		(ord_member(ActionName,DisabledOperations) ->
366		retract(nr_skipped_guard_evaluations(NrDisabled)),
367		NrDisabled1 is NrDisabled + 1,
368		assertz(nr_skipped_guard_evaluations(NrDisabled1)),
369		fail
370		; true).
371
372
373		:- use_module(probsrc(preferences),[temporary_set_preference/3,reset_temporary_preference/2]).
374
375		explore_current_state_pge(ActionNames,CurID,CurState,CurTO,EnabledOperations,Transitions,DisabledActionsNew) :-
376		explore_current_state_pge1(ActionNames,CurID,CurState,CurTO,EnabledOperations,[],Transitions,[],DisabledActionsNew).
377
378		explore_current_state_pge1([],_CurID,_CurState,_CurTO,_EnabledOperations,Transitions,Transitions,DisabledActions,DisabledActions).
379		explore_current_state_pge1([ActionName|R],CurID,CurState,CurTO,EnabledOperations,TransitionsGen,Transitions,DisabledActionsGen,DisabledActions) :-
380		(ord_member(ActionName,EnabledOperations) ->
381		retract(nr_skipped_guard_evaluations(NrDisabled)),
382		NrDisabled1 is NrDisabled +1,
383		assertz(nr_skipped_guard_evaluations(NrDisabled1)),
384		debug_println(9,do_not_evaluate_guard(ActionName)),
385		temporary_set_preference(ltsmin_do_not_evaluate_top_level_guards,full,CHNG)
386		;
387		CHNG=false % so that reset_temporary_preference does nothing
388		),
389		findall(NewId,add_transition_timeout(CurID,CurTO,CurState,ActionName,NewId),NewIds),
390		(NewIds = [] -> % ActionName is disabled at CurState
391		TransitionsGen1 = TransitionsGen,
392		DisabledActionsGen1 = [ActionName|DisabledActionsGen]
393		;
394		TransitionsGen1 = [(ActionName,NewIds)|TransitionsGen],
395		DisabledActionsGen1 = DisabledActionsGen
396		),
397		reset_temporary_preference(ltsmin_do_not_evaluate_top_level_guards,CHNG),
398		explore_current_state_pge1(R,CurID,CurState,CurTO,EnabledOperations,TransitionsGen1,Transitions,DisabledActionsGen1,DisabledActions).
399
400		compute_and_update_disabled_enabled_operations([],_DisabledActionsAtCurState,_EnabledActionsAtCurState).
401		compute_and_update_disabled_enabled_operations([(ActionName,SuccStates)|R],DisabledActionsAtCurState,EnabledActionsAtCurState) :-
402		compute_disabled_operations(ActionName,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateDisabledActions),
403		compute_enabled_operations(ActionName,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateEnabledActions),
404		update_disabled_enabled_operations_l(SuccStates,SuccStateDisabledActions,SuccStateEnabledActions),
405		compute_and_update_disabled_enabled_operations(R,DisabledActionsAtCurState,EnabledActionsAtCurState).
406
407		compute_disabled_operations(ActionName,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateDisabledActions) :-
408		get_preference(pge,Pref),
409		(check_only_enabled(Pref) ->
410		SuccStateDisabledActions = []
411		; compute_disabled_operations_after_state(Pref,ActionName,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateDisabledActions)
412		).
413
414		compute_enabled_operations(ActionName,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateEnabledActions) :-
415		get_preference(pge,Pref),
416		(check_only_disabled(Pref) ->
417		SuccStateEnabledActions = []
418		; compute_enabled_operations_after_state(Pref,ActionName,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateEnabledActions)
419		).
420
421		update_disabled_enabled_operations_l(StateIDs,NewDisabledOperations,NewEnabledOperations) :-
422		maplist(update_disabled_enabled_operations(NewDisabledOperations,NewEnabledOperations),StateIDs).
423
424		update_disabled_enabled_operations(NewDisabledOperations,NewEnabledOperations,StateID) :-
425		(disabled_operations(StateID,DisabledOperations,EnabledOperations) ->
426		ord_union(DisabledOperations,NewDisabledOperations,DisabledOperations1),
427		ord_union(EnabledOperations,NewEnabledOperations,EnabledOperations1),
428		retractall(disabled_operations(StateID,_,_)),
429		assertz(disabled_operations(StateID,DisabledOperations1,EnabledOperations1))
430		;
431		assertz(disabled_operations(StateID,NewDisabledOperations,NewEnabledOperations))
432		).
433
434		compute_disabled_operations_after_state(Pref,OpName1,DisabledActionsAtCurState,_EnabledActionsAtCurState,SuccStateDisabledActions) :-
435		(Pref = disabled; Pref = full),!,
436		findall(OpName2,disables(OpName1,OpName2),ImpossibleEnabled),
437		findall(OpName2,get_disabled_action_by_keep(OpName1,DisabledActionsAtCurState,OpName2),SuccStateDisabledActions1,ImpossibleEnabled),
438		list_to_ord_set(SuccStateDisabledActions1,SuccStateDisabledActions).
439		compute_disabled_operations_after_state(Pref,OpName1,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateDisabledActions) :-
440		(Pref = disabled2; Pref = full2),!,
441		findall(OpName2,(member(OpName2,EnabledActionsAtCurState),enabling_relations(OpName1,OpName2,_,false,_,_)),DisbaledOps1),
442		findall(OpName2,(animation_mode(b),member(OpName2,DisabledActionsAtCurState),enabling_relations(OpName1,OpName2,false,_,_,_)),DisabledOps2,DisbaledOps1),
443		list_to_ord_set(DisabledOps2,SuccStateDisabledActions).
444		compute_disabled_operations_after_state(_Pref,_OpName1,_DisabledActionsAtCurState,_EnabledActionsAtCurState,[]).
445
446		get_disabled_action_by_keep(OpName1,DisabledActionsAtCurState,OpName2) :-
447		animation_mode(b),!, % can be applied only in B mode, for CSP||B is generally not sound
448		member(OpName2,DisabledActionsAtCurState),
449		keeps(OpName1,OpName2).
450
451		compute_enabled_operations_after_state(Pref,OpName1,_DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateEnabledActions) :-
452		(Pref = enabled; Pref = full),!,
453		findall(OpName2,enables(OpName1,OpName2),GuaranteedEnabled),
454		findall(OpName2,get_enabled_action_by_keep(OpName1,EnabledActionsAtCurState,OpName2),SuccStateEnabledActions1,GuaranteedEnabled),
455		list_to_ord_set(SuccStateEnabledActions1,SuccStateEnabledActions).
456		compute_enabled_operations_after_state(Pref,OpName1,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateEnabledActions) :-
457		(Pref = enabled2; Pref = full2),!,
458		findall(OpName2,(member(OpName2,EnabledActionsAtCurState),enabling_relations(OpName1,OpName2,_,_,false,_)),EnabledOps1),
459		findall(OpName2,(animation_mode(b),member(OpName2,DisabledActionsAtCurState),enabling_relations(OpName1,OpName2,_,_,_,false)),EnabledOps2,EnabledOps1),
460		list_to_ord_set(EnabledOps2,SuccStateEnabledActions).
461		compute_enabled_operations_after_state(_Pref,_OpName1,_DisabledActionsAtCurState,_EnabledActionsAtCurState,[]).
462
463		get_enabled_action_by_keep(OpName1,EnabledActionsAtCurState,OpName2) :-
464		member(OpName2,EnabledActionsAtCurState),
465		keeps(OpName1,OpName2).
466
467		get_first_argument((A,_B),A).
468
469		check_only_disabled(disabled).
470		check_only_disabled(disabled2).
471
472		check_only_enabled(enabled).
473		check_only_enabled(enabled2).
474
475		%------------------------------