KMonitor is a collection of scripts and support programs which use the KDiagnose tool and DLV to monitor plan execution. During the execution of a plan (a linear sequence A_0, ... , A_n of actions) in a non-deterministic environment we may reach some state which doesn't correspond to any of the expected trajectories.
KMonitor facilitates the execution of this plan, and calls the KDiagnose to check for these discrepancies at given checkpoints during the execution.
A formal description of discrepancies, trajectories and types of checkpointing policies can be found in paper "KMonitor - A Tool for Monitoring Plan Execution in Action Theories". The implementation is available as a .tar.gz package of Linux/i386 binaries and shell scripts. The examples used are also available for download.
The approach has been "agentized" in JADE as part of a student project.
This work is part of the project "Answer Set Programming for Reactive Planning and Execution Monitoring"
You can invoke KMonitor with the following parameters:
KMonitor PLAN BACKGROUND PLAN TRAJTYPE TRAJ POLTYPE POLICY [-i]| PLAN | File which contains the planning problem described in language K (.plan extension required) | ||||||
| BACKGROUND | File which contains the background logic for the planning problem in Datalog language (.dl extension required) | ||||||
| PLAN | File which contains the plan to diagnose (syntax as in the output of DLV) | ||||||
| TRAJTYPE |
Switch which selects how the preferred trajectories T should be generated:
| ||||||
| TRAJ | Used with previous switch | ||||||
| POLTYPE |
Switch which selects what type of checkpointing policy is used:
| ||||||
| POLICY | File which contains the checkpointing policy, described in the DLV language | ||||||
| -i | If present, enables `interactive' mode -- after each discrepancy user can choose whether abort, continue or switch back to batch mode. |
STATE 0: on(x,table), on(a,table), on(p,a), on(r,i), on(i,table), on(s,table) STATE 1: on(x,table), on(a,table), on(p,a), on(r,p), on(i,table), on(s,table) STATE 2: on(x,table), on(a,table), on(p,a), on(r,p), on(i,s), on(s,table) STATE 3: on(x,table), on(a,table), on(p,a), on(r,i), on(i,s), on(s,table) STATE 4: on(x,table), on(a,table), on(p,r), on(r,i), on(i,s), on(s,table) STATE 5: on(x,table), on(a,p), on(p,r), on(r,i), on(i,s), on(s,table) STATE 6: on(x,table), on(a,p), on(p,r), on(r,i), on(i,s), on(s,table)
In this policy, we define checkpoints as the states after moving a `heavy' block, where heavy blocks are blocks p, r and s.
The checkpointing policy definition file static.cp is as follows:
#maxint=20.
checkpoint(TT) :- move(X,Y,T),heavy(X),#succ(T,TT).
heavy(p).
heavy(r).
heavy(s).
Evaluation of the policy yields the following checkpoints: 1,3,4 and
6. During the plan execution monitoring, the states at these stages
are checked and, if a discrepancy is detected, then a diagnosis is computed.
In this policy, checkpoints are states after moving a block, in which this block didn't land on its intended target location.
The checkpointing policy definition file dynamic.cp is as follows:
#maxint=20.
checkpoint(TT) :- now(TT), move(X,Y,T),not on(X,Y), #succ(T,TT).
The stages which qualify for a checkpoint are 1,4 and 6. These are diagnosed and discrepancy can be
found at stage 4. Here is the sample output of kmonitor:
> Calling DLV to check whether to do a checkpoint at stage 0
> Calling DLV to check whether to do a checkpoint at stage 1
> Checkpoint found, calling diagnosis
No error at stage 1.
> Calling DLV to check whether to do a checkpoint at stage 2
> Calling DLV to check whether to do a checkpoint at stage 3
> Calling DLV to check whether to do a checkpoint at stage 4
> Checkpoint found, calling diagnosis
Error at stage 4 - Point of failure at stage 3
Point(s) of failure at stage 3;
Failure state(s):
istime(3), occupied(a), occupied(i), occupied(s), on(x,table), on(p,a), on(a,table),
-on(r,table), -on(r,x), -on(r,p), -on(r,a), -on(r,r), on(r,i), -on(r,s), on(i,s),
on(s,table), supported(x), supported(p), supported(a), supported(r), supported(i),
supported(s)
In this policy, the current stage is a checkpoint if the move of a block did not work out as in the plan (i.e., the block just landed on a different location). Furthermore, checkpointing is suspended until the next "heavy" block will be moved, if such a move is on the agenda.
The checkpointing policy definition file
sleep.cp is as follows:
#maxint=20.
checkpoint(TT) :- now(TT), move(X,Y,T), not on(X,Y), #succ(T,TT).
checkpoint(UU) :- not now(UU), move(X,Y,U), heavy(X), #succ(U,UU).
heavy(p).
heavy(r).
heavy(s).
Then the stages 1,3,4, and 6 are "suspicious," because according to the
plan, a heavy block is moved in the previous stage.
The checkpointing proceeds as follows:
> First checkpoint information found for stage 0 > Calling DLV to check whether to do a checkpoint at stage 0 > Sleeping until stage 1 > Calling DLV to check whether to do a checkpoint at stage 1 > Checkpoint found, calling diagnosis No error at stage 1. > Sleeping until stage 3 > Calling DLV to check whether to do a checkpoint at stage 3 > Sleeping until stage 4 > Calling DLV to check whether to do a checkpoint at stage 4 > Checkpoint found, calling diagnosis Error at stage 4 - Point of failure at stage 3 Point(s) of failure at stage 3; Failure state(s): istime(3), occupied(a), occupied(i), occupied(s), on(x,table), on(p,a), on(a,table), -on(r,table), -on(r,x), -on(r,p), -on(r,a), -on(r,r), on(r,i), -on(r,s), on(i,s), on(s,table), supported(x), supported(p), supported(a), supported(r), supported(i), supported(s) istime(3), occupied(a), occupied(i), occupied(s), on(x,table), on(p,a), on(a,table), -on(r,table), -on(r,x), -on(r,p), -on(r,a), -on(r,r), on(r,i), -on(r,s), on(i,s), on(s,table), supported(x), supported(p), supported(a), supported(r), supported(i), supported(s) > Sleeping until stage 6 > Calling DLV to check whether to do a checkpoint at stage 6 > Checkpoint found, calling diagnosis No error at stage 6.Try the examples above also with the -i switch (for interactive mode), and remove some of the state information ...
Created and maintained by Jan Senko