Multiple Systems

In a situation where the SYS process is defined for a mission that has has sensor processes that may trigger different behaviors, verification proceeds by starting a SYS that consists of only the TR processes such as Robot etc, and those parts of the nonTR mission process that are active when the mission starts.

Example

For example, consider that SYS=(Robot1 | Robot2 | Mission) and Mission = (P1; Q1 | P2;Q2).

The mission is a non TR process, and there is only one non TR process allowed in a SYS curently.

The mission processes has two sequential chains (processes in sequence) in parallel. If P1 and P2 are sensory processes - processes that monitor some sensory condition and terminate when it holds, then P1 can trigger the action Q1 and P2 the action Q2.

Verification proceeds as follows.

SYS0 is defined to be (Robot1 | Robot2 | P1 | P2).

That is, all the TR processes and those parts of the nonTR process that execute first. A trigger vector is defined within VIPARS whose entries are the goals that need to be monitored for P1 and P2 to achieve completion. When TSS reports one or both of these are achieved, then VIPARS will consider what SYS to make next.

Suppose that P1 had terminated and P2 had not. Then then next SYS is SYS1=(Robot1 | Robot2 | Q1 | P2 ) and the trigger vector monitors the termination of Q1 and P2. Suppose that P2 had terminated and P1 had not. Then the next SYS is SYS1=(Robot1 | Robot2 | P1 | Q2 ) Suppose they both had terminated, then the next SYS is SYS1=(Robot1 | Robot2 | Q1 | Q2) If neither terminate of coursse, then TSS just continues until one or both do or there is a timeout.

Let us consider one of these cases in more details, SYS1=(Robot1 | Robot2 | Q1 | P2). If the trigger vector reports when TSS has ended that Q1 has ended but not P2, then SYS2=(Robot1 | Robot 2 | P2) and only P2 is monitored. Of course, P2 might end instead of P1, Q1, or P1 and Q2 might both end.

Continuing the example, SYS2=(Robot1 | Robot2 | P2) if P2 ends, then SYS3=(Robot1 | Robot 2 | Q2) and when Q2 end, since there are no nonTR processes left, the problem is considered done.

Internal data structures

VIPARS keeps a number of internal data structures to do the houskeeping described above. These data structures are in sysProb.h/.cpp, and the main routine thathandles this reasoning is called reMakeMultiStepProb. Each sequential chain in the nonTR process is called a branch, numbered from 0 in the left/top. The peel number (peelNum) is the index into the sequential chain, starting at 0 as the first process.

So SYS = (Robot1|Robot2|P1;Q1|P2;Q2) has two branches each of which has two processes (max peel = 2). Branch 1 peel number 0 is P2 and branch 1 peel number 1 is Q2.

So the current SYS (SYS0, SYS1 etc) always is made by taking the current peel number for each branch. When the last process in a chain has terminated the peel number for that branch is set to a large number 9999.

The list of goals (lhsGoal,rhsGoal) printed in the output log is the list of termination conditions for each branch. There is one boolean trigger entry per goal, and this is returned from TSS and says which processes have terminated (true=> the process has terminated). However, some branches may not have termination conditions. Thus, the array trigger2branch tells for each trigger which branch it refers to.

Disabling composition

Consider SYS=( A # B # C | P1;Q1 ). In this case if A terminates, then it is considered to cause B and C to terminate as well - even when B and C do not have any goal conditions being monitored. This latter case is handled by using an array of booleans isTC that indicates whether each branch is a # (min) or | (max) style parallel composition. isTC is true iff the branch is a min style composition (#). If a trigger is seen to be true (eg A's trigger, which would be trigger 0, since A is branch 0, peel 0), then it is checked whether branch 1 (which is B) posted a goal to the list of goals or not. If it did, that means there is a trigger vector entry for it, and it then is simply set to true, then same as if had come from TSS as true. If there is no goal, then an extra entry is inserted into the trigger vector for B, and it is set to true.

Consider the case SYS=( P1;Q1 # P2;Q2). When P1 terminates it does NOT cause P2;Q2 to terminate, because';' binds tighter than # or |.

-- (c) Fordham University Robotics and Computer Vision