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 :- use_module(probsrc(tools), [print_message/1]).
285 check_timeout_result(CurID,ActionName,CurTO,TimeOutRes) :-
286 (is_time_out_result(TimeOutRes)
287 ->
288 ( TimeOutRes = virtual_time_out(_) ->
289 true
290 ; print_message('TIME OUT: '), print_message(CurID), print_message(CurTO),
291 print_message(ActionName)
292 ),
293 (var(ActionName)
294 -> assert_time_out_for_node(CurID,'unspecified_operation',TimeOutRes)
295 ; assert_time_out_for_node(CurID,ActionName,TimeOutRes))
296 ; true
297 ).
298
299 /* Auxiliary predicates for getting action names enabled at the curent state */
300 %---------------------------------------------------------------------------------------------------------------------------------
301 /************************** DETERMINING POSSIBLE AMPLE SETS (BEGIN) ******************************/
302
303 /************************** PREDICATES COMPUTING AMPLE SETS WITH RESPECT TO CONDITIONS (A 2) and (A 3) *************************/
304
305 /*
306
307 implementation of the ample-sets approach satisfying the dependency condition (A 2)
308 by using enabling and dependence analysis (see module enabling analysis)
309
310 */
311
312 get_ample_actions(CurID,AllEnabledActions,POROptions,AmpleSet) :-
313 get_preference(por_heur,Pref),
314 ? get_ample_actions_pref(Pref,CurID,AllEnabledActions,POROptions,AmpleSet).
315
316 get_ample_actions_pref(minimal,CurID,AllEnabledActions,POROptions,AmpleSet) :- !,
317 get_possible_ample_actions_minimal(AllEnabledActions,CurID,AllEnabledActions,POROptions,AmpleSet).
318 get_ample_actions_pref(Pref,CurID,AllEnabledActions,POROptions,AmpleSet) :-
319 ? get_possible_ample_actions(Pref,AllEnabledActions,CurID,AllEnabledActions,POROptions,AmpleSet).
320
321 get_possible_ample_actions(_Pref,[],_CurID,AllEnabledActions,_POROptions,AllEnabledActions).
322 get_possible_ample_actions(Pref,Actions,CurID,AllEnabledActions,POROptions,AmpleSet) :-
323 % choosing of action for computing a possible ample set for CurID should be random
324 select_enabled_action_pref(Pref,Actions,Act,RemainedActions),
325 (get_valid_ample_set_act(CurID,POROptions,Act,AllEnabledActions,AmpleSet) -> % get ample set satisfying (A 2) and (A 3) i.r.t. Act
326 true
327 ; % search for another valid ample set
328 ? get_possible_ample_actions(Pref,RemainedActions,CurID,AllEnabledActions,POROptions,AmpleSet)
329 ).
330
331 get_valid_ample_set_act(CurID,POROptions,Act,AllEnabledActions,AmpleSet) :-
332 POROptions = por(ample_sets2,_,_,_),!,
333 %% trying to find an ample set by the closure method
334 get_possible_ample_set_closure(CurID,Act,AllEnabledActions,AmpleSet).
335 get_valid_ample_set_act(CurID,POROptions,Act,AllEnabledActions,AmpleSet) :-
336 get_valid_ample_set_act_normal(CurID,POROptions,Act,AllEnabledActions,AmpleSet).
337
338 get_valid_ample_set_act_normal(CurID,POROptions,Act,AllEnabledActions,AmpleSet) :-
339 % finding a set (DepActs) satisfying (A 2.1) // there is only one possible set, do not recall here
340 ? get_dependent_actions(CurID,POROptions,Act,AllEnabledActions,DepActs,IndActs),!,
341 ( (is_enabling_dependency_condition_satisfied(IndActs,DepActs,AllEnabledActions,CurID,POROptions), % check whether DepActs satisfies (A 2.2)
342 check_stutter_condition(DepActs,AllEnabledActions)) % checking (A 3)
343 -> AmpleSet = DepActs
344 ; fail). % should fail in order to try to get another valid ample set
345
346 select_enabled_action_pref(random,Actions,Act,RemainedActions):- !,
347 random_select(Act,Actions,RemainedActions).
348 select_enabled_action_pref(first,[Act|RemainedActions],Act,RemainedActions):- !.
349 select_enabled_action_pref(Pref,Actions,Act,RemainedActions) :-
350 add_warning(ample_sets,'Unknown preference for choosing an action from the set of enabled actions: ', Pref),
351 random_select(Act,Actions,RemainedActions). % choose the default option for choosing an action
352
353 check_stutter_condition(AmpleSet,AllEnabledActions) :-
354 \+ ord_seteq(AmpleSet,AllEnabledActions),!,
355 check_cycle_proviso(AmpleSet).
356
357 % this actually checks condition A3 not the cycle condition A4:
358 check_cycle_proviso(AmpleSet) :-
359 % in case that we don't check for invariant violations, we don't have to prove the stuttering condition for AmpleSet
360 (check_cycle_proviso % true when we search for invariant violations
361 -> stutter_actions(AmpleSet)
362 ; true).
363
364 get_possible_ample_actions_minimal(AllEnabledActions,CurID,AllEnabledActions,POROptions,AmpleSet) :-
365 maplist(get_valid_ample_set_act_nonfail(CurID,AllEnabledActions,POROptions),AllEnabledActions,AmpleSets),
366 get_minimal_set(AmpleSets,AmpleSet),
367 debug_println(9,minimal_ample_set(AmpleSet,AmpleSets)).
368
369 get_minimal_set([AmpleSet|Rest],MinAmpleSet) :-
370 length(AmpleSet,Length),
371 get_minimal_set_length(Length,AmpleSet,Rest,MinAmpleSet).
372
373 get_minimal_set_length(1,AmpleSet,_Rest,AmpleSet).
374 get_minimal_set_length(_Length,AmpleSet,[],AmpleSet).
375 get_minimal_set_length(Length,AmpleSet,[AmpleSet2|Rest],MinAmpleSet) :-
376 length(AmpleSet2,Length2),
377 (Length2<Length ->
378 get_minimal_set_length(Length2,AmpleSet2,Rest,MinAmpleSet)
379 ;
380 get_minimal_set_length(Length,AmpleSet,Rest,MinAmpleSet)).
381
382 get_valid_ample_set_act_nonfail(CurID,AllEnabledActions,POROptions,Act,AmpleSet) :-
383 (get_valid_ample_set_act(CurID,POROptions,Act,AllEnabledActions,AmpleSet)
384 -> true
385 ; AmpleSet = AllEnabledActions).
386
387 %%%%%% the closure method for computing ample sets %%%%%%
388 get_possible_ample_set_closure(CurID,Act,AllEnabledActions,AmpleSet) :-
389 get_valid_ample_set_act_closure(CurID,Act,AllEnabledActions,AmpleSet),!,
390 check_stutter_condition(AmpleSet,AllEnabledActions). % checking (A 3)
391
392 get_valid_ample_set_act_closure(CurID,Act,AllEnabledActions,AmpleSet) :-
393 %(length(AllEnabledActions,3) -> trace;true),
394 list_to_ord_set([Act],WorkSet),
395 list_to_ord_set([],ClosureSet),
396 compute_closure_set(WorkSet,CurID,ClosureSet,AllEnabledActions,Result),
397 ord_intersection(Result,AllEnabledActions,AmpleSet).
398
399 compute_closure_set([],_CurID,ClosureSet,_AllEnabledActions,ClosureSet).
400 compute_closure_set([Act|Acts],CurID,ClosureSet,AllEnabledActions,Result) :-
401 ord_add_element(ClosureSet,Act,ClosureSet1),
402 get_new_work_set(Act,Acts,CurID,AllEnabledActions,ClosureSet1,NewWorkSet),
403 compute_closure_set(NewWorkSet,CurID,ClosureSet1,AllEnabledActions,Result).
404
405 get_new_work_set(Act,WorkSet,CurID,AllEnabledActions,ClosureSet1,NewWorkSet) :-
406 ord_member(Act,AllEnabledActions),!,
407 get_dependency_set_closure(Act,WorkSet,CurID,ClosureSet1,NewWorkSet).
408 get_new_work_set(Act,WorkSet,CurID,AllEnabledActions,ClosureSet1,NewWorkSet) :-
409 get_enabling_set_for_act(Act,WorkSet,CurID,AllEnabledActions,ClosureSet1,NewWorkSet).
410
411 get_dependency_set_closure(Act,WorkSet,CurID,ClosureSet1,NewWorkSet) :-
412 findall(Act1,(is_dependent_to_and_coenabled(Act,Act1,CurID),ord_nonmember(Act1,ClosureSet1)),NewActions),
413 list_to_ord_set(NewActions,NewActionsSet),
414 ord_union(WorkSet,NewActionsSet,NewWorkSet).
415
416 get_enabling_set_for_act(Act,WorkSet,CurID,AllEnabledActions,ClosureSet1,NewWorkSet) :-
417 % Act is disabled at current state
418 findall(Act1,find_enabling_action(Act,CurID,AllEnabledActions,ClosureSet1,Act1),NewActions),
419 list_to_ord_set(NewActions,NewActionsSet),
420 ord_union(WorkSet,NewActionsSet,NewWorkSet).
421
422 find_enabling_action(Act,CurID,AllEnabledActions,ClosureSet,Act1) :-
423 member(Act1,AllEnabledActions),
424 ord_nonmember(Act1,ClosureSet),
425 can_enable_certain_action(Act1,Act,CurID).
426
427 can_enable_certain_action(Act,ActionToBeEnabled,CurID) :-
428 ( enables(Act,ActionToBeEnabled) ->
429 debug_println(9,enables(Act,ActionToBeEnabled))
430 ;
431 enable_graph(EnableGraph),
432 min_path(Act,ActionToBeEnabled,EnableGraph,P,L),
433 debug_print_path(CurID,P,L),
434 assertz(enables(Act,ActionToBeEnabled))).
435
436 % get_dependent_actions(+CurID,+POROptions,+Act,+AllEnabledActions,+EnGraph,-DepActs)
437 % CurID - the ID of the current state (used here only for debugging purposes)
438 % POROptions - partial order reduction options (e.g. UseEnableGraph, Depth)
439 % Act - the action with which the current dependency class will be computed
440 % AllEnabledActions - the set of all in CurID enabled actions and it is an ordinary set
441 % DepActs - the computed candidate for ample set
442 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
443 % EnableGraph - the enable graph for all possible enable actions' relations in the current machine. The enable graph will
444 % be computed only single time (before starting with the verification of the state space).
445
446 get_dependent_actions(CurID,_POROptions,Act,AllEnabledActions,DepActs,IndActions) :-
447 % finding all dependent actions to Act (A 2.1)
448 ? get_dependency_set(Act,AllEnabledActions,CurID,DepActs),
449 ord_subtract(AllEnabledActions,DepActs,IndActions).
450
451 is_enabling_dependency_condition_satisfied([],_DepActs,_AllEnabledActions,_CurID,_POROptions) :- !,fail.
452 is_enabling_dependency_condition_satisfied(IndActs,DepActs,AllEnabledActions,CurID,POROptions) :-
453 enable_graph(EnableGraph),
454 vertices(EnableGraph,Vertices), % getting all possible actions that can be enabled
455 % DisabledActions = Vertices\AllEnabledActions
456 ord_subtract(Vertices,AllEnabledActions,DisabledActions),
457 % searching for an independent action to Act that could enable a currently disabled action that is dependent to Act (A 2.2)
458 ? \+may_enable_dep_action_list(IndActs,DepActs,DisabledActions,EnableGraph,CurID,POROptions).
459
460 may_enable_dep_action_list(IndActs,DepActs,DisabledActions,EnableGraph,CurID,POROptions) :-
461 ? member(Act2,IndActs),
462 may_enable_dep_action(Act2,DepActs,DisabledActions,EnableGraph,CurID,POROptions).
463
464
465 get_dependency_set(Act,AllEnabledActions,CurID,DepActions_so_far) :-
466 vertices_edges_to_ugraph([],[],G),
467 get_dependency_tuples_converted_to_edges(Act,AllEnabledActions,RestEnabledActions,CurID,Edges),
468 add_edges(G,Edges,G1),
469 ? get_dependency_set1(Act,G1,[],RestEnabledActions,CurID,DepActions_so_far).
470
471 get_dependency_tuples_converted_to_edges(Act,AllEnabledActions,RestEnabledActions,CurID,Res) :-
472 findall(Act1,(member(Act1,AllEnabledActions), is_dependent_to(Act,Act1,CurID)),DepActs),
473 findall([Act-Act1,Act1-Act],member(Act1,DepActs),Edges),
474 ord_subtract(AllEnabledActions,DepActs,RestEnabledActions),
475 append(Edges,Res).
476
477 get_dependency_set1(Act,G,G,_Actions,_CurID,Res) :-
478 reachable(Act,G,Res).
479 get_dependency_set1(Act,G,_GPrime,Actions,CurID,Res) :-
480 GPrime1 = G,
481 vertices(G,Vertices),
482 findall([V-Act1,Act1-V],(member(Act1,Actions),member(V,Vertices),is_dependent_to(V,Act1,CurID)),NewEdges),
483 append(NewEdges,NewEdges1),
484 add_edges(G,NewEdges1,G1),vertices(G1,Vertices1),
485 ord_subtract(Actions,Vertices1,Actions1),
486 ? get_dependency_set1(Act,G1,GPrime1,Actions1,CurID,Res).
487
488 is_dependent_to(Act,Act1,CurID) :-
489 (dependent_act(Act,Act1,Status,_Coenabled) ->
490 (Status=predicate(Pred) -> check_enable_dependency(Act,Act1,Pred,CurID); true)
491 ;
492 fail
493 ).
494
495 is_dependent_to_and_coenabled(Act,Act1,CurID) :-
496 dependent_act(Act,Act1,Status,true),
497 (Status=predicate(Pred) -> check_enable_dependency(Act,Act1,Pred,CurID); true).
498
499 check_enable_dependency(Act,Act1,Pred,CurID) :-
500 debug_println(9,checking_guard_dependency(Act,Act1,Pred)),
501 visited_expression(CurID,RawState),
502 state_corresponds_to_initialised_b_machine(RawState,State),
503 empty_state(LocalState),
504 % if the enable predicate Pred evaluates to false we know that (Act,Act1) is a dependent pair
505 \+ b_interpreter:b_test_boolean_expression_cs(Pred,LocalState,State,'enable dependency',Act:Act1).
506
507 /* searching for enabling path beginning from an action which is not from AmpleSet and
508 which enables action dependent on AmpleSet */
509 may_enable_dep_action(Act,AmpleSet,DisabledActions,EnableGraph,CurID,por(_TYPE,UseEnableGraph,Depth,_PGE)) :-
510 ( UseEnableGraph = true ->
511 check_enabling_path(CurID,Act,DisabledActions,AmpleSet,EnableGraph,Depth)
512 ;
513 ? member(DisAct,DisabledActions),
514 % we check here only currently disabled actions dependent on AmpleSet that can be enabled later
515 ? depends_on_ample_set_and_coenabled(DisAct,AmpleSet,_DepAct),
516 % is there a path that can enable Act1, which is dependent on Act
517 enables_action(CurID,Act,DisAct,AmpleSet,EnableGraph)
518 ),
519 !.
520
521 enables_action(CurID,Act,DisAct,AmpleSet,EnableGraph) :-
522 ( enables(Act,DisAct) ->
523 % should improve performance a little bit (not applicable when using enable graphs)
524 debug_println(9,enables(Act,DisAct))
525 ; check_if_enabled(CurID,Act,DisAct,AmpleSet,EnableGraph) ->
526 true
527 ;
528 fail
529 ).
530
531 check_if_enabled(CurID,Act,DisAct,AmpleSet,EnableGraph) :-
532 min_path(Act,DisAct,EnableGraph,P,L),
533 sets_disjoint(AmpleSet,P),
534 debug_print_path(CurID,P,L),
535 assertz(enables(Act,DisAct)).
536
537 % predicates used for the enable graph feature
538 check_enabling_path(CurID,Act,DisabledActions,AmpleSet,EnableGraph,Depth) :-
539 findall(DepDisAct,(member(DepDisAct,DisabledActions),depends_on_ample_set_and_coenabled(DepDisAct,AmpleSet,_Act)),DependentDisabledActions),
540 ( DependentDisabledActions = [] ->
541 fail % in this case we know that no action dependent on AmpleSet can be enabled after executing Act
542 ;
543 enables_pred_action1(Act,DependentDisabledActions,AmpleSet,CurID,EnableGraph,Depth)).
544
545 enables_pred_action1(Act,DepDisActs,AmpleSet,CurID,EnableGraph,Depth) :-
546 % visited_expression/2 and state_corresponds_to_initialised_b_machine/2 should be called once for each state,
547 % avoid multiple calls per state
548 (Depth==0 ->
549 empty_state(ST)
550 ;
551 visited_expression(CurID,RawState),
552 state_corresponds_to_initialised_b_machine(RawState,ST)
553 ),
554 %Pred =.. [evaluate_enabling_predicate_for_por, ST, AmpleSet],
555 enable_graph: path_set(EnableGraph,Act,DepDisActs,enable_graph,
556 evaluate_enabling_predicate_for_por(ST,AmpleSet),Depth,Path,Length),
557 debug_print_path(CurID,Path,Length).
558
559 % guaranteeing that the dependent action to AmpleSet has been enabled from an action off AmpleSet
560 sets_disjoint(AmpleSet,Path) :-
561 list_to_ord_set(Path,OrdSet),
562 \+ord_intersection(AmpleSet,OrdSet).
563
564 depends_on_ample_set_and_coenabled(Act,AmpleSet,Act1) :-
565 ? member(Act1,AmpleSet),
566 dependent_act(Act,Act1,_Status,Coenabled),
567 Coenabled==true.
568
569 debug_print_path(CurID,Path,Length) :-
570 debug_println(20,'***** Enable Path *****'),
571 debug_println(20,path(CurID,Path,Length)),
572 debug_println(20,'***********************').
573
574 /************************** DETERMINING POSSIBLE AMPLE SETS (END) ******************************/
575
576 /************************** CHECKING IF ALL ACTIONS FROM AMPLE SET ARE STUTTER ACTIONS (BEGIN) WITH REGARD TO THE INVARIANT ******************************/
577 /************************** PREDICATES WHICH SATISFY CONDITION (A3) ******************************/
578
579 stutter_actions(Actions) :-
580 maplist(is_stutter_action,Actions).
581
582 % visible actions are non stutter actions
583 is_stutter_action(Act) :-
584 ( stutter_action(Act) ->
585 debug_println(19,stutter_action(Act))
586 ; visible_action(Act) ->
587 debug_println(19,visible_action(Act)),
588 fail
589 ;
590 check_if_action_is_stutter_wrt_inv(Act)
591 ).
592
593 % A stutter action
594 % * either cannot change the current invariant value or
595 % * if it violates the invariant then no independent action can undo the change
596 % That's why we must check if the particular action preserves
597 % the full invariant in order to determine if the action is
598 % stutter under the following LTL formula:
599 % G Phi, where Phi is the invariant.
600 check_if_action_is_stutter_wrt_inv(Act) :- %print(check_stutter(Act)),nl,
601 b_operation_preserves_full_invariant(Act),!,
602 assertz(stutter_action(Act)),
603 debug_println(19,stutter_according_to_proof_info(Act)).
604 check_if_action_is_stutter_wrt_inv(Act) :-
605 b_specialized_invariant_for_op(Act,Invariant), %translate:print_bexpr(Invariant),nl,
606 conjunction_to_list(Invariant,Conjunctions), % getting all conjunctions from the invariant
607 b_get_read_write(Act,_Reads,Writes), % print(writes(Act,Writes)),nl,
608 ? ( action_does_not_modify_inv_or_inv_cannot_be_repaired(Writes,Conjunctions)
609 -> assertz(stutter_action(Act)),
610 debug_println(19,stutter_or_not_repairable(Act))
611 ; assertz(visible_action(Act)),fail
612 ).
613
614 :- use_module(probsrc(bsyntaxtree),[find_identifier_uses/3]).
615 :- use_module(probsrc(bmachine),[b_specialized_invariant_for_op/2]).
616 % either an action does not affect an invariant or it writes *all* variables of an invariant
617 % TODO: a third option would be if no other independent event modifies the variable of this invariant
618 % one could even look whether any (enabled) event in the ample set modifies the given conjunct
619 % For example if we modify x and invariant is x<y, but if no other enabled event modifies x,y we are fine
620 action_does_not_modify_inv_or_inv_cannot_be_repaired(_Vars,[]).
621 action_does_not_modify_inv_or_inv_cannot_be_repaired(Vars,[Conj|Conjs]) :-
622 find_identifier_uses(Conj,[],UsedIds),
623 ord_intersection(UsedIds,Vars,Common),
624 (Common=[]
625 -> true % invariant not affected by action
626 ; ord_seteq(Common,UsedIds) % we write all variables of an invariant; no independent action can change/repair its status
627 ),
628 ? action_does_not_modify_inv_or_inv_cannot_be_repaired(Vars,Conjs).
629
630
631
632 /************************** CHECKING IF ALL ACTIONS FROM AMPLE SET ARE STUTTER ACTIONS (END) ******************************/