%
% 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?