Support Nodes with Memory

[StefanoSoffiaUTRC]

Support nodes with memory, or starred nodes.

As already discussed over the phone, we have an open discussion to understand how nodes with memory shall be specified in COQ:

• As @miccol pointed out, this functionality can in principle be delegated to skills.
• On the other hand, it would be nice to have this functionality available directly in the BT interpreter itself because of usability (the behavior designer would otherwise have to focus on BT and the skills) and because this enables COQ to reason about the composition of BT and skills.

As for what concerns the implementation, classic functional approach to handle state is to let the semantic function (the tick function in this case) take the current state or store and return the updated state. The store is:

• Classically, a map from the variable names to the variable values. This approach would definitively work but it would also incur the additional complexity of handling disambiguation whan BT are composed.
• In order to support starred nodes, it is enough to have a boolean variable local to the node itself. For example see the proposed SMV implementation. The picture below highlights the differences between the binary sequence and the binary sequence with memory.

[miccol]

Looks good to me.

Note: I am not very familiar with the language but it is very similar to one I know (TLA+).

[barbalberto]

Is SequenceStar supported in out BT engine?
I tried with this xml

<root>
  <BehaviorTree ID="bt0001">
    <SequenceStar name="seq0001">
      <Action ID="ConditionTrue" />
      <Action ID="Action1SecondSuccess" />
    </SequenceStar>
  </BehaviorTree>
</root>

but I get the error: BT parsing error: unkown node: SequenceStar

I just updated the code.

[altacch]

Nope, starred nodes are not supported at the moment; you have to translate them manually into Fallbacks.

[StefanoSoffiaUTRC]

@altacch I do not understand the "translate them manually into Fallbacks* suggestion.
I added the smv files already in the repo the SMV formalization of the SEQUENCE/FALLBACK nodes for the simple BT semantics and also for the BT semantics with reset.

Can we have a discussion about how to extend the COQ BT interpreter so as to support these nodes at run-time as well? Do you have any idea about how to proceed?

[altacch]

I do not understand the "translate them manually into Fallbacks* suggestion.

I mean something like the discussion in Michele's book, section 1.3.2.

Can we have a discussion about how to extend the COQ BT interpreter so as to support these nodes at run-time as well? Do you have any idea about how to proceed?

This is surely going to be a major change: I don't see how to implement the functionality without adding a notion of state, either into the btree data type or inside the tick function.

In the first case we could, for instance, change the Node constructor from the current
Node: nodeKind -> string -> btforest -> btree
to something like
Node: nodeKind -> string -> btforest -> list return_enum -> btree
where the new argument is a list of return values from the previous tick. Note that this means that each tick updates the data structure (we may call it a btree_with_memory type).

Alternatively, we can add just another nodeKind, say SequenceStar, and manage the state by passing it as an argument to tick. At the moment I don't know which of the two ideas makes more sense.

[barbalberto]

I was aking because I wanted the robot to follow a path, so I tried with:

<root>
  <BehaviorTree ID="bt0001">
    <Sequence name="seq0001">
      <Action ID="Go_to_location_1" />
      <Action ID="Go_to_location_2" />
      <Action ID="Go_to_location_3" />
    </Sequence>
  </BehaviorTree>
</root>

With simple sequence it is not gonna work, because Go_to_location_1 will always be ticked (also after it succeeded) so as soon as the robot tries to go to location 2, it will come back at the following tick.

SequenceStar will fix this because it basically introduces memory.
Converting the previous sequence into fallback will be something like:

<root>
  <BehaviorTree ID="bt0008">
    <Sequence name="seq0008">
      <Fallback name="fb0008a">
        <Condition ID="Location1_done" />
         <Action ID="Go_to_location1" />
      </Fallback>
      <Fallback name="fb0008b">
        <Condition ID="Location2_done" />
        <Action ID="Go_to_location2" />
      </Fallback>
    </Sequence>
  </BehaviorTree>
</root>

Which basically means to move the memory inside the Condition.
This implies that each condition must be a skill (executable) that externally (wrt the BT) checks for the condition and stores the value. It shall also be cleared eventually, by who and when?

The other option I see is to to use a blackboard, but this means the blackboard becames a must have also for very trivial BTs.

I think it'll be better if memory required by the BT could be handled internally, otherwise the complexity in integration is gonna explode very quickly.

Anyway, after chatting with @miccol we agreeded to:

• for path including many waypoints I created a specialized skill (which in turns calls the basic navigation skill) which holds the memory for already accomplished steps.

• I'll start to sketch a simple blackboard (in yarp) 'cause I sense it is gonna needed anyway, and I'm waiting for SmartSoft guys to help me fixing an issue

[StefanoSoffiaUTRC]

@altacch now I understand the approach suggested. Though, as pointed out also by @barbalberto it requires the designer to explicitly think and model the flag reset logic ("It shall also be cleared eventually, by who and when?") With this in mind, please consider what I propose below.

