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