1 % (c) 2012-2019 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/2,specfile_possible_trans_name/2,specfile_trans/6]).
23 :- use_module(probsrc(state_space),[visited_expression/2,use_no_timeout/1]).
24
25 /* POR modules */
26 :- use_module(probporsrc(enable_graph)).
27 % --> /* The Static Analysis' module */
28 :- use_module(probporsrc(static_analysis),[enable_graph/1,dependent_act/4]).
29 :- use_module(probpgesrc(pge_algo),[is_pge_opt_on/1,compute_and_update_disabled_enabled_operations/3]).
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.').
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 % Arguments:
120 % CurID - the current ID of the state.
121 % CurState - the current evaluation of all global variables (and constants) in the machine.
122 % 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.
123 % POROptions - the options being set for exploring the state space by means of partial order reduction
124 %
125 compute_ample_set2(CurID,CurState,por(TYPE,UseEnableGraph,Depth,PGE)) :-
126 user: reset_max_reached,
127 prepare_state_for_specfile_trans(CurState,PreparedCurState),
128 get_enabled_actions_at_state(CurID,PreparedCurState,PGE,TopLevelActions,Transitions,DisabledTopLevelActions),
129 % we want only unique action names for analyzing and computing of ample sets
130 list_to_ord_set(TopLevelActions,TopLevelActionsSet),
131 % compute a sound ample set from all actions enabled in state CurID
132 compute_ample_actions(CurID,TopLevelActionsSet,por(TYPE,UseEnableGraph,Depth,PGE),AmpleSet),
133 debug_println(20,sets(CurID,allActions(TopLevelActionsSet),ampleSet(AmpleSet))),
134 % mark state as visited (Cycle Condition (A 4))
135 assert(explored_state(CurID)),
136 ( (AmpleSet \= []) ->
137 % compute just the actions from the ample set (case of state space reduction)
138 % AmpleSet is a non-empty subset of enabled(CurID), AmpleSet can be equal to AllEnabledActions
139 add_transitions(AmpleSet,CurID,Transitions,ActNameSuccessors),
140 update_enabled_disabled_information_if_necessary(PGE,ActNameSuccessors,DisabledTopLevelActions,AmpleSet)
141 ; otherwise ->
142 true /* DEADLOCK */
143 ),
144 (user: max_reached ->
145 user: assert_max_reached_for_node(CurID),
146 MaxReached=true
147 ; MaxReached=false
148 ),
149 (CurID==root ->
150 user: save_constants(MaxReached)
151 ; user: add_new_transitions_to_cache(CurID)
152 ),!. % once we have computed the ample set in CurState we don't want to backtrack
153
154 % computing a sound ample set of actions.
155 compute_ample_actions(CurID,AllEnabledActions,POROptions,AmpleSet) :-
156 % get_ample_actions/5 call only reasonable to be executed when more than one actions are enabled in CurID
157 (more_than_one_event(AllEnabledActions) ->
158 get_ample_actions(CurID,AllEnabledActions,POROptions,AmpleSet)
159 ; otherwise ->
160 AmpleSet = AllEnabledActions
161 ).
162
163 more_than_one_event(SetOfActions) :-
164 length(SetOfActions,L),L>1.
165
166 /************************** ADD TRANSITIONS (BEGIN) ******************************/
167
168 % +ActNameSuccessors: a list of tuples (Act,SuccIds), where 'SuccIds' is the list of all state ids that are successor states of Act
169 add_transitions(AmpleSet,CurID,Transitions,ActNameSuccessors) :-
170 add_transitions(no,AmpleSet,CurID,Transitions,[],ActNameSuccessors).
171
172 % first argument tests if the state has been fully explored while adding the
173 % ample set transitions to the state space ('yes' means state has been fully explored, so we can stop,
174 % 'no' means that the rest of the ample set transitions should be added to the state space until
175 % no more ample actions in the list or until the state is fully explored)
176 add_transitions(yes,_AmpleSet,_CurID,_Transitions,ActNameSuccessors,ActNameSuccessors).
177 add_transitions(_FullyExplored,[],_CurID,_Transitions,ActNameSuccessors,ActNameSuccessors).
178 add_transitions(no,[ActionName|ActNames],CurID,Transitions,ActNameSuccessorsGen,ActNameSuccessors) :-
179 add_action_name_transitions(Transitions,CurID,ActionName,[],RemTransitions,FullyExplored,ActNameSuccessorsGen,ActNameSuccessorsGen1),
180 add_transitions(FullyExplored,ActNames,CurID,RemTransitions,ActNameSuccessorsGen1,ActNameSuccessors).
181
182 add_action_name_transitions([],_CurID,_ActionName,RemTransitions,RemTransitions,no,ActSuccsGen,ActSuccsGen).
183 add_action_name_transitions([(ActionName1,Transitions)|R],CurID,ActionName,IgnoredActions_so_far,
184 RemTransitions,FullyExplored,ActSuccsGen,ActSuccs) :-
185 (ActionName == ActionName1 ->
186 % in this case we do not need to go through the rest of the transitions list
187 add_action_transitions(ActionName,Transitions,CurID,NewIds),
188 ActSuccsGen1 = [(ActionName,NewIds)|ActSuccsGen],
189 append(IgnoredActions_so_far,R,AllRemainedActions),
190 (cycle_condition_check_positive_l(NewIds) ->
191 debug_println(9,'*********** POSSIBLE CYCLE DETECTED *************'),
192 debug_println(9,computing_all_other_enabled_actions(back_transition(ActionName),AllRemainedActions)),
193 add_all_other_enabled_transitions(AllRemainedActions,CurID,ActSuccsGen1,ActSuccs),
194 RemTransitions=[],
195 FullyExplored = yes
196 ; otherwise -> FullyExplored = no, RemTransitions = AllRemainedActions, ActSuccs=ActSuccsGen1)
197 ; otherwise ->
198 % keeping track of all ignored actions so far, we don't want to go through the same order of actions every time we
199 % want to add a transition from AmpleSet to the state space
200 ord_add_element(IgnoredActions_so_far, (ActionName1,Transitions), IgnoredActions_so_far1),
201 add_action_name_transitions(R,CurID,ActionName,IgnoredActions_so_far1,RemTransitions,FullyExplored,ActSuccsGen,ActSuccs)
202 ).
203
204 % cycle condition A4 check
205 cycle_condition_check_positive_l(NewIds) :-
206 check_cycle_proviso,!,
207 member(NewId,NewIds),
208 \+var(NewId),
209 explored_state(NewId).
210
211 add_all_other_enabled_transitions([],_CurID,ActSuccsGen,ActSuccsGen).
212 add_all_other_enabled_transitions([(ActionName,Transitions)|R],CurID,ActSuccsGen,ActSuccs) :-
213 add_action_transitions(ActionName,Transitions,CurID,NewIds),
214 ActSuccsGen1 = [(ActionName,NewIds)|ActSuccsGen],
215 add_all_other_enabled_transitions(R,CurID,ActSuccsGen1,ActSuccs).
216
217 add_action_transitions(_ActionName,Transitions,CurID,NewIds) :-
218 findall(NewId,
219 (member((Act,NewExpression,TransInfo,Residue),Transitions),
220 user: add_trans_id(CurID,Act,NewExpression,Residue,NewId,TransInfo,_)),NewIds).
221
222 update_enabled_disabled_information_if_necessary(PGE,ActNameSuccessors,DisabledActionsAtCurState,EnabledActionsAtCurState) :-
223 (is_pge_opt_on(PGE) ->
224 compute_and_update_disabled_enabled_operations(ActNameSuccessors,DisabledActionsAtCurState,EnabledActionsAtCurState)
225 ; true).
226
227 /************************** ADD TRANSITIONS (END) ******************************/
228
229 /* Auxiliary predicates for getting action names enabled at the current state */
230
231 % getting action names from the action tuples
232 %get_action_names_only(Actions,ActionNames) :-
233 % maplist(get_action_name,Actions,ActionNames).
234 %get_action_name((ActionName,_Representations),ActionName).
235
236 get_enabled_actions_at_state(CurID,CurState,PGE,EnabledTopLevelActions,Transitions,DisabledTopLevelActions) :-
237 get_specfile_possible_trans_names(CurID,CurState,PGE,TopLevelActions,DisabledOperations),
238 get_enabled_actions_at_state_aux(TopLevelActions,CurID,CurState,EnabledTopLevelActions,Transitions,DisabledOperationsNew),
239 list_to_ord_set(DisabledOperationsNew,DisabledOperationsNewSet),
240 ord_union(DisabledOperations,DisabledOperationsNewSet,DisabledTopLevelActions).
241
242 get_specfile_possible_trans_names(CurID,CurState,PGE,TopLevelActions,DisabledOperations) :-
243 ( PGE\= off ->
244 % get enabled top level actoions using the information from the PGE algo
245 pge_algo: get_possible_enabled_trans_names(CurID,CurState,DisabledOperations,_EnabledOperations,TopLevelActions)
246 ; otherwise ->
247 get_specfile_possible_trans_names(CurState,TopLevelActions),
248 DisabledOperations = [] % in case PGE is not on we don't have any information about the disabledness of actions
249 ).
250
251 get_specfile_possible_trans_names(CurState,TopLevelActions) :-
252 findall(ActionName,specfile_possible_trans_name(CurState,ActionName),TopLevelActions).
253
254 get_enabled_actions_at_state_aux(TopLevelActions,CurID,CurState,EnabledTopLevelActions,Transitions,DisabledTopLevelActionsNew) :-
255 get_enabled_actions_at_state_aux2(TopLevelActions,CurID,CurState,[],EnabledTopLevelActions,[],Transitions,[],DisabledTopLevelActionsNew).
256
257 get_enabled_actions_at_state_aux2([],_CurID,_CurState,EnabledTopLevelActions,EnabledTopLevelActions,Transitions,Transitions,DisabledNew,DisabledNew).
258 get_enabled_actions_at_state_aux2([TopLevelAction|R],CurID,CurState,EnabledTopLevelActionsGen,EnabledTopLevelActions,TransitionsGen,Transitions,DisabledNewGen,DisabledNew) :-
259 (get_top_level_action_transitions(CurID,CurState,TopLevelAction,ActionTransitionsTuple) ->
260 EnabledTopLevelActionsGen1 = [TopLevelAction|EnabledTopLevelActionsGen],
261 TransitionsGen1 = [ActionTransitionsTuple|TransitionsGen],
262 DisabledNewGen1 = DisabledNewGen
263 ; otherwise ->
264 EnabledTopLevelActionsGen1 = EnabledTopLevelActionsGen,
265 TransitionsGen1 = TransitionsGen,
266 DisabledNewGen1 = [TopLevelAction|DisabledNewGen]
267 ),
268 get_enabled_actions_at_state_aux2(R,CurID,CurState,EnabledTopLevelActionsGen1,EnabledTopLevelActions,TransitionsGen1,Transitions,DisabledNewGen1,DisabledNew).
269
270 get_top_level_action_transitions(CurID,CurState,TopLevelAction,ActionTransitionsTuple) :-
271 findall((Act,NewExpression,TransInf,Residue),
272 specfile_trans_timeout(CurID,CurState,TopLevelAction,Act,NewExpression,TransInf,Residue),
273 Transitions),
274 % in case TopLevelAction is not enabled we do not save the transitions in the list
275 Transitions\=[],
276 ActionTransitionsTuple = (TopLevelAction,Transitions).
277
278 specfile_trans_timeout(CurID,CurState,ActionName,Act,NewExpression,TransInf,Residue) :-
279 (use_no_timeout(CurID) ->
280 specfile_trans(CurState,ActionName,Act,NewExpression,TransInf,Residue)
281 ; preferences:preference(time_out,CurTO),
282 time_out_with_enum_warning_for_findall(specfile_trans(CurState,ActionName,Act,NewExpression,TransInf,Residue),CurTO,TimeOutRes),
283 pge_algo: check_timeout_result(CurID,ActionName,CurTO,TimeOutRes),
284 Residue==[]
285 ).
286 /* Auxiliary predicates for getting action names enabled at the curent state */
287 %---------------------------------------------------------------------------------------------------------------------------------
288 /************************** DETERMINING POSSIBLE AMPLE SETS (BEGIN) ******************************/
289
290 /************************** PREDICATES COMPUTING AMPLE SETS WITH RESPECT TO CONDITIONS (A 2) and (A 3) *************************/
291
292 /*
293
294 implementation of the ample-sets approach satisfying the dependency condition (A 2)
295 by using enabling and dependence analysis (see module enabling analysis)
296
297 */
298
299 get_ample_actions(CurID,AllEnabledActions,POROptions,AmpleSet) :-
300 get_preference(por_heur,Pref),
301 get_ample_actions_pref(Pref,CurID,AllEnabledActions,POROptions,AmpleSet).
302
303 get_ample_actions_pref(minimal,CurID,AllEnabledActions,POROptions,AmpleSet) :- !,
304 get_possible_ample_actions_minimal(AllEnabledActions,CurID,AllEnabledActions,POROptions,AmpleSet).
305 get_ample_actions_pref(Pref,CurID,AllEnabledActions,POROptions,AmpleSet) :-
306 get_possible_ample_actions(Pref,AllEnabledActions,CurID,AllEnabledActions,POROptions,AmpleSet).
307
308 get_possible_ample_actions(_Pref,[],_CurID,AllEnabledActions,_POROptions,AllEnabledActions).
309 get_possible_ample_actions(Pref,Actions,CurID,AllEnabledActions,POROptions,AmpleSet) :-
310 % choosing of action for computing a possible ample set for CurID should be random
311 select_enabled_action_pref(Pref,Actions,Act,RemainedActions),
312 (get_valid_ample_set_act(CurID,POROptions,Act,AllEnabledActions,AmpleSet) -> % get ample set satisfying (A 2) and (A 3) i.r.t. Act
313 true
314 ; otherwise -> % search for another valid ample set
315 get_possible_ample_actions(Pref,RemainedActions,CurID,AllEnabledActions,POROptions,AmpleSet)
316 ).
317
318 get_valid_ample_set_act(CurID,POROptions,Act,AllEnabledActions,AmpleSet) :-
319 POROptions = por(ample_sets2,_,_,_),!,
320 %% trying to find an ample set by the closure method
321 get_possible_ample_set_closure(CurID,Act,AllEnabledActions,AmpleSet).
322 get_valid_ample_set_act(CurID,POROptions,Act,AllEnabledActions,AmpleSet) :-
323 get_valid_ample_set_act_normal(CurID,POROptions,Act,AllEnabledActions,AmpleSet).
324
325 get_valid_ample_set_act_normal(CurID,POROptions,Act,AllEnabledActions,AmpleSet) :-
326 % finding a set (DepActs) satisfying (A 2.1) // there is only one possible set, do not recall here
327 get_dependent_actions(CurID,POROptions,Act,AllEnabledActions,DepActs,IndActs),!,
328 ( (is_enabling_dependency_condition_satisfied(IndActs,DepActs,AllEnabledActions,CurID,POROptions), % check whether DepActs satisfies (A 2.2)
329 check_stutter_condition(DepActs,AllEnabledActions)) % checking (A 3)
330 -> AmpleSet = DepActs
331 ; fail). % should fail in order to try to get another valid ample set
332
333 select_enabled_action_pref(random,Actions,Act,RemainedActions):- !,
334 random_select(Act,Actions,RemainedActions).
335 select_enabled_action_pref(first,[Act|RemainedActions],Act,RemainedActions):- !.
336 select_enabled_action_pref(Pref,Actions,Act,RemainedActions) :-
337 add_warning(ample_sets,'Unknown preference for choosing an action from the set of enabled actions: ', Pref),
338 random_select(Act,Actions,RemainedActions). % choose the default option for choosing an action
339
340 check_stutter_condition(AmpleSet,AllEnabledActions) :-
341 \+ ord_seteq(AmpleSet,AllEnabledActions),!,
342 check_cycle_proviso(AmpleSet).
343
344 check_cycle_proviso(AmpleSet) :-
345 % in case that we don't check for invariant violations, we don't have to prove the stuttering condition for AmpleSet
346 (check_cycle_proviso ->
347 stutter_actions(AmpleSet)
348 ; true).
349
350 get_possible_ample_actions_minimal(AllEnabledActions,CurID,AllEnabledActions,POROptions,AmpleSet) :-
351 maplist(get_valid_ample_set_act_nonfail(CurID,AllEnabledActions,POROptions),AllEnabledActions,AmpleSets),
352 get_minimal_set(AmpleSets,AmpleSet),
353 debug_println(9,minimal_ample_set(AmpleSet,AmpleSets)).
354
355 get_minimal_set([AmpleSet|Rest],MinAmpleSet) :-
356 length(AmpleSet,Length),
357 get_minimal_set_length(Length,AmpleSet,Rest,MinAmpleSet).
358
359 get_minimal_set_length(1,AmpleSet,_Rest,AmpleSet).
360 get_minimal_set_length(_Length,AmpleSet,[],AmpleSet).
361 get_minimal_set_length(Length,AmpleSet,[AmpleSet2|Rest],MinAmpleSet) :-
362 length(AmpleSet2,Length2),
363 (Length2<Length ->
364 get_minimal_set_length(Length2,AmpleSet2,Rest,MinAmpleSet)
365 ; otherwise ->
366 get_minimal_set_length(Length,AmpleSet,Rest,MinAmpleSet)).
367
368 get_valid_ample_set_act_nonfail(CurID,AllEnabledActions,POROptions,Act,AmpleSet) :-
369 (get_valid_ample_set_act(CurID,POROptions,Act,AllEnabledActions,AmpleSet)
370 -> true
371 ; AmpleSet = AllEnabledActions).
372
373 %%%%%% the closure method for computing ample sets %%%%%%
374 get_possible_ample_set_closure(CurID,Act,AllEnabledActions,AmpleSet) :-
375 get_valid_ample_set_act_closure(CurID,Act,AllEnabledActions,AmpleSet),!,
376 check_stutter_condition(AmpleSet,AllEnabledActions). % checking (A 3)
377
378 get_valid_ample_set_act_closure(CurID,Act,AllEnabledActions,AmpleSet) :-
379 %(length(AllEnabledActions,3) -> trace;true),
380 list_to_ord_set([Act],WorkSet),
381 list_to_ord_set([],ClosureSet),
382 compute_closure_set(WorkSet,CurID,ClosureSet,AllEnabledActions,Result),
383 ord_intersection(Result,AllEnabledActions,AmpleSet).
384
385 compute_closure_set([],_CurID,ClosureSet,_AllEnabledActions,ClosureSet).
386 compute_closure_set([Act|Acts],CurID,ClosureSet,AllEnabledActions,Result) :-
387 ord_add_element(ClosureSet,Act,ClosureSet1),
388 get_new_work_set(Act,Acts,CurID,AllEnabledActions,ClosureSet1,NewWorkSet),
389 compute_closure_set(NewWorkSet,CurID,ClosureSet1,AllEnabledActions,Result).
390
391 get_new_work_set(Act,WorkSet,CurID,AllEnabledActions,ClosureSet1,NewWorkSet) :-
392 ord_member(Act,AllEnabledActions),!,
393 get_dependency_set_closure(Act,WorkSet,CurID,ClosureSet1,NewWorkSet).
394 get_new_work_set(Act,WorkSet,CurID,AllEnabledActions,ClosureSet1,NewWorkSet) :-
395 get_enabling_set_for_act(Act,WorkSet,CurID,AllEnabledActions,ClosureSet1,NewWorkSet).
396
397 get_dependency_set_closure(Act,WorkSet,CurID,ClosureSet1,NewWorkSet) :-
398 findall(Act1,(is_dependent_to_and_coenabled(Act,Act1,CurID),ord_nonmember(Act1,ClosureSet1)),NewActions),
399 list_to_ord_set(NewActions,NewActionsSet),
400 ord_union(WorkSet,NewActionsSet,NewWorkSet).
401
402 get_enabling_set_for_act(Act,WorkSet,CurID,AllEnabledActions,ClosureSet1,NewWorkSet) :-
403 % Act is disabled at current state
404 findall(Act1,find_enabling_action(Act,CurID,AllEnabledActions,ClosureSet1,Act1),NewActions),
405 list_to_ord_set(NewActions,NewActionsSet),
406 ord_union(WorkSet,NewActionsSet,NewWorkSet).
407
408 find_enabling_action(Act,CurID,AllEnabledActions,ClosureSet,Act1) :-
409 member(Act1,AllEnabledActions),
410 ord_nonmember(Act1,ClosureSet),
411 can_enable_certain_action(Act1,Act,CurID).
412
413 can_enable_certain_action(Act,ActionToBeEnabled,CurID) :-
414 ( enables(Act,ActionToBeEnabled) ->
415 debug_println(9,enables(Act,ActionToBeEnabled))
416 ; otherwise ->
417 enable_graph(EnableGraph),
418 min_path(Act,ActionToBeEnabled,EnableGraph,P,L),
419 debug_print_path(CurID,P,L),
420 assert(enables(Act,ActionToBeEnabled))).
421
422 % get_dependent_actions(+CurID,+POROptions,+Act,+AllEnabledActions,+EnGraph,-DepActs)
423 % CurID - the ID of the current state (used here only for debugging purposes)
424 % POROptions - partial order reduction options (e.g. UseEnableGraph, Depth)
425 % Act - the action with which the current dependency class will be computed
426 % AllEnabledActions - the set of all in CurID enabled actions and it is an ordinary set
427 % DepActs - the computed candidate for ample set
428 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
429 % EnableGraph - the enable graph for all possible enable actions' relations in the current machine. The enable graph will
430 % be computed only single time (before starting with the verification of the state space).
431
432 get_dependent_actions(CurID,_POROptions,Act,AllEnabledActions,DepActs,IndActions) :-
433 % finding all dependent actions to Act (A 2.1)
434 get_dependency_set(Act,AllEnabledActions,CurID,DepActs),
435 ord_subtract(AllEnabledActions,DepActs,IndActions).
436
437 is_enabling_dependency_condition_satisfied([],_DepActs,_AllEnabledActions,_CurID,_POROptions) :- !,fail.
438 is_enabling_dependency_condition_satisfied(IndActs,DepActs,AllEnabledActions,CurID,POROptions) :-
439 enable_graph(EnableGraph),
440 vertices(EnableGraph,Vertices), % getting all possible actions that can be enabled
441 % DisabledActions = Vertices\AllEnabledActions
442 ord_subtract(Vertices,AllEnabledActions,DisabledActions),
443 % searching for an independent action to Act that could enable a currently disabled action that is dependent to Act (A 2.2)
444 \+may_enable_dep_action_list(IndActs,DepActs,DisabledActions,EnableGraph,CurID,POROptions).
445
446 may_enable_dep_action_list(IndActs,DepActs,DisabledActions,EnableGraph,CurID,POROptions) :-
447 member(Act2,IndActs),
448 may_enable_dep_action(Act2,DepActs,DisabledActions,EnableGraph,CurID,POROptions).
449
450
451 get_dependency_set(Act,AllEnabledActions,CurID,DepActions_so_far) :-
452 vertices_edges_to_ugraph([],[],G),
453 get_dependency_tuples_converted_to_edges(Act,AllEnabledActions,RestEnabledActions,CurID,Edges),
454 add_edges(G,Edges,G1),
455 get_dependency_set1(Act,G1,[],RestEnabledActions,CurID,DepActions_so_far).
456
457 get_dependency_tuples_converted_to_edges(Act,AllEnabledActions,RestEnabledActions,CurID,Res) :-
458 findall(Act1,(member(Act1,AllEnabledActions), is_dependent_to(Act,Act1,CurID)),DepActs),
459 findall([Act-Act1,Act1-Act],member(Act1,DepActs),Edges),
460 ord_subtract(AllEnabledActions,DepActs,RestEnabledActions),
461 append(Edges,Res).
462
463 get_dependency_set1(Act,G,G,_Actions,_CurID,Res) :-
464 reachable(Act,G,Res).
465 get_dependency_set1(Act,G,_GPrime,Actions,CurID,Res) :-
466 GPrime1 = G,
467 vertices(G,Vertices),
468 findall([V-Act1,Act1-V],(member(Act1,Actions),member(V,Vertices),is_dependent_to(V,Act1,CurID)),NewEdges),
469 append(NewEdges,NewEdges1),
470 add_edges(G,NewEdges1,G1),vertices(G1,Vertices1),
471 ord_subtract(Actions,Vertices1,Actions1),
472 get_dependency_set1(Act,G1,GPrime1,Actions1,CurID,Res).
473
474 is_dependent_to(Act,Act1,CurID) :-
475 (dependent_act(Act,Act1,Status,_Coenabled) ->
476 (Status=predicate(Pred) -> check_enable_dependency(Act,Act1,Pred,CurID); true)
477 ; otherwise ->
478 fail
479 ).
480
481 is_dependent_to_and_coenabled(Act,Act1,CurID) :-
482 dependent_act(Act,Act1,Status,true),
483 (Status=predicate(Pred) -> check_enable_dependency(Act,Act1,Pred,CurID); true).
484
485 check_enable_dependency(Act,Act1,Pred,CurID) :-
486 debug_println(9,checking_guard_dependency(Act,Act1,Pred)),
487 visited_expression(CurID,RawState),
488 state_corresponds_to_initialised_b_machine(RawState,State),
489 empty_state(LocalState),
490 % if the enable predicate Pred evaluates to false we know that (Act,Act1) is a dependent pair
491 \+enable_graph: b_test_boolean_expression_wf(Pred,LocalState,State).
492
493 /* searching for enabling path beginning from an action which is not from AmpleSet and
494 which enables action dependent on AmpleSet */
495 may_enable_dep_action(Act,AmpleSet,DisabledActions,EnableGraph,CurID,por(_TYPE,UseEnableGraph,Depth,_PGE)) :-
496 ( UseEnableGraph = true ->
497 check_enabling_path(CurID,Act,DisabledActions,AmpleSet,EnableGraph,Depth)
498 ; otherwise ->
499 member(DisAct,DisabledActions),
500 % we check here only currently disabled actions dependent on AmpleSet that can be enabled later
501 depends_on_ample_set_and_coenabled(DisAct,AmpleSet,_DepAct),
502 % is there a path that can enable Act1, which is dependent on Act
503 enables_action(CurID,Act,DisAct,AmpleSet,EnableGraph)
504 ),
505 !.
506
507 enables_action(CurID,Act,DisAct,AmpleSet,EnableGraph) :-
508 ( enables(Act,DisAct) ->
509 % should improve performance a little bit (not applicable when using enable graphs)
510 debug_println(9,enables(Act,DisAct))
511 ; check_if_enabled(CurID,Act,DisAct,AmpleSet,EnableGraph) ->
512 true
513 ; otherwise ->
514 fail
515 ).
516
517 check_if_enabled(CurID,Act,DisAct,AmpleSet,EnableGraph) :-
518 min_path(Act,DisAct,EnableGraph,P,L),
519 sets_disjoint(AmpleSet,P),
520 debug_print_path(CurID,P,L),
521 assert(enables(Act,DisAct)).
522
523 % predicates used for the enable graph feature
524 check_enabling_path(CurID,Act,DisabledActions,AmpleSet,EnableGraph,Depth) :-
525 findall(DepDisAct,(member(DepDisAct,DisabledActions),depends_on_ample_set_and_coenabled(DepDisAct,AmpleSet,_Act)),DependentDisabledActions),
526 ( DependentDisabledActions = [] ->
527 fail % in this case we know that no action dependent on AmpleSet can be enabled after executing Act
528 ; otherwise ->
529 enables_pred_action1(Act,DependentDisabledActions,AmpleSet,CurID,EnableGraph,Depth)).
530
531 enables_pred_action1(Act,DepDisActs,AmpleSet,CurID,EnableGraph,Depth) :-
532 % visited_expression/2 and state_corresponds_to_initialised_b_machine/2 should be called once for each state,
533 % avoid multiple calls per state
534 (Depth==0 ->
535 empty_state(ST)
536 ; otherwise ->
537 visited_expression(CurID,RawState),
538 state_corresponds_to_initialised_b_machine(RawState,ST)
539 ),
540 %Pred =.. [evaluate_enabling_predicate_for_por, ST, AmpleSet],
541 enable_graph: path_set(EnableGraph,Act,DepDisActs,enable_graph,
542 evaluate_enabling_predicate_for_por(ST,AmpleSet),Depth,Path,Length),
543 debug_print_path(CurID,Path,Length).
544
545 % guaranteeing that the dependent action to AmpleSet has been enabled from an action off AmpleSet
546 sets_disjoint(AmpleSet,Path) :-
547 list_to_ord_set(Path,OrdSet),
548 \+ord_intersection(AmpleSet,OrdSet).
549
550 depends_on_ample_set_and_coenabled(Act,AmpleSet,Act1) :-
551 member(Act1,AmpleSet),
552 dependent_act(Act,Act1,_Status,Coenabled),
553 Coenabled==true.
554
555 debug_print_path(CurID,Path,Length) :-
556 debug_println(20,'***** Enable Path *****'),
557 debug_println(20,path(CurID,Path,Length)),
558 debug_println(20,'***********************').
559
560 /************************** DETERMINING POSSIBLE AMPLE SETS (END) ******************************/
561
562 /************************** CHECKING IF ALL ACTIONS FROM AMPLE SET ARE STUTTER ACTIONS (BEGIN) WITH REGARD TO THE INVARIANT ******************************/
563 /************************** PREDICATES WHICH SATISFY CONDITION (A3) ******************************/
564
565 stutter_actions(Actions) :-
566 maplist(is_stutter_action,Actions).
567
568 % visible actions are non stutter actions
569 is_stutter_action(Act) :-
570 ( stutter_action(Act) ->
571 debug_println(9,stutter_action(Act))
572 ; visible_action(Act) ->
573 debug_println(9,visible_action(Act)),
574 fail
575 ; otherwise ->
576 check_if_action_is_stutter_wrt_inv(Act)
577 ).
578
579 % A stutter action cannot change the current invariant value.
580 % That's why we must check if the particular action preserves
581 % the full invariant in order to determine if the action is
582 % stutter under the following LTL formula:
583 % G Phi, where Phi is the invariant.
584 check_if_action_is_stutter_wrt_inv(Act) :-
585 b_operation_preserves_full_invariant(Act),!,
586 assert(stutter_action(Act)),
587 debug_println(9,stutter_according_to_proof_info(Act)).
588 check_if_action_is_stutter_wrt_inv(Act) :-
589 b_get_invariant_from_machine(Invariant),
590 conjunction_to_list(Invariant,Conjunctions), % getting all conjunctions from the invariant
591 b_get_read_write(Act,_Reads,Writes),
592 ( action_does_not_modify_important_variables_in_the_inv(Writes,Conjunctions)
593 -> assert(stutter_action(Act)),
594 debug_println(9,stutter_according_to_read_write_info(Act))
595 ; otherwise
596 -> assert(visible_action(Act)),fail
597 ).
598
599 action_does_not_modify_important_variables_in_the_inv([],_Conjuncions).
600 action_does_not_modify_important_variables_in_the_inv([Var|WrVars],Conjunctions) :-
601 var_not_changing_visible_condition_in_the_inv(Var,Conjunctions),
602 action_does_not_modify_important_variables_in_the_inv(WrVars,Conjunctions).
603
604 var_not_changing_visible_condition_in_the_inv(_Var,[]).
605 var_not_changing_visible_condition_in_the_inv(Var,[Conj|Conjs]) :-
606 ( occurs_in_expr(Var,Conj)
607 -> (\+ trivial_predicate(Var,Conj) -> fail; true)
608 ; otherwise -> true
609 ),
610 var_not_changing_visible_condition_in_the_inv(Var,Conjs).
611
612 trivial_predicate(Var,Conj) :-
613 \+var(Conj),
614 trivial_member_predicate(Var,Conj).
615
616 /*
617
618 TODO: Define formal when an action in Event-B/B can be seen as a stutter action.
619 Maybe we should use here the predicate b_specialized_invariant_for_op/2 from bmachine.pl.
620
621 */
622
623 /*trivial_member_predicate(Var,Conj) :-
624 Conj=b(member(b(identifier(Var),integer,_),b(integer_set('NATURAL'),set(integer),_)),pred,_).
625 trivial_member_predicate(Var,Conj) :-
626 Conj=b(member(b(identifier(Var),integer,_),b(integer_set('NAT'),set(integer),_)),pred,_).*/
627 trivial_member_predicate(Var,Conj) :-
628 Conj=b(member(b(identifier(Var),integer,_),b(integer_set('INT'),set(integer),_)),pred,_).
629 trivial_member_predicate(Var,Conj) :-
630 Conj=b(member(b(identifier(Var),integer,_),b(integer_set('INTEGER'),set(integer),_)),pred,_).
631
632 /************************** CHECKING IF ALL ACTIONS FROM AMPLE SET ARE STUTTER ACTIONS (END) ******************************/