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) ******************************/ |