% % The workflow repair engine % % Reasoning module % % % The reasoning module takes as input: % - the workflow model % - the failure information % - information about the initial workflow execution (execution log) % - the time model (time slots) % and generates % - the repair plan which leads the workflow to the correct (w.r.t. object states) completion % % The repair reasoner is implemented using DLV system. % See www.dlvsystem.com for further information. % % (c) 2006-2008 % %%%% BASICS OF TIME MODEL % % nodes are ordered time points % before is defined on time points % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% node(1). node(Y):-next(X,Y). % ,#int(X),#int(Y). before(X,Z) :- next(X,Z). before(X,Z) :- before(X,Y), before(Y,Z), X != Z. %%%% PRECEIDING OF ACTIVITIES % % preceiding of activities is the transitive relation % preceiding is defined on activities according to WF model % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% prec(A,B):- prec(A,C), prec(C,B). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% PROPERTIES OF OBJECTS %%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% RIGHTVERSION of an object % % object has a right version (w.r.t. to an activity which effects it) only if there were no possibility to % overwrite it % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% rightVersion(A,OI,AI,T) :- prec(AI,A), node(T), ineffset(AI,OI), inreadset(A,OI), not unfixed(A,OI,AI,T). unfixed(A,OI,AI,T) :- prec(AI,B), prec(B,A), node(T), ineffset(B,OI), ineffset(AI,OI), not skipped(B,T), inreadset(A,OI). %%%% -SUSPECTED activities % % an object state is not suspected to be infected if % (1) the application $v$ of activity $a$ which % produced $o$ was correct at $v$, % (2) at $t$ this activity is enabled % (3) at $t$ all inputs of $a$ are correct and these inputs are in the % right version for $a$ % (4) the object state of $(o,a,v)$ was not % produced by different applications of activities. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% someInputSuspOrFalseVersion(A,V,T) :- inreadset(A,OI), node(T), dep(O,A,V,OI,AI,VI), not rightVersion(A,OI,AI,T). someInputSuspOrFalseVersion(A,V,T) :- inreadset(A,OI), node(T), dep(O,A,V,OI,AI,VI), not notsusp(OI,AI,VI,T). diffVersions(O,A,V) :- depTrans(O,A,V,Oi,Ai,Vi1), depTrans(O,A,V,Oi,Ai,Vi2), Vi1 != Vi2. notsusp(O,A,V,T) :- node(T), ok(A,V), ineffset(A,O), completed(A,V,T), enabled(A,T), not someInputSuspOrFalseVersion(A,V,T), not diffVersions(O,A,V). %%%% % % check that all current states of input objects at $t$ of an activity $a$ are not suspected to be % infected and have correct versions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% someCurrInputSuspOrUnfixed(A,T) :- inreadset(A,OI), node(T), cversion(OI,AI,VI,T), not notsusp(OI,AI,VI,T). someCurrInputSuspOrUnfixed(A,T) :- inreadset(A,OI), node(T), cversion(OI,AI,VI,T), notsusp(OI,AI,VI,T), not rightVersion(A,OI,AI,T). %%%% DEPENDENCIES % % dep relation shows dependencies between objects % this relation is transitivie % dependencies are effects of $do$ actions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% dep(Oo,Ao,T1,Oi,Ai,Vi) :- do(Ao,T1), ineffset(Ao,Oo), inreadset(Ao,Oi), cversion(Oi,Ai,Vi,T1). depTrans(Oo,Ao,Vo,Oi,Ai,Vi) :- dep(Oo,Ao,Vo,Oi,Ai,Vi). depTrans(Oo,Ao,Vo,Oi2,Ai2,Vi2) :- depTrans(Oo,Ao,Vo,Oi1,Ai1,Vi1),depTrans(Oi1,Ai1,Vi1,Oi2,Ai2,Vi2). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% PROPERTIES OF ACTIVITIES %%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% OK status of activities % % the diagnosis provides information about -ok activities % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -ok(A,T) :- failure(A,T). -ok(A,T2) :- activity(A), node(T2), -ok(A,T1), next(T1,T2), not substituted(A,T2), not isTransFaulty(A,T1). ok(A,T2) :- activity(A), node(T2), not -ok(A,T2). %%%% ENABLED activities % % an activity is enabled if it is placed on the branch which was correctly truesignaled % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% notEnabled(A,T) :- xedges(A,O), cversion(O,X,V,T), not value(O,X,V,truesignaled,T). notEnabled(A,T) :- xedges(A,O), cversion(O,X,V,T), value(O,X,V,truesignaled,T), not notsusp(O,X,V,T). enabled(A,T) :- node(T), activity(A), not notEnabled(A,T). %%%% SKIPPED activities % % an activity is skipped (must not be executed) if it is placed % on the branch which was correctly falsesignaled % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% skipped(A,T) :- node(T), xedges(A,O), cversion(O,X,V,T), value(O,X,V,falsesignaled,T), notsusp(O,X,V,T). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% DO ACTION %%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% PRE-CONDITIONS % % an activity can be executed if there is a slot for this execution, % all its input objects are in ok state, % and if % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% do(A,T) v -do(A,T) :- node(T), doAt(A,T), ok(A,T), enabled(A,T), not someCurrInputSuspOrUnfixed(A,T), not goal_reached(T), not impossible(a,T). %%%% POST-CONDITIONS % % after executing 1)an activity it is considered as completed % 2)old value of all ouput objects are stored in vbe relation % 3)objects in effect set become new versions of object states % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% completed(A,T1,T2) :- do(A,T1), next(T1,T2). completed(A,V,T2) :- completed(A,V,T1), next(T1,T2). vbe(Ao,T1,Oo,Ax,Vx) :- do(Ao,T1), ineffset(Ao,Oo), cversion(Oo,Ax,Vx,T1). cversion(Oo,A,T1,T2) :- do(A,T1), next(T1,T2), ineffset(A,Oo). -cversion(Oo,AX,VX,T2) :- do(A,T1), next(T1,T2), ineffset(A,Oo), cversion(Oo,AX,VX,T1). cversion(O,A,V,T2) :- cversion(O,A,V,T1), next(T1,T2), not -cversion(O,A,V,T2). %%%% SIGNALING BRANCHES % % executing a choosing block activity causes signaling of its branches (truesignaled or falsesignaled) % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% check if inputs during this execution differ from the old one % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% notSameInputsOfActionAt(A,T2,T1) :- xor(A), doAt(A,T2), inreadset(A,O), cversion(O,AE,VE,T2), completed(A,T1,T2), dep(_,A,T1,O,AF,VF), AE != AF. notSameInputsOfActionAt(A,T2,T1) :- xor(A), doAt(A,T2), inreadset(A,O), cversion(O,AE,VE,T2), completed(A,T1,T2), dep(_,A,T1,O,AF,VF), VE != VF. sameInputsOfActionAt(A,T2,T1) :- xor(A), doAt(A,T2), completed(A,T1,T2), not notSameInputsOfActionAt(A,T2,T1). actionSameInputsExists(A,T2) :- node(T1), sameInputsOfActionAt(A,T2,T1). %%%% CASE if values are different % % in this case left branch in the left time point must be truesignaled % and the right branch in the right time point must be truesignaled % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% value(O1,A,T0,truesignaled,T1) :- next(T0,T1), next(T0,T2), leftrightnexts(T1,T2), not actionSameInputsExists(A,T0), do(A,T0), xor(A), ineffset(A,O1), leftright(O1,_). value(O2,A,T0,truesignaled,T2) :- next(T0,T1), next(T0,T2), leftrightnexts(T1,T2), not actionSameInputsExists(A,T0), do(A,T0), xor(A), ineffset(A,O2), leftright(_,O2). %%%% FALSE signaling % % if one choosing block variable was signaled to true than the second % one must be signaled to false % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% value(O1,A,T0,falsesignaled,T) :- value(O2,A,T0,truesignaled,T), xor(A), ineffset(A,O1),ineffset(A,O2), O1 != O2. %%%% CASE if values are the same as it was at some execution time previously % % then all variables must be signaled in the same way in both new time branches % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% value(O,A,T1,truesignaled,T2) :- next(T1,T2), do(A,T0), xor(A), sameInputsOfActionAt(A,T1,T0), value(O,A,T0,truesignaled,T1). %%%% INERTIA % % true/false signaling is an inertial property (it stay the same in all subsequent time points % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% value(O,X,V,Val,T2) :- value(O,X,V,Val,T1), next(T1,T2). %%%% IMPOSSIBLE % % the time point is impossible (and not be analysed) if an appropriate branch of a choosing block % was correctly falsesignaled during the initial workflow execution % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% impossible(T2) :- doAt(A,T1), next(T1,T2), next(T1,T3), leftrightnexts(T2,T3), ineffset(A,O), leftright(O,_), notsusp(O,A,TX,T2), cversion(O,A,TX,T2), value(O,A,TX,falsesignaled,T2). impossible(T3) :- doAt(A,T1), next(T1,T2), next(T1,T3), leftrightnexts(T2,T3), ineffset(A,O), leftright(_,O), notsusp(O,A,TX,T3), cversion(O,A,TX,T3), value(O,A,TX,falsesignaled,T3). %%%% INERTIA % % impossible is an inertial property (it stay the same in all subsequent time points % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% impossible(a,T2) :- next(T1,T2), impossible(a,T1). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% COMPENSATE ACTION %%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% PRE-CONDITIONS % % an objects effected by an activity can be compensated if there is a slot for this compensation % there we no other executions of this activity previously % and if all required objects are in appropriate states. % A state of on object can be considered as appropriate if the last activity which effected % this object is exactly the activity which will be compensated (one step back compensation) % or simply if it is compensatable (always compensatable case). % impossible time points can be excluded to make the reasoning process faster % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% someCurrMissingOfComp(A,O,T) :- lastCompleted(A,V,T), ineffset(A,O), cversion(O,Ax,Vx,T), Ax != A. someCurrMissingOfComp(A,O,T) :- lastCompleted(A,V,T), ineffset(A,O), cversion(O,Ax,Vx,T), Ax = A, Vx != V. completedAgainLater(A,T1,T):- completed(A,T1,T), completed(A,T2,T), before(T1,T2). lastCompleted(A,V,T) :- completed(A,V,T), not completedAgainLater(A,V,T). comp(A,V,O,T) v -comp(A,V,O,T) :- compAt(A,O,T), lastCompleted(A,V,T), alwaysComp(A,O), not impossible(a,T). comp(A,V,O,T) v -comp(A,V,O,T) :- compAt(A,O,T), lastCompleted(A,V,T), oneBackComp(A,O), not someCurrMissingOfComp(A,O,T), not impossible(a,T). %%%% POST-CONDITIONS % % compensation of an activity restores the old states of objects which they had before the execution of this activity % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% cversion(O,Ai,Vi,T2) :- comp(A,V,O,T1), next(T1,T2), vbe(A,V,O,Ai,Vi). -cversion(O,Ax,Vx,T2) :- comp(A,V,O,T1), next(T1,T2), cversion(O,Ax,Vx,T1). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% SUBSTITUTE ACTION %%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%% PRE-CONDITIONS % % an activity can be substituted if there is a slot for this substitution % all activities which are not ok at some time point get a subsAt before doAt. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% subs(A,T) v -subs(A,T) :- subsAt(A,T), not impossible(a,T). %%%% POST-CONDITIONS % % activity is considered as substituted (affects its ok / -ok state at appropriate time points) % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% substituted(A,T2) :- subs(A,T1), next(T1,T2). %%%% INPUT FROM DIAGNOSIS % % the diagnoser provides only names of activities which are considered to be faulty % time points of their execution must be restrored from the execution logs % this is the case where activities were executed at most once, e.g. no diagnosis of % previously repaired work flow instances % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% failure(A,T):-permanentfaulty(A), effectsObserved(A,T). failure(A,T):-transientfaulty(A), effectsObserved(A,T). isTransFaulty(A,T):-transientfaulty(A), effectsObserved(A,T). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%% REASONING GOAL %%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% true. goalReached(T) :- cversion(finished,endflow,V,T), notsusp(finished,endflow,V,T). finalNode(X) :- node(X), not fromNode(X). fromNode(X) :- next(X,Y). :- finalNode(T), not goalReached(T), not impossible(a,T). %[1:2] true?