@barbalberto and @miccol please help us understand what does the SequenceStart enable you to solve in your specific use-case. Specifically, how did you came to realize that a SequenceStar was needed instead of a plain Sequence? This might sound trivial ("I run it, and then I saw that there was an issue.") but can you think about at why it is so, what properties the action has to require the starred operator?

From what I see, the choice between e.g. Sequence and SequenceStar often depends on design decision subtleties and thus subject to misinterpretation and errors. If we can capture such subtleties with our formal analysis, then we can provide some value out of the framework we are proposing. More in general, starred operators are quite used in practice, therefore it is worth considering them in the formalization.

[barbalberto]

@StefanoSoffiaUTRC

Specifically, how did you came to realize that a SequenceStar was needed instead of a plain Sequence?

I'l try to explain it by taking 'snapshots' of the BT state in time.
At the beginning:

    <Sequence name="seq0001">
      <Action ID="Go_to_location_1" />   First tick -> retuns running
      <Action ID="Go_to_location_2" />   Not ticked yet
      <Action ID="Go_to_location_3" />   Not ticked yet
    </Sequence>

The robot moves and reaches location_1

<Sequence name="seq0001">
  <Action ID="Go_to_location_1" />   Robot arrives in location1 -> return Success
  <Action ID="Go_to_location_2" />   First tick -> returns running  ->  robot starts 
                         moving  toward location2 -> therefore **away** from location 1
  <Action ID="Go_to_location_3" />   Not ticked yet
</Sequence>

At a certain point

<Sequence name="seq0001">
  <Action ID="Go_to_location_1" />   Robot moved away from location1 -> returns Failure -> 
                             got ticked again and halts Go_to_location_2
  <Action ID="Go_to_location_2" />  Halted
  <Action ID="Go_to_location_3" />   Not ticked yet
</Sequence>

So as soon as the robot moves from location_1 to location_2 it comes back.
It is not possible that both "Go_to_location_1" and "Go_to_location_2" are success at the same time because the robot is either in location_1 or location_2.

The ratio is that as long as a "Go_to_location" is ticked, it brings the robot there, hence it prevents the robot to go elsewhere.

By using the sequenceStar my understanding is that once the first go_to_location return succes, it is not ticked anymore, freeing the robot to reach another location.

[miccol]

In the sequence star node, the memory is inside the node. If we go with the translation "sequence+fallback+memory nodes" we need a way to store those memory nodes somewhere.

[altacch]

Let me point out a subtlety I was thinking about in the last few days.
With the current interpreter, as pointed out by @barbalberto , the only way to have a persistent state between ticks is to implement an ad-hoc Condition node (e.g. Location1_done). Now, the code in this node can do two very different things:

• check if the skill Go_to_location1 is done and always return Success from that point on,
• check directly the physical state of the robot each time it is called.

Now if we introduce nodes with memory inside the interpreter, we add another "source" of state in a BT execution. Since the BT interpreter is oblivious to the physical state of the robot, this new source of state can only be of the first (i.e., "cache") kind. I am wondering if this can cause problems and, if so, how to avoid them.

[barbalberto]

Just to clarify, I'm not suggesting to have generic nodes (leaves) with memory, only to have the SequenceStar.

With @miccol we are building the black-board, so that conditions can store their memory in. Better, the skills can write into the black-board, the BT can tick a condition and get a fresh value from the blackboard.

At first we can emulate the Star with "sequence+fallback+condition+blackboard" but it is cumbersome, not efficient and difficult to maintain.

At the end, a generic condition ("is_the_robot_happy?") will need either a specialized skill or the blackboard, but the "internal logic of BT", like SequenceStar shall not rely on external process as the black-board.

[StefanoSoffiaUTRC]

@barbalberto your example is clear. Moreover, @miccol BT engine supports starred operators, and Davide Faconti's Groot supports them as well.

On the other hand, I understand that as part of CARVE there is a trade-off between the number of features supported by the interpreter and the formality of the approach. So:

1. @altacch let us try to reason together about what would be needed in COQ to implement these nodes. Last week I pushed a reference implementation in SMV (the model checker) for both the basic and reactive BT semantics. I'll try to push a simplified proof-of-concept in COQ asap.
2. Let me understand if I can rephrase @barbalberto example so as to suggest that the formal analysis can help the designer to early pinpoint starred/non-starred errors. This would contribute to bring evidence to the CARVE thesis, i.e. the value of formal methods to behavior designers.

[StefanoSoffiaUTRC]

@altacch please checkout this branch.

I added a BT_binary_with_memory to experiment our ideas.
Currently there is a lot of repetition in the tick function. Not sure about how to remove it, maybe you can continue from here.

[StefanoSoffiaUTRC]

@altacch and @barbalberto, I would like to write unit tests to exercise the Caml code extracted from COQ. What do you suggest?

E.g. to test the reference SMV I created the smv/run_all_verification.py which includes the specification of the unit tests and exercises them by invoking the external executable nuXmv and checking its output.

[altacch]

I think we should make our experiments directly on the arbitrary-branching implementation of BTs, since all the infrastructure (tests included) is geared towards this case.
Sorry for not being of help at the moment; I may be able to allocate some time to the problem tomorrow.