1		% (c) 2015-2025 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		:- use_module(probsrc(runtime_profiler),[start_profile/2, stop_profile/4]).
115
116		compute_operation_relations_for_pge(FindInvViolations) :-
117		(pge_predicates_computed
118		-> true
119		; debug_println(19,'********** START PGE ANALYSIS *************'),
120		start_profile(partial_order_reduction,Timer),
121		get_preference(timeout_cbc_analysis,Timeout),
122		cputime(T1),
123		enter_new_error_scope(ScopeID),
124		get_preference(pge,Pref),
125		(member(Pref,[disabled,enabled,full]) ->
126		call_cleanup(compute_impossible_keep_guaranteed(FindInvViolations,Timeout,Pref),
127		my_exit_error_scope(ScopeID))
128		; member(Pref,[disabled2,enabled2,full2]) -> % now used for experimental issues
129		call_cleanup(compute_enabling_relations(FindInvViolations,Timeout,Pref),
130		my_exit_error_scope(ScopeID))
131		;
132		add_warning(pge,'Unknown PGE preference: ',Pref)
133		),
134		assert_disabled_ops_to_init_states_if_necessary,
135		cputime(T2),
136		debug_println(19,'********** PGE ANALYSIS FINISHED **********'),
137		D is T2-T1,
138		formatsilent('PGE Analysis Checking Time: ~w ms.~n',[D]),
139		assertz(pge_predicates_computed),
140		assertz(nr_skipped_guard_evaluations(0)),
141		stop_profile(partial_order_reduction,compute_pge_relations,unknown,Timer),
142		!
143		).
144
145		%%%%%%%% Analysis for the enabling relations: keep, guaranteed, and impossible (in case 'pge' is set to 'enabled', 'disabled', or 'full') %%%%%%%%%%
146		% failure loop
147		compute_impossible_keep_guaranteed(FindInvViolations,Timeout,Pref) :-
148	?	init_or_op(OpName1),
149		b_get_read_write(OpName1,_Reads1,Writes1),
150	?	b_top_level_operation(OpName2),
151		b_get_operation_read_guard_vars(OpName2,true,GReads2,_Precise),
152		(OpName1\='INITIALISATION',\+ord_intersect(Writes1,GReads2) ->
153		assertz(keeps(OpName1,OpName2)),
154		debug_println(9,keeps(OpName1, OpName2))
155	?	; (Pref\=enabled, disables(OpName1,OpName2,FindInvViolations,Timeout)) ->
156		assertz(disables(OpName1,OpName2)),
157		debug_println(9,disables(OpName1,OpName2))
158	?	; (Pref\=disabled, enables(OpName1,OpName2,FindInvViolations,Timeout)) ->
159		assertz(enables(OpName1,OpName2)),
160		debug_println(9,enables(OpName1,OpName2))
161		; true
162		),fail.
163		compute_impossible_keep_guaranteed(_FindInvViolations,_Timeout,_Pref).
164
165		:- use_module(cbcsrc(cbc_path_solver), [testcase_path_timeout/9]).
166		disables('INITIALISATION',OpName2,FindInvViolations,Timeout) :-
167		get_goal_predicate(OpName2,FindInvViolations,no,GoalPred),
168		(catch_and_ignore_well_definedness_error(
169		cbc_path_solver:testcase_path_timeout(init,Timeout,[],GoalPred,_,_,_,_,_R),_Result) -> fail; true).
170		disables(OpName1, OpName2, FindInvViolations, Timeout) :-
171		get_start_predicate(OpName1,FindInvViolations,StartPred),
172		get_goal_predicate(OpName2,FindInvViolations,no,GoalPred),
173		(catch_and_ignore_well_definedness_error(
174		cbc_path_solver:testcase_path_timeout(StartPred,Timeout,[OpName1],GoalPred,_,_,_,_,_R),_Result) ->fail; true).
175
176		enables('INITIALISATION',OpName2,FindInvViolations,Timeout) :-
177		get_goal_predicate(OpName2,FindInvViolations,yes,GoalPred),
178		(catch_and_ignore_well_definedness_error(
179		cbc_path_solver:testcase_path_timeout(init,Timeout,[],GoalPred,_,_,_,_,_R),_Result) ->fail; true).
180		enables(OpName1, OpName2, FindInvViolations, Timeout) :-
181		get_start_predicate(OpName1,FindInvViolations,StartPred),
182		get_goal_predicate(OpName2,FindInvViolations,yes,GoalPred),
183		(catch_and_ignore_well_definedness_error(
184		cbc_path_solver:testcase_path_timeout(StartPred,Timeout,[OpName1],GoalPred,_,_,_,_,_R),_Result) ->fail; true).
185
186		get_start_predicate(OpName,FindInvViolations,StartPred) :-
187		get_guard(OpName,PosGuard),
188		(FindInvViolations=1 -> StartPred = pred(PosGuard); StartPred=typing(PosGuard)).
189
190		get_goal_predicate(OpName,FindInvViolations,Negated,GoalPred) :-
191		get_negated_guard(OpName,PosGuard,NegGuard),
192		(Negated = yes -> GuardPred = NegGuard; GuardPred = PosGuard),
193		get_conj_inv_predicate([GuardPred],FindInvViolations,GoalPred). % add invariant if we perform invariant checking
194
195		%%%%%%%% Analysis for the enabling relations: ER(e1,e2) (in case 'pge' is set to 'enabled2', 'disabled2', or 'full2') %%%%%%%%%%
196		% failure loop
197		compute_enabling_relations(FindInvViolations,Timeout,Pref) :-
198		init_or_op(OpName1),
199		b_top_level_operation(OpName2),
200		b_get_read_write(OpName1,_Reads1,Writes1),
201		b_get_operation_read_guard_vars(OpName2,true,GReads2,_Precise),
202		(OpName1='INITIALISATION' ->
203		true % we do not predict the enabling status of the events in the init state, for now...
204		;
205		((\+ord_intersect(Writes1,GReads2)) ->
206		assertz(enabling_relations(OpName1,OpName2,false,ok,false,ok)),
207		debug_println(9,enabling_relations(OpName1,OpName2,false,ok,false,ok))
208		;
209		compute_cbc_enabling_relation_and_assert(OpName1,OpName2,FindInvViolations,Timeout,Pref)
210		)),fail.
211		compute_enabling_relations(_FindInvViolations,_Timeout,_Pref).
212
213		compute_cbc_enabling_relation_and_assert(OpName1,OpName2,FindInvViolations,Timeout,Pref) :-
214		b_get_read_write(OpName1,_Reads1_,Writes1),
215		get_negated_guard(OpName2,PosGuard2,NegGuard2),
216		enabling_analysis: partition_predicate(PosGuard2,Writes1,FilteredPosGuard2,StaticPosGuard2),
217		create_negation(FilteredPosGuard2,FilteredNegGuard2),
218		(OpName1==OpName2 ->
219		KeepDisabled=false, Enable=false,
220		(Pref=enabled2 ->
221		test_path_non_failing(PosGuard2,[OpName1],FilteredNegGuard2,FindInvViolations,Timeout,Disable),
222		KeepEnabled = unknown
223		;Pref=disabled2 ->
224		translate: print_bexpr(PosGuard2),
225		translate: print_bexpr(FilteredPosGuard2),
226		test_path_non_failing(PosGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,KeepEnabled),
227		Disable = unknown
228		;
229		test_path_non_failing(PosGuard2,[OpName1],FilteredNegGuard2,FindInvViolations,Timeout,Disable),
230		test_path_non_failing(PosGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,KeepEnabled)
231		)
232		;
233		conjunct_predicates([StaticPosGuard2,FilteredNegGuard2],NegEnableGuard2),
234		(Pref=enabled2 -> % need to known just Disable and KeepDisabled
235		Enable = unknown, KeepEnabled = unknown,
236		test_path_non_failing(PosGuard2,[OpName1],FilteredNegGuard2,FindInvViolations,Timeout,Disable),
237		test_path_non_failing(NegGuard2,[OpName1],NegGuard2,FindInvViolations,Timeout,KeepDisabled)
238		;Pref=disabled2 -> % need to known just Enable and KeepEnabled
239		test_path_non_failing(NegEnableGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,Enable),
240		test_path_non_failing(PosGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,KeepEnabled),
241		Disable = unknown, KeepDisabled = unknown
242		; % we have full2
243		test_path_non_failing(NegEnableGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,Enable),
244		test_path_non_failing(PosGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,KeepEnabled),
245		test_path_non_failing(PosGuard2,[OpName1],FilteredNegGuard2,FindInvViolations,Timeout,Disable),
246		test_path_non_failing(NegGuard2,[OpName1],NegGuard2,FindInvViolations,Timeout,KeepDisabled)
247		)
248		),
249		prove_and_assert_enabling_relation(OpName1,OpName2,Enable,KeepEnabled,Disable,KeepDisabled),
250		debug_println(9,enabling_relations(OpName1,OpName2,Enable,KeepEnabled,Disable,KeepDisabled)).
251
252		prove_and_assert_enabling_relation(OpName1,OpName2,Enable,KeepEnabled,Disable,KeepDisabled) :-
253		(maplist(nonvar,[Enable,KeepEnabled,Disable,KeepDisabled]) ->
254		assertz(enabling_relations(OpName1,OpName2,Enable,KeepEnabled,Disable,KeepDisabled))
255		; add_warning(cbc_enabling_relation,'A variable result occurred for one of the enabling relations result',
256		[Enable,KeepEnabled,Disable,KeepDisabled])).
257
258
259		my_exit_error_scope(ScopeID) :-
260		(specific_event_occurred_at_level(ScopeID,Event) ->
261		format('### ERROR/ENUMERATION WARING OCCURED : ~w !~n',[Event])),fail.
262		my_exit_error_scope(ScopeID) :- %error_manager:print_error_scopes,
263		clear_all_errors_in_error_scope(ScopeID),
264		exit_error_scope(ScopeID,_,my_exit_error_scope).
265
266		% TODO: consider if we need this at all
267		tcltk_disabling_analysis(list([list(['Origin'|Ops])|Result])) :-
268		get_preference(timeout_cbc_analysis,Timeout),
269		findall(Op, b_top_level_operation(Op), Ops),
270		findall(list([OpName1|DisableList]),
271		(init_or_op(OpName1),
272		findall(Disables,(b_top_level_operation(OpName2),(disables(OpName1,OpName2,1,Timeout) -> Disables=yes; Disables=no)),DisableList)),
273		Result),
274		print_enable_table([list(['Origin'|Ops])|Result]).
275
276		%----------------- Auxiliary predicates for the Partial Guard Evaluation implementation
277
278		:- use_module(probsrc(tcltk_interface),[add_transition/4]).
279		add_transition_timeout(CurID,CurTO,CurState,ActionName,NewId) :-
280		set_error_context(operation(ActionName,CurID)),
281		(CurTO > 0
282	?	-> time_out_with_enum_warning_for_findall(tcltk_interface:add_transition(CurID,CurState,ActionName,NewId),CurTO,TimeOutRes),
283		check_timeout_result(CurID,ActionName,CurTO,TimeOutRes)
284		; add_transition(CurID,CurState,ActionName,NewId)
285		).
286
287		check_timeout_result(CurID,ActionName,CurTO,TimeOutRes) :-
288		(is_time_out_result(TimeOutRes)
289		->
290		( TimeOutRes = virtual_time_out(_) ->
291		true
292		; print_message('TIME OUT: '), print_message(CurID), print_message(CurTO),
293		print_message(ActionName)
294		),
295		(var(ActionName)
296		-> assert_time_out_for_node(CurID,'unspecified_operation',TimeOutRes)
297		; assert_time_out_for_node(CurID,ActionName,TimeOutRes))
298		; true
299		).
300
301		setup_constants_state1(csp_and_b_root) :- !.
302		setup_constants_state1(CurState) :-
303		setup_constants_state(CurState).
304
305		setup_constants_state(concrete_constants(_)).
306		setup_constants_state(const_and_vars(_,_)).
307
308		% failure loop
309		assert_disabled_ops_to_init_states_if_necessary :-
310		\+b_machine_has_constants_or_properties, % we do not want to explore states prior to firing the model checker
311		findall(Op,disables('INITIALISATION',Op),DisabledOps),
312		findall(Op,enables('INITIALISATION',Op),EnabledOps),
313		% init states finds exactly the initial states of the checked machine
314		find_initialised_states(Init),
315		member(I,Init),
316		assertz(disabled_operations(I,DisabledOps,EnabledOps)),
317		fail.
318		assert_disabled_ops_to_init_states_if_necessary.
319
320
321		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
322		%%%%%%%%%%%%%%%%%% State Exploration by means of PGE %%%%%%%%%%%%%%%%%%%%%%%
323		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
324
325		:- use_module(probsrc(tcltk_interface),[catch_clpfd_overflow_call_for_state/4]).
326		compute_transitions_pge(CurID,CurState) :-
327		catch_clpfd_overflow_call_for_state(CurID,'computing transitions for PGE',
328		pge_algo:compute_transitions_pge2(CurID,CurState),
329		clear_context_state).
330		:- public compute_transitions_pge2/2.
331		compute_transitions_pge2(CurID,CurState) :-
332		reset_max_reached,
333		prepare_state_for_specfile_trans(CurState,CurID,PreparedCurState),
334		(use_no_timeout(CurID) ->
335		add_transitions_pge(CurID,PreparedCurState,0)
336		;
337		preferences: preference(time_out,CurTO),
338		add_transitions_pge(CurID,PreparedCurState,CurTO)
339		),
340		(setup_constants_state1(CurState) -> true ; retractall(disabled_operations(CurID,_,_))),
341		debug_println(9,state_has_been_explored(CurID,CurState)),
342		clear_error_context,
343		(max_reached -> assert_max_reached_for_node(CurID),MaxReached=true ; MaxReached=false),
344		(CurID==root -> save_constants(MaxReached) ; add_new_transitions_to_cache(CurID)).
345
346
347		add_transitions_pge(CurID,CurState,CurTO) :-
348		% PossiblyEnActionNames contains all possible actions that are not recognised to be disabled and need to be tested for enabledness
349		get_possible_enabled_trans_names(CurID,CurState,DisabledOperations,EnabledOperations,PossiblyEnActionNames),
350		explore_current_state_pge(PossiblyEnActionNames,CurID,CurState,CurTO,EnabledOperations,Transitions,DisabledActionsNew),
351		list_to_ord_set(DisabledActionsNew,DisabledActionsNewSet),
352		ord_union(DisabledOperations,DisabledActionsNewSet,DisabledActionsAtCurState),
353		maplist(get_first_argument,Transitions,EnabledActions),
354		list_to_ord_set(EnabledActions,EnabledActionsAtCurState),
355		compute_and_update_disabled_enabled_operations(Transitions,DisabledActionsAtCurState,EnabledActionsAtCurState).
356
357		get_possible_enabled_trans_names(CurID,CurState,DisabledOperations,EnabledOperations,PossiblyEnActionNames) :-
358		(disabled_operations(CurID,DisabledOperations,EnabledOperations) -> true; DisabledOperations = [], EnabledOperations = []),
359		get_possible_enabled_trans_names_aux(CurID,CurState,DisabledOperations,PossiblyEnActionNames).
360
361		get_possible_enabled_trans_names_aux(CurID,CurState,DisabledOperations,PossiblyEnActionNames) :-
362		findall(PossibleEnActionName,
363		(specfile_possible_trans_name_for_successors(CurState,PossibleEnActionName),
364		not_a_member_of_disabled(PossibleEnActionName,DisabledOperations)),
365		PossiblyEnActionNames),
366		debug_println(9,skipped_guard_evaluations_at_state(CurID,DisabledOperations)).
367
368		not_a_member_of_disabled(ActionName,DisabledOperations) :-
369		(ord_member(ActionName,DisabledOperations) ->
370		retract(nr_skipped_guard_evaluations(NrDisabled)),
371		NrDisabled1 is NrDisabled + 1,
372		assertz(nr_skipped_guard_evaluations(NrDisabled1)),
373		fail
374		; true).
375
376
377		:- use_module(probsrc(preferences),[temporary_set_preference/3,reset_temporary_preference/2]).
378
379		explore_current_state_pge(ActionNames,CurID,CurState,CurTO,EnabledOperations,Transitions,DisabledActionsNew) :-
380		explore_current_state_pge1(ActionNames,CurID,CurState,CurTO,EnabledOperations,[],Transitions,[],DisabledActionsNew).
381
382		explore_current_state_pge1([],_CurID,_CurState,_CurTO,_EnabledOperations,Transitions,Transitions,DisabledActions,DisabledActions).
383		explore_current_state_pge1([ActionName|R],CurID,CurState,CurTO,EnabledOperations,TransitionsGen,Transitions,DisabledActionsGen,DisabledActions) :-
384		(ord_member(ActionName,EnabledOperations) ->
385		retract(nr_skipped_guard_evaluations(NrDisabled)),
386		NrDisabled1 is NrDisabled +1,
387		assertz(nr_skipped_guard_evaluations(NrDisabled1)),
388		debug_println(9,do_not_evaluate_guard(ActionName)),
389		temporary_set_preference(ltsmin_do_not_evaluate_top_level_guards,full,CHNG)
390		;
391		CHNG=false % so that reset_temporary_preference does nothing
392		),
393		findall(NewId,add_transition_timeout(CurID,CurTO,CurState,ActionName,NewId),NewIds),
394		(NewIds = [] -> % ActionName is disabled at CurState
395		TransitionsGen1 = TransitionsGen,
396		DisabledActionsGen1 = [ActionName|DisabledActionsGen]
397		;
398		TransitionsGen1 = [(ActionName,NewIds)|TransitionsGen],
399		DisabledActionsGen1 = DisabledActionsGen
400		),
401		reset_temporary_preference(ltsmin_do_not_evaluate_top_level_guards,CHNG),
402		explore_current_state_pge1(R,CurID,CurState,CurTO,EnabledOperations,TransitionsGen1,Transitions,DisabledActionsGen1,DisabledActions).
403
404		compute_and_update_disabled_enabled_operations([],_DisabledActionsAtCurState,_EnabledActionsAtCurState).
405		compute_and_update_disabled_enabled_operations([(ActionName,SuccStates)|R],DisabledActionsAtCurState,EnabledActionsAtCurState) :-
406		compute_disabled_operations(ActionName,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateDisabledActions),
407		compute_enabled_operations(ActionName,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateEnabledActions),
408		update_disabled_enabled_operations_l(SuccStates,SuccStateDisabledActions,SuccStateEnabledActions),
409		compute_and_update_disabled_enabled_operations(R,DisabledActionsAtCurState,EnabledActionsAtCurState).
410
411		compute_disabled_operations(ActionName,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateDisabledActions) :-
412		get_preference(pge,Pref),
413		(check_only_enabled(Pref) ->
414		SuccStateDisabledActions = []
415		; compute_disabled_operations_after_state(Pref,ActionName,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateDisabledActions)
416		).
417
418		compute_enabled_operations(ActionName,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateEnabledActions) :-
419		get_preference(pge,Pref),
420		(check_only_disabled(Pref) ->
421		SuccStateEnabledActions = []
422		; compute_enabled_operations_after_state(Pref,ActionName,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateEnabledActions)
423		).
424
425		update_disabled_enabled_operations_l(StateIDs,NewDisabledOperations,NewEnabledOperations) :-
426		maplist(update_disabled_enabled_operations(NewDisabledOperations,NewEnabledOperations),StateIDs).
427
428		update_disabled_enabled_operations(NewDisabledOperations,NewEnabledOperations,StateID) :-
429		(disabled_operations(StateID,DisabledOperations,EnabledOperations) ->
430		ord_union(DisabledOperations,NewDisabledOperations,DisabledOperations1),
431		ord_union(EnabledOperations,NewEnabledOperations,EnabledOperations1),
432		retractall(disabled_operations(StateID,_,_)),
433		assertz(disabled_operations(StateID,DisabledOperations1,EnabledOperations1))
434		;
435		assertz(disabled_operations(StateID,NewDisabledOperations,NewEnabledOperations))
436		).
437
438		compute_disabled_operations_after_state(Pref,OpName1,DisabledActionsAtCurState,_EnabledActionsAtCurState,SuccStateDisabledActions) :-
439		(Pref = disabled; Pref = full),!,
440		findall(OpName2,disables(OpName1,OpName2),ImpossibleEnabled),
441		findall(OpName2,get_disabled_action_by_keep(OpName1,DisabledActionsAtCurState,OpName2),SuccStateDisabledActions1,ImpossibleEnabled),
442		list_to_ord_set(SuccStateDisabledActions1,SuccStateDisabledActions).
443		compute_disabled_operations_after_state(Pref,OpName1,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateDisabledActions) :-
444		(Pref = disabled2; Pref = full2),!,
445		findall(OpName2,(member(OpName2,EnabledActionsAtCurState),enabling_relations(OpName1,OpName2,_,false,_,_)),DisbaledOps1),
446		findall(OpName2,(animation_mode(b),member(OpName2,DisabledActionsAtCurState),enabling_relations(OpName1,OpName2,false,_,_,_)),DisabledOps2,DisbaledOps1),
447		list_to_ord_set(DisabledOps2,SuccStateDisabledActions).
448		compute_disabled_operations_after_state(_Pref,_OpName1,_DisabledActionsAtCurState,_EnabledActionsAtCurState,[]).
449
450		get_disabled_action_by_keep(OpName1,DisabledActionsAtCurState,OpName2) :-
451		animation_mode(b),!, % can be applied only in B mode, for CSP||B is generally not sound
452	?	member(OpName2,DisabledActionsAtCurState),
453		keeps(OpName1,OpName2).
454
455		compute_enabled_operations_after_state(Pref,OpName1,_DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateEnabledActions) :-
456		(Pref = enabled; Pref = full),!,
457		findall(OpName2,enables(OpName1,OpName2),GuaranteedEnabled),
458		findall(OpName2,get_enabled_action_by_keep(OpName1,EnabledActionsAtCurState,OpName2),SuccStateEnabledActions1,GuaranteedEnabled),
459		list_to_ord_set(SuccStateEnabledActions1,SuccStateEnabledActions).
460		compute_enabled_operations_after_state(Pref,OpName1,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateEnabledActions) :-
461		(Pref = enabled2; Pref = full2),!,
462		findall(OpName2,(member(OpName2,EnabledActionsAtCurState),enabling_relations(OpName1,OpName2,_,_,false,_)),EnabledOps1),
463		findall(OpName2,(animation_mode(b),member(OpName2,DisabledActionsAtCurState),enabling_relations(OpName1,OpName2,_,_,_,false)),EnabledOps2,EnabledOps1),
464		list_to_ord_set(EnabledOps2,SuccStateEnabledActions).
465		compute_enabled_operations_after_state(_Pref,_OpName1,_DisabledActionsAtCurState,_EnabledActionsAtCurState,[]).
466
467		get_enabled_action_by_keep(OpName1,EnabledActionsAtCurState,OpName2) :-
468	?	member(OpName2,EnabledActionsAtCurState),
469		keeps(OpName1,OpName2).
470
471		get_first_argument((A,_B),A).
472
473		check_only_disabled(disabled).
474		check_only_disabled(disabled2).
475
476		check_only_enabled(enabled).
477		check_only_enabled(enabled2).
478
479		%------------------------------