1 % (c) 2012-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(ample_sets, [
6 compute_ample_set2/3,
7 clear_dynamic_predicates_for_POR/0,
8 reset_runtime_dynamic_predicates_POR/0, % now done via event-handling
9 stutter_action/1, visible_action/1,check_cycle_proviso/0 % exported for ltl.pl for asserting and retracting stutter/visible actions
10 ]).
11
12 /* SICSTUS Libraries */
13 :- use_module(library(ordsets)).
14 :- use_module(library(random)).
15 :- use_module(library(lists)).
16 :- use_module(library(ugraphs)).
17 %:- use_module(library(timeout)).
18
19 /* B module sources */
20 :- use_module(probsrc(bmachine),[b_get_invariant_from_machine/1,b_operation_preserves_full_invariant/1]).
21 :- use_module(probsrc(bsyntaxtree),[conjunction_to_list/2,occurs_in_expr/2]).
22 :- use_module(probsrc(specfile),[prepare_state_for_specfile_trans/3,
23 specfile_possible_trans_name_for_successors/2,specfile_trans/6]).
24 :- use_module(probsrc(state_space),[visited_expression/2,use_no_timeout/1]).
25
26 /* POR modules */
27 :- use_module(probporsrc(enable_graph)).
28 % --> /* The Static Analysis' module */
29 :- use_module(probporsrc(static_analysis),[enable_graph/1,dependent_act/4]).
30
31 /* Importing predicates for handling the states of a respective B/Event-B machine */
32 :- use_module(probsrc(specfile),[state_corresponds_to_initialised_b_machine/2]).
33 :- use_module(probsrc(store), [empty_state/1]).
34
35 /* Other modules from ProB */
36 :- use_module(probsrc(debug),[debug_println/2]).
37 :- use_module(probsrc(preferences), [get_preference/2]).
38 :- use_module(probsrc(error_manager), [time_out_with_enum_warning_for_findall/3, add_warning/3]).
39
40 % Cosider to remove this import
41 :- use_module(probsrc(b_read_write_info),[b_get_read_write/3]).
42
43 /* Modules and Infos for the code coverage analysis */
44 :- use_module(probsrc(module_information)).
45 :- module_info(group,model_checker).
46 :- module_info(description,'This module contains predictes for partial order reduction using the ample sets\' theory. It is only applicable in B mode (not CSP||B).').
47
48 % Dynamic predicates for keeping track of visible and stutter actions,
49 % as well as of all dependent reations between the actions of the B model
50 :- dynamic stutter_action/1,visible_action/1,enables/2,explored_state/1,check_cycle_proviso/0.
51
52
53 :- public reset_static_dynamic_predicates_POR/0.
54 clear_dynamic_predicates_for_POR :-
55 reset_static_dynamic_predicates_POR,
56 reset_runtime_dynamic_predicates_POR.
57
58 :- use_module(probsrc(eventhandling),[register_event_listener/3]).
59 :- register_event_listener(clear_specification,clear_dynamic_predicates_for_POR,
60 'Reset Ample Sets.').
61 :- register_event_listener(reset_specification,reset_static_dynamic_predicates_POR,
62 'Reset Ample Sets.').
63
64 % predicates that will be asserted once on every loading of the machine
65 reset_static_dynamic_predicates_POR :-
66 retractall(dependent_act(_,_,_,_)),
67 retractall(enable_graph(_)).
68
69 % predicates that will be asserted at runtime
70 reset_runtime_dynamic_predicates_POR :-
71 retractall(stutter_action(_)),
72 retractall(visible_action(_)),
73 retractall(explored_state(_)),
74 retractall(enables(_,_)),
75 retractall(check_cycle_proviso). % used to not track in the enable graph
76
77 /* This implementation of the ample sets approach sastisfies all four conditions of the ample sets theory (not proved yet).
78 The conditions are taken from the book "Principles of Model Checking" written by C.Baier and J.P.Katoen.
79
80 For every state s in the state space, where Act(s) stands for all enabled actions in state s, the following conditions
81 must be satisfied:
82
83 1. Nonemptiness condition (A1) and terminal states
84 (A 1.1) ample(s) <: Act(s) (set equality is possible)
85 (A 1.2) ample(s) = {} <=> Act(s) = {}
86
87 2. Dependency condition
88 (A 2) Let s -a_{1}> s_{1} -a_{2}> ... -a_{n}> s_{n} -a> s' be a finite execution
89 fragment in the original state space. If a depends on ample(s), then a_{i}:ample(s) for some 0<i<=n.
90
91 This condition can be satisfied by the following conditions (Local Criteria):
92 (A 2.1) Any action b: Act(s)\ample(s) is independent of any a:ample(s) (Here we use the dependency graph generated from the Enabling Analysis)
93 (A 2.2) Any disabled action b:Act\en(s) which is dependent on ample(s) cannot become enabled by a possible sequence of actions starting with an action
94 from en(s)\ample(s). (We check this condition by means of using the enable graph generated from the Enabling Analysis)
95
96 Note that determining the local criteria's conditions above is dependent on the formalism on which we are applying the partial order reduction method.
97 The conditions (A 2.1) and (A 2.2) are adjusted to the semantics of the B method/Event-B. For other formalisms such as CSP we will need to define
98 the conditions differently. On the one hand because we cannot use the Constraint Based Checker of ProB (it is not implemented for CSP yet), on the other hand
99 because CSP differs semantically from B/Event-B (the process structure). An idea to apply Partial Order Reduction on CSP is to make the reduction
100 on the CSP operator-level ('|||', [|X|] and so on). For more detailed description of how to apply POR on CSP read the following papers:
101 - H. Wehrheim. Partial order reductions for failure refinement.
102 - J. Sung, Y. Liu and J.S. Dong. Model Checking CSP Revisited: Introducing a Process Analysis Toolkit.
103
104 3. Stutter condition
105 (A 3) If ample(s) /= Act(s) then any action t:ample(s) is a stutter action.
106
107 4. Cycle condition
108 (A 4) For any cycle s_{0}s_{1}...s_{n} in the reduced state space and actions t:Act(s_{i}), for some
109 0 < i <= n, there exists j:{1..n} such that t:ample(s_{j}). (s_{0},...,s_{n} are states)
110
111 */
112
113 % compute_ample_set2(+CurID,+CurState,+POROptions)
114 %
115 % The main predicate for computing ample sets by respecting the four ample set conditions specified above.
116 % A subset of all possible enabled outgoing transitions in CurState will be computed and added to the state space. The predicate is similar
117 % to the compute_all_transitions/2 predicate implemented in tcltk_interface.pl.
118
119 :- use_module(probsrc(succeed_max),[reset_max_reached/0, max_reached/0]).
120 :- use_module(probsrc(state_space),[assert_max_reached_for_node/1]).
121 :- use_module(probsrc(value_persistance),[save_constants/1, add_new_transitions_to_cache/1]).
122
123 % Arguments:
124 % CurID - the current ID of the state.
125 % CurState - the current evaluation of all global variables (and constants) in the machine.
126 % FindInvViolations (obsolete) - possible values 1 (option setted) and 0 (option not setted). Conditions (A 3) and (A 4) checked if check_cycle_proviso/0 is set.
127 % POROptions - the options being set for exploring the state space by means of partial order reduction
128 %
129 compute_ample_set2(CurID,CurState,por(TYPE,UseEnableGraph,Depth,PGE)) :-
130 reset_max_reached,
131 prepare_state_for_specfile_trans(CurState,CurID,PreparedCurState),
132 get_enabled_actions_at_state(CurID,PreparedCurState,TopLevelActions,Transitions,_DisabledTopLevelActions),
133 % we want only unique action names for analyzing and computing of ample sets
134 list_to_ord_set(TopLevelActions,TopLevelActionsSet),
135 % compute a sound ample set from all actions enabled in state CurID
136 compute_ample_actions(CurID,TopLevelActionsSet,por(TYPE,UseEnableGraph,Depth,PGE),AmpleSet),
137 debug_println(20,sets(CurID,allActions(TopLevelActionsSet),ampleSet(AmpleSet))),
138 % mark state as visited (Cycle Condition (A 4))
139 assertz(explored_state(CurID)),
140 ( AmpleSet \= [] ->
141 % compute just the actions from the ample set (case of state space reduction)
142 % AmpleSet is a non-empty subset of enabled(CurID), AmpleSet can be equal to AllEnabledActions
143 add_transitions(AmpleSet,CurID,Transitions,_ActNameSuccessors)
144 ;
145 true /* DEADLOCK */
146 ),
147 (max_reached ->
148 assert_max_reached_for_node(CurID),
149 MaxReached=true
150 ; MaxReached=false
151 ),
152 (CurID==root ->
153 save_constants(MaxReached)
154 ; add_new_transitions_to_cache(CurID)
155 ),!. % once we have computed the ample set in CurState we don't want to backtrack
156
157 % computing a sound ample set of actions.
158 compute_ample_actions(CurID,AllEnabledActions,POROptions,AmpleSet) :-
159 % get_ample_actions/5 call only reasonable to be executed when more than one actions are enabled in CurID
160 (more_than_one_event(AllEnabledActions) ->
161 get_ample_actions(CurID,AllEnabledActions,POROptions,AmpleSet)
162 ;
163 AmpleSet = AllEnabledActions
164 ).
165
166 more_than_one_event(SetOfActions) :-
167 length(SetOfActions,L),L>1.
168
169 /************************** ADD TRANSITIONS (BEGIN) ******************************/
170
171 % +ActNameSuccessors: a list of tuples (Act,SuccIds), where 'SuccIds' is the list of all state ids that are successor states of Act
172 add_transitions(AmpleSet,CurID,Transitions,ActNameSuccessors) :-
173 add_transitions(no,AmpleSet,CurID,Transitions,[],ActNameSuccessors).
174
175 % first argument tests if the state has been fully explored while adding the
176 % ample set transitions to the state space ('yes' means state has been fully explored, so we can stop,
177 % 'no' means that the rest of the ample set transitions should be added to the state space until
178 % no more ample actions in the list or until the state is fully explored)
179 add_transitions(yes,_AmpleSet,_CurID,_Transitions,ActNameSuccessors,ActNameSuccessors).
180 add_transitions(_FullyExplored,[],_CurID,_Transitions,ActNameSuccessors,ActNameSuccessors).
181 add_transitions(no,[ActionName|ActNames],CurID,Transitions,ActNameSuccessorsGen,ActNameSuccessors) :-
182 add_action_name_transitions(Transitions,CurID,ActionName,[],RemTransitions,FullyExplored,ActNameSuccessorsGen,ActNameSuccessorsGen1),
183 add_transitions(FullyExplored,ActNames,CurID,RemTransitions,ActNameSuccessorsGen1,ActNameSuccessors).
184
185 add_action_name_transitions([],_CurID,_ActionName,RemTransitions,RemTransitions,no,ActSuccsGen,ActSuccsGen).
186 add_action_name_transitions([(ActionName1,Transitions)|R],CurID,ActionName,IgnoredActions_so_far,
187 RemTransitions,FullyExplored,ActSuccsGen,ActSuccs) :-
188 (ActionName == ActionName1 ->
189 % in this case we do not need to go through the rest of the transitions list
190 add_action_transitions(ActionName,Transitions,CurID,NewIds),
191 ActSuccsGen1 = [(ActionName,NewIds)|ActSuccsGen],
192 append(IgnoredActions_so_far,R,AllRemainedActions),
193 (cycle_condition_check_positive_l(NewIds) ->
194 debug_println(9,'*********** POSSIBLE CYCLE DETECTED *************'),
195 debug_println(9,computing_all_other_enabled_actions(back_transition(ActionName),AllRemainedActions)),
196 add_all_other_enabled_transitions(AllRemainedActions,CurID,ActSuccsGen1,ActSuccs),
197 RemTransitions=[],
198 FullyExplored = yes
199 ; FullyExplored = no, RemTransitions = AllRemainedActions, ActSuccs=ActSuccsGen1)
200 ;
201 % keeping track of all ignored actions so far, we don't want to go through the same order of actions every time we
202 % want to add a transition from AmpleSet to the state space
203 ord_add_element(IgnoredActions_so_far, (ActionName1,Transitions), IgnoredActions_so_far1),
204 add_action_name_transitions(R,CurID,ActionName,IgnoredActions_so_far1,RemTransitions,FullyExplored,ActSuccsGen,ActSuccs)
205 ).
206
207 % cycle condition A4 check
208 cycle_condition_check_positive_l(NewIds) :-
209 check_cycle_proviso,!,
210 member(NewId,NewIds),
211 nonvar(NewId),
212 explored_state(NewId).
213
214 add_all_other_enabled_transitions([],_CurID,ActSuccsGen,ActSuccsGen).
215 add_all_other_enabled_transitions([(ActionName,Transitions)|R],CurID,ActSuccsGen,ActSuccs) :-
216 add_action_transitions(ActionName,Transitions,CurID,NewIds),
217 ActSuccsGen1 = [(ActionName,NewIds)|ActSuccsGen],
218 add_all_other_enabled_transitions(R,CurID,ActSuccsGen1,ActSuccs).
219
220 add_action_transitions(_ActionName,Transitions,CurID,NewIds) :-
221 findall(NewId,
222 (member((Act,NewExpression,TransInfo,Residue),Transitions),
223 tcltk_interface: add_trans_id_with_infos(CurID,[],Act,NewExpression,Residue,NewId,TransInfo,_)),NewIds).
224
225
226 /************************** ADD TRANSITIONS (END) ******************************/
227
228 /* Auxiliary predicates for getting action names enabled at the current state */
229
230 % getting action names from the action tuples
231 %get_action_names_only(Actions,ActionNames) :-
232 % maplist(get_action_name,Actions,ActionNames).
233 %get_action_name((ActionName,_Representations),ActionName).
234
235 get_enabled_actions_at_state(CurID,CurState,EnabledTopLevelActions,Transitions,DisabledTopLevelActions) :-
236 get_specfile_possible_trans_names(CurID,CurState,TopLevelActions,DisabledOperations),
237 get_enabled_actions_at_state_aux(TopLevelActions,CurID,CurState,EnabledTopLevelActions,Transitions,DisabledOperationsNew),
238 list_to_ord_set(DisabledOperationsNew,DisabledOperationsNewSet),
239 ord_union(DisabledOperations,DisabledOperationsNewSet,DisabledTopLevelActions).
240
241 get_specfile_possible_trans_names(_CurID,CurState,TopLevelActions,DisabledOperations) :-
242 get_specfile_possible_trans_names(CurState,TopLevelActions),
243 DisabledOperations = [].% in case PGE is not on we don't have any information about the disabledness of actions
244
245
246 get_specfile_possible_trans_names(CurState,TopLevelActions) :-
247 findall(ActionName,specfile_possible_trans_name_for_successors(CurState,ActionName),TopLevelActions).
248
249 get_enabled_actions_at_state_aux(TopLevelActions,CurID,CurState,EnabledTopLevelActions,Transitions,DisabledTopLevelActionsNew) :-
250 get_enabled_actions_at_state_aux2(TopLevelActions,CurID,CurState,[],EnabledTopLevelActions,[],Transitions,[],DisabledTopLevelActionsNew).
251
252 get_enabled_actions_at_state_aux2([],_CurID,_CurState,EnabledTopLevelActions,EnabledTopLevelActions,Transitions,Transitions,DisabledNew,DisabledNew).
253 get_enabled_actions_at_state_aux2([TopLevelAction|R],CurID,CurState,EnabledTopLevelActionsGen,EnabledTopLevelActions,TransitionsGen,Transitions,DisabledNewGen,DisabledNew) :-
254 (get_top_level_action_transitions(CurID,CurState,TopLevelAction,ActionTransitionsTuple) ->
255 EnabledTopLevelActionsGen1 = [TopLevelAction|EnabledTopLevelActionsGen],
256 TransitionsGen1 = [ActionTransitionsTuple|TransitionsGen],
257 DisabledNewGen1 = DisabledNewGen
258 ;
259 EnabledTopLevelActionsGen1 = EnabledTopLevelActionsGen,
260 TransitionsGen1 = TransitionsGen,
261 DisabledNewGen1 = [TopLevelAction|DisabledNewGen]
262 ),
263 get_enabled_actions_at_state_aux2(R,CurID,CurState,EnabledTopLevelActionsGen1,EnabledTopLevelActions,TransitionsGen1,Transitions,DisabledNewGen1,DisabledNew).
264
265 get_top_level_action_transitions(CurID,CurState,TopLevelAction,ActionTransitionsTuple) :-
266 findall((Act,NewExpression,TransInf,Residue),
267 specfile_trans_timeout(CurID,CurState,TopLevelAction,Act,NewExpression,TransInf,Residue),
268 Transitions),
269 % in case TopLevelAction is not enabled we do not save the transitions in the list
270 Transitions\=[],
271 ActionTransitionsTuple = (TopLevelAction,Transitions).
272
273 specfile_trans_timeout(CurID,CurState,ActionName,Act,NewExpression,TransInf,Residue) :-
274 (use_no_timeout(CurID) ->
275 specfile_trans(CurState,ActionName,Act,NewExpression,TransInf,Residue)
276 ; preferences:preference(time_out,CurTO),
277 time_out_with_enum_warning_for_findall(specfile_trans(CurState,ActionName,Act,NewExpression,TransInf,Residue),CurTO,TimeOutRes),
278 check_timeout_result(CurID,ActionName,CurTO,TimeOutRes),
279 Residue==[]
280 ).
281
282 :- use_module(probsrc(error_manager),[is_time_out_result/1]).
283 :- use_module(probsrc(state_space),[ assert_time_out_for_node/3]).
284 check_timeout_result(CurID,ActionName,CurTO,TimeOutRes) :-
285 (is_time_out_result(TimeOutRes)
286 ->
287 ( TimeOutRes = virtual_time_out(_) ->
288 true
289 ; print_message('TIME OUT: '), print_message(CurID), print_message(CurTO),
290 print_message(ActionName)
291 ),
292 (var(ActionName)
293 -> assert_time_out_for_node(CurID,'unspecified_operation',TimeOutRes)
294 ; assert_time_out_for_node(CurID,ActionName,TimeOutRes))
295 ; true
296 ).
297
298 /* Auxiliary predicates for getting action names enabled at the curent state */
299 %---------------------------------------------------------------------------------------------------------------------------------
300 /************************** DETERMINING POSSIBLE AMPLE SETS (BEGIN) ******************************/
301
302 /************************** PREDICATES COMPUTING AMPLE SETS WITH RESPECT TO CONDITIONS (A 2) and (A 3) *************************/
303
304 /*
305
306 implementation of the ample-sets approach satisfying the dependency condition (A 2)
307 by using enabling and dependence analysis (see module enabling analysis)
308
309 */
310
311 get_ample_actions(CurID,AllEnabledActions,POROptions,AmpleSet) :-
312 get_preference(por_heur,Pref),
313 get_ample_actions_pref(Pref,CurID,AllEnabledActions,POROptions,AmpleSet).
314
315 get_ample_actions_pref(minimal,CurID,AllEnabledActions,POROptions,AmpleSet) :- !,
316 get_possible_ample_actions_minimal(AllEnabledActions,CurID,AllEnabledActions,POROptions,AmpleSet).
317 get_ample_actions_pref(Pref,CurID,AllEnabledActions,POROptions,AmpleSet) :-
318 get_possible_ample_actions(Pref,AllEnabledActions,CurID,AllEnabledActions,POROptions,AmpleSet).
319
320 get_possible_ample_actions(_Pref,[],_CurID,AllEnabledActions,_POROptions,AllEnabledActions).
321 get_possible_ample_actions(Pref,Actions,CurID,AllEnabledActions,POROptions,AmpleSet) :-
322 % choosing of action for computing a possible ample set for CurID should be random
323 select_enabled_action_pref(Pref,Actions,Act,RemainedActions),
324 (get_valid_ample_set_act(CurID,POROptions,Act,AllEnabledActions,AmpleSet) -> % get ample set satisfying (A 2) and (A 3) i.r.t. Act
325 true
326 ; % search for another valid ample set
327 get_possible_ample_actions(Pref,RemainedActions,CurID,AllEnabledActions,POROptions,AmpleSet)
328 ).
329
330 get_valid_ample_set_act(CurID,POROptions,Act,AllEnabledActions,AmpleSet) :-
331 POROptions = por(ample_sets2,_,_,_),!,
332 %% trying to find an ample set by the closure method
333 get_possible_ample_set_closure(CurID,Act,AllEnabledActions,AmpleSet).
334 get_valid_ample_set_act(CurID,POROptions,Act,AllEnabledActions,AmpleSet) :-
335 get_valid_ample_set_act_normal(CurID,POROptions,Act,AllEnabledActions,AmpleSet).
336
337 get_valid_ample_set_act_normal(CurID,POROptions,Act,AllEnabledActions,AmpleSet) :-
338 % finding a set (DepActs) satisfying (A 2.1) // there is only one possible set, do not recall here
339 get_dependent_actions(CurID,POROptions,Act,AllEnabledActions,DepActs,IndActs),!,
340 ( (is_enabling_dependency_condition_satisfied(IndActs,DepActs,AllEnabledActions,CurID,POROptions), % check whether DepActs satisfies (A 2.2)
341 check_stutter_condition(DepActs,AllEnabledActions)) % checking (A 3)
342 -> AmpleSet = DepActs
343 ; fail). % should fail in order to try to get another valid ample set
344
345 select_enabled_action_pref(random,Actions,Act,RemainedActions):- !,
346 random_select(Act,Actions,RemainedActions).
347 select_enabled_action_pref(first,[Act|RemainedActions],Act,RemainedActions):- !.
348 select_enabled_action_pref(Pref,Actions,Act,RemainedActions) :-
349 add_warning(ample_sets,'Unknown preference for choosing an action from the set of enabled actions: ', Pref),
350 random_select(Act,Actions,RemainedActions). % choose the default option for choosing an action
351
352 check_stutter_condition(AmpleSet,AllEnabledActions) :-
353 \+ ord_seteq(AmpleSet,AllEnabledActions),!,
354 check_cycle_proviso(AmpleSet).
355
356 % this actually checks condition A3 not the cycle condition A4:
357 check_cycle_proviso(AmpleSet) :-
358 % in case that we don't check for invariant violations, we don't have to prove the stuttering condition for AmpleSet
359 (check_cycle_proviso % true when we search for invariant violations
360 -> stutter_actions(AmpleSet)
361 ; true).
362
363 get_possible_ample_actions_minimal(AllEnabledActions,CurID,AllEnabledActions,POROptions,AmpleSet) :-
364 maplist(get_valid_ample_set_act_nonfail(CurID,AllEnabledActions,POROptions),AllEnabledActions,AmpleSets),
365 get_minimal_set(AmpleSets,AmpleSet),
366 debug_println(9,minimal_ample_set(AmpleSet,AmpleSets)).
367
368 get_minimal_set([AmpleSet|Rest],MinAmpleSet) :-
369 length(AmpleSet,Length),
370 get_minimal_set_length(Length,AmpleSet,Rest,MinAmpleSet).
371
372 get_minimal_set_length(1,AmpleSet,_Rest,AmpleSet).
373 get_minimal_set_length(_Length,AmpleSet,[],AmpleSet).
374 get_minimal_set_length(Length,AmpleSet,[AmpleSet2|Rest],MinAmpleSet) :-
375 length(AmpleSet2,Length2),
376 (Length2<Length ->
377 get_minimal_set_length(Length2,AmpleSet2,Rest,MinAmpleSet)
378 ;
379 get_minimal_set_length(Length,AmpleSet,Rest,MinAmpleSet)).
380
381 get_valid_ample_set_act_nonfail(CurID,AllEnabledActions,POROptions,Act,AmpleSet) :-
382 (get_valid_ample_set_act(CurID,POROptions,Act,AllEnabledActions,AmpleSet)
383 -> true
384 ; AmpleSet = AllEnabledActions).
385
386 %%%%%% the closure method for computing ample sets %%%%%%
387 get_possible_ample_set_closure(CurID,Act,AllEnabledActions,AmpleSet) :-
388 get_valid_ample_set_act_closure(CurID,Act,AllEnabledActions,AmpleSet),!,
389 check_stutter_condition(AmpleSet,AllEnabledActions). % checking (A 3)
390
391 get_valid_ample_set_act_closure(CurID,Act,AllEnabledActions,AmpleSet) :-
392 %(length(AllEnabledActions,3) -> trace;true),
393 list_to_ord_set([Act],WorkSet),
394 list_to_ord_set([],ClosureSet),
395 compute_closure_set(WorkSet,CurID,ClosureSet,AllEnabledActions,Result),
396 ord_intersection(Result,AllEnabledActions,AmpleSet).
397
398 compute_closure_set([],_CurID,ClosureSet,_AllEnabledActions,ClosureSet).
399 compute_closure_set([Act|Acts],CurID,ClosureSet,AllEnabledActions,Result) :-
400 ord_add_element(ClosureSet,Act,ClosureSet1),
401 get_new_work_set(Act,Acts,CurID,AllEnabledActions,ClosureSet1,NewWorkSet),
402 compute_closure_set(NewWorkSet,CurID,ClosureSet1,AllEnabledActions,Result).
403
404 get_new_work_set(Act,WorkSet,CurID,AllEnabledActions,ClosureSet1,NewWorkSet) :-
405 ord_member(Act,AllEnabledActions),!,
406 get_dependency_set_closure(Act,WorkSet,CurID,ClosureSet1,NewWorkSet).
407 get_new_work_set(Act,WorkSet,CurID,AllEnabledActions,ClosureSet1,NewWorkSet) :-
408 get_enabling_set_for_act(Act,WorkSet,CurID,AllEnabledActions,ClosureSet1,NewWorkSet).
409
410 get_dependency_set_closure(Act,WorkSet,CurID,ClosureSet1,NewWorkSet) :-
411 findall(Act1,(is_dependent_to_and_coenabled(Act,Act1,CurID),ord_nonmember(Act1,ClosureSet1)),NewActions),
412 list_to_ord_set(NewActions,NewActionsSet),
413 ord_union(WorkSet,NewActionsSet,NewWorkSet).
414
415 get_enabling_set_for_act(Act,WorkSet,CurID,AllEnabledActions,ClosureSet1,NewWorkSet) :-
416 % Act is disabled at current state
417 findall(Act1,find_enabling_action(Act,CurID,AllEnabledActions,ClosureSet1,Act1),NewActions),
418 list_to_ord_set(NewActions,NewActionsSet),
419 ord_union(WorkSet,NewActionsSet,NewWorkSet).
420
421 find_enabling_action(Act,CurID,AllEnabledActions,ClosureSet,Act1) :-
422 member(Act1,AllEnabledActions),
423 ord_nonmember(Act1,ClosureSet),
424 can_enable_certain_action(Act1,Act,CurID).
425
426 can_enable_certain_action(Act,ActionToBeEnabled,CurID) :-
427 ( enables(Act,ActionToBeEnabled) ->
428 debug_println(9,enables(Act,ActionToBeEnabled))
429 ;
430 enable_graph(EnableGraph),
431 min_path(Act,ActionToBeEnabled,EnableGraph,P,L),
432 debug_print_path(CurID,P,L),
433 assertz(enables(Act,ActionToBeEnabled))).
434
435 % get_dependent_actions(+CurID,+POROptions,+Act,+AllEnabledActions,+EnGraph,-DepActs)
436 % CurID - the ID of the current state (used here only for debugging purposes)
437 % POROptions - partial order reduction options (e.g. UseEnableGraph, Depth)
438 % Act - the action with which the current dependency class will be computed
439 % AllEnabledActions - the set of all in CurID enabled actions and it is an ordinary set
440 % DepActs - the computed candidate for ample set
441 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
442 % EnableGraph - the enable graph for all possible enable actions' relations in the current machine. The enable graph will
443 % be computed only single time (before starting with the verification of the state space).
444
445 get_dependent_actions(CurID,_POROptions,Act,AllEnabledActions,DepActs,IndActions) :-
446 % finding all dependent actions to Act (A 2.1)
447 get_dependency_set(Act,AllEnabledActions,CurID,DepActs),
448 ord_subtract(AllEnabledActions,DepActs,IndActions).
449
450 is_enabling_dependency_condition_satisfied([],_DepActs,_AllEnabledActions,_CurID,_POROptions) :- !,fail.
451 is_enabling_dependency_condition_satisfied(IndActs,DepActs,AllEnabledActions,CurID,POROptions) :-
452 enable_graph(EnableGraph),
453 vertices(EnableGraph,Vertices), % getting all possible actions that can be enabled
454 % DisabledActions = Vertices\AllEnabledActions
455 ord_subtract(Vertices,AllEnabledActions,DisabledActions),
456 % searching for an independent action to Act that could enable a currently disabled action that is dependent to Act (A 2.2)
457 \+may_enable_dep_action_list(IndActs,DepActs,DisabledActions,EnableGraph,CurID,POROptions).
458
459 may_enable_dep_action_list(IndActs,DepActs,DisabledActions,EnableGraph,CurID,POROptions) :-
460 member(Act2,IndActs),
461 may_enable_dep_action(Act2,DepActs,DisabledActions,EnableGraph,CurID,POROptions).
462
463
464 get_dependency_set(Act,AllEnabledActions,CurID,DepActions_so_far) :-
465 vertices_edges_to_ugraph([],[],G),
466 get_dependency_tuples_converted_to_edges(Act,AllEnabledActions,RestEnabledActions,CurID,Edges),
467 add_edges(G,Edges,G1),
468 get_dependency_set1(Act,G1,[],RestEnabledActions,CurID,DepActions_so_far).
469
470 get_dependency_tuples_converted_to_edges(Act,AllEnabledActions,RestEnabledActions,CurID,Res) :-
471 findall(Act1,(member(Act1,AllEnabledActions), is_dependent_to(Act,Act1,CurID)),DepActs),
472 findall([Act-Act1,Act1-Act],member(Act1,DepActs),Edges),
473 ord_subtract(AllEnabledActions,DepActs,RestEnabledActions),
474 append(Edges,Res).
475
476 get_dependency_set1(Act,G,G,_Actions,_CurID,Res) :-
477 reachable(Act,G,Res).
478 get_dependency_set1(Act,G,_GPrime,Actions,CurID,Res) :-
479 GPrime1 = G,
480 vertices(G,Vertices),
481 findall([V-Act1,Act1-V],(member(Act1,Actions),member(V,Vertices),is_dependent_to(V,Act1,CurID)),NewEdges),
482 append(NewEdges,NewEdges1),
483 add_edges(G,NewEdges1,G1),vertices(G1,Vertices1),
484 ord_subtract(Actions,Vertices1,Actions1),
485 get_dependency_set1(Act,G1,GPrime1,Actions1,CurID,Res).
486
487 is_dependent_to(Act,Act1,CurID) :-
488 (dependent_act(Act,Act1,Status,_Coenabled) ->
489 (Status=predicate(Pred) -> check_enable_dependency(Act,Act1,Pred,CurID); true)
490 ;
491 fail
492 ).
493
494 is_dependent_to_and_coenabled(Act,Act1,CurID) :-
495 dependent_act(Act,Act1,Status,true),
496 (Status=predicate(Pred) -> check_enable_dependency(Act,Act1,Pred,CurID); true).
497
498 check_enable_dependency(Act,Act1,Pred,CurID) :-
499 debug_println(9,checking_guard_dependency(Act,Act1,Pred)),
500 visited_expression(CurID,RawState),
501 state_corresponds_to_initialised_b_machine(RawState,State),
502 empty_state(LocalState),
503 % if the enable predicate Pred evaluates to false we know that (Act,Act1) is a dependent pair
504 \+ b_interpreter:b_test_boolean_expression_cs(Pred,LocalState,State,'enable dependency',Act:Act1).
505
506 /* searching for enabling path beginning from an action which is not from AmpleSet and
507 which enables action dependent on AmpleSet */
508 may_enable_dep_action(Act,AmpleSet,DisabledActions,EnableGraph,CurID,por(_TYPE,UseEnableGraph,Depth,_PGE)) :-
509 ( UseEnableGraph = true ->
510 check_enabling_path(CurID,Act,DisabledActions,AmpleSet,EnableGraph,Depth)
511 ;
512 member(DisAct,DisabledActions),
513 % we check here only currently disabled actions dependent on AmpleSet that can be enabled later
514 depends_on_ample_set_and_coenabled(DisAct,AmpleSet,_DepAct),
515 % is there a path that can enable Act1, which is dependent on Act
516 enables_action(CurID,Act,DisAct,AmpleSet,EnableGraph)
517 ),
518 !.
519
520 enables_action(CurID,Act,DisAct,AmpleSet,EnableGraph) :-
521 ( enables(Act,DisAct) ->
522 % should improve performance a little bit (not applicable when using enable graphs)
523 debug_println(9,enables(Act,DisAct))
524 ; check_if_enabled(CurID,Act,DisAct,AmpleSet,EnableGraph) ->
525 true
526 ;
527 fail
528 ).
529
530 check_if_enabled(CurID,Act,DisAct,AmpleSet,EnableGraph) :-
531 min_path(Act,DisAct,EnableGraph,P,L),
532 sets_disjoint(AmpleSet,P),
533 debug_print_path(CurID,P,L),
534 assertz(enables(Act,DisAct)).
535
536 % predicates used for the enable graph feature
537 check_enabling_path(CurID,Act,DisabledActions,AmpleSet,EnableGraph,Depth) :-
538 findall(DepDisAct,(member(DepDisAct,DisabledActions),depends_on_ample_set_and_coenabled(DepDisAct,AmpleSet,_Act)),DependentDisabledActions),
539 ( DependentDisabledActions = [] ->
540 fail % in this case we know that no action dependent on AmpleSet can be enabled after executing Act
541 ;
542 enables_pred_action1(Act,DependentDisabledActions,AmpleSet,CurID,EnableGraph,Depth)).
543
544 enables_pred_action1(Act,DepDisActs,AmpleSet,CurID,EnableGraph,Depth) :-
545 % visited_expression/2 and state_corresponds_to_initialised_b_machine/2 should be called once for each state,
546 % avoid multiple calls per state
547 (Depth==0 ->
548 empty_state(ST)
549 ;
550 visited_expression(CurID,RawState),
551 state_corresponds_to_initialised_b_machine(RawState,ST)
552 ),
553 %Pred =.. [evaluate_enabling_predicate_for_por, ST, AmpleSet],
554 enable_graph: path_set(EnableGraph,Act,DepDisActs,enable_graph,
555 evaluate_enabling_predicate_for_por(ST,AmpleSet),Depth,Path,Length),
556 debug_print_path(CurID,Path,Length).
557
558 % guaranteeing that the dependent action to AmpleSet has been enabled from an action off AmpleSet
559 sets_disjoint(AmpleSet,Path) :-
560 list_to_ord_set(Path,OrdSet),
561 \+ord_intersection(AmpleSet,OrdSet).
562
563 depends_on_ample_set_and_coenabled(Act,AmpleSet,Act1) :-
564 member(Act1,AmpleSet),
565 dependent_act(Act,Act1,_Status,Coenabled),
566 Coenabled==true.
567
568 debug_print_path(CurID,Path,Length) :-
569 debug_println(20,'***** Enable Path *****'),
570 debug_println(20,path(CurID,Path,Length)),
571 debug_println(20,'***********************').
572
573 /************************** DETERMINING POSSIBLE AMPLE SETS (END) ******************************/
574
575 /************************** CHECKING IF ALL ACTIONS FROM AMPLE SET ARE STUTTER ACTIONS (BEGIN) WITH REGARD TO THE INVARIANT ******************************/
576 /************************** PREDICATES WHICH SATISFY CONDITION (A3) ******************************/
577
578 stutter_actions(Actions) :-
579 maplist(is_stutter_action,Actions).
580
581 % visible actions are non stutter actions
582 is_stutter_action(Act) :-
583 ( stutter_action(Act) ->
584 debug_println(19,stutter_action(Act))
585 ; visible_action(Act) ->
586 debug_println(19,visible_action(Act)),
587 fail
588 ;
589 check_if_action_is_stutter_wrt_inv(Act)
590 ).
591
592 % A stutter action
593 % * either cannot change the current invariant value or
594 % * if it violates the invariant then no independent action can undo the change
595 % That's why we must check if the particular action preserves
596 % the full invariant in order to determine if the action is
597 % stutter under the following LTL formula:
598 % G Phi, where Phi is the invariant.
599 check_if_action_is_stutter_wrt_inv(Act) :- %print(check_stutter(Act)),nl,
600 b_operation_preserves_full_invariant(Act),!,
601 assertz(stutter_action(Act)),
602 debug_println(19,stutter_according_to_proof_info(Act)).
603 check_if_action_is_stutter_wrt_inv(Act) :-
604 b_specialized_invariant_for_op(Act,Invariant), %translate:print_bexpr(Invariant),nl,
605 conjunction_to_list(Invariant,Conjunctions), % getting all conjunctions from the invariant
606 b_get_read_write(Act,_Reads,Writes), % print(writes(Act,Writes)),nl,
607 ( action_does_not_modify_inv_or_inv_cannot_be_repaired(Writes,Conjunctions)
608 -> assertz(stutter_action(Act)),
609 debug_println(19,stutter_or_not_repairable(Act))
610 ; assertz(visible_action(Act)),fail
611 ).
612
613 :- use_module(probsrc(bsyntaxtree),[find_identifier_uses/3]).
614 :- use_module(probsrc(bmachine),[b_specialized_invariant_for_op/2]).
615 % either an action does not affect an invariant or it writes *all* variables of an invariant
616 % TODO: a third option would be if no other independent event modifies the variable of this invariant
617 % one could even look whether any (enabled) event in the ample set modifies the given conjunct
618 % For example if we modify x and invariant is x<y, but if no other enabled event modifies x,y we are fine
619 action_does_not_modify_inv_or_inv_cannot_be_repaired(_Vars,[]).
620 action_does_not_modify_inv_or_inv_cannot_be_repaired(Vars,[Conj|Conjs]) :-
621 find_identifier_uses(Conj,[],UsedIds),
622 ord_intersection(UsedIds,Vars,Common),
623 (Common=[]
624 -> true % invariant not affected by action
625 ; ord_seteq(Common,UsedIds) % we write all variables of an invariant; no independent action can change/repair its status
626 ),
627 action_does_not_modify_inv_or_inv_cannot_be_repaired(Vars,Conjs).
628
629
630
631 /************************** CHECKING IF ALL ACTIONS FROM AMPLE SET ARE STUTTER ACTIONS (END) ******************************/