CTPX: In build_requirement check if the RHS has a free variable

[jefft0]

Background: When CTPX builds a model where the LHS is a command, it has all the information needed for forward chaining to assign values to the variables in the RHS. However, CTPX can also build a model where the LHS is an imdl, called a "reuse" model. An example from hand-grab-sphere-learn is the following model which says that if a hand H is holding object X and moves, then X moves too (simplified with meaningful variable names):

mdl_move_reuse:(mdl [P0: (ti T0: T1:)] []
   (fact (imdl mdl_move [P0: (ti T0: T1:)] [H: DeltaP: P1: T2B: T2B:]) T0_cmd: T1_cmd:)
   (fact (mk.val X: position P1:) T2: T3:))
[]
   T2:(add T0 100ms)
   T3:(add T1 100ms)
[]
   T0:(sub T2 100ms)
   T1:(sub T3 100ms)
   T0_cmd:(sub T2 80ms)
   T1_cmd:(sub T3 100ms)

mdl_move_reuse_req:(mdl [] []
   (fact (icst cst_same_position [] [H: X: P0:]) T0: T1:)
   (fact (imdl mdl_move_reuse [P0: (ti T0: T1:)] [H: DeltaP: P1: T2B: T2B: X:]) T0: T1:))

Here, we are concerned with forward chaining as follows. cst_same_position is instantiated with hand H holding object X at position P0. This matches the LHS of the requirement model mdl_move_reuse_req which uses the RHS to create the requirement for mdl_move_reuse. (Note that the requirement has X, discussed below.) Later in the same frame, the move command fires to move hand H from P0 to P1, and creates the imdl (imdl mdl_move [P0: (ti T0: T1:)] [H: DeltaP: P1: T2B: T2B:]). This matches the LHS of model mdl_move_reuse whose RHS predicts the new position of the object (mk.val X: position P1:).

How does AERA assign the variables for X and P1 (during forward chaining)? The new position P1 comes directly from the LHS imdl which contains P1. The value for X comes from the requirement created by the RHS of mdl_move_reuse_req. This has a value because it came from the icst on the requirement model's LHS.

In summary, all of the variables on the RHS of mdl_move_reuse are mentioned in other places where they can be bound with a value. However if a variable is not mentioned in other places, it is called a "free variable". If the RHS has a free variable then the prediction made from the RHS will have an unbound variable, which we don't want. Consider the following reuse model created by CTPX:

mdl_displace_reuse:(mdl [P0: (ti T0: T1:)] []
   (fact (imdl mdl_displace [P0: (ti T0: T1:)] [H: DeltaP: T2B: T2B:]) T0_cmd: T1_cmd:)
   (fact (mk.val X: position P1:) T2: T3:))
[]
   T2:(add T0 100ms)
   T3:(add T1 100ms)
[]
   T0:(sub T2 100ms)
   T1:(sub T3 100ms)
   T0_cmd:(sub T2 80ms)
   T1_cmd:(sub T3 100ms)

mdl_displace_reuse_req:(mdl [] []
   (fact (icst cst_same_position [] [H: X: P0:]) T0: T1:)
   (fact (imdl mdl_displace_reuse [P0: (ti T0: T1:)] [H: DeltaP: T2B: T2B: X:]) T0: T1:))

This is very similar except that mdl_displace does not predict the new position of the hand. It only predicts that hand will not be at position P0 after a displacement. (mdl_displace has an anti-fact on the RHS which doesn't have P1. SIDENOTE: Instead of this pull request, a solution could be for CTPX to handle models that have an anti-fact on the RHS in a special way, for example in this case to predict that the object X will not be at P0.) Therefore, when the model fires it produces the imdl (imdl mdl_displace [P0: (ti T0: T1:)] [H: DeltaP: T2B: T2B:]). This is similar to the imdl above for mdl_move except that there is no P1. The RHS of the reuse model is (mk.val X: position P1:) but in this case P1 is a free variable. A prediction made from the RHS of this reuse model would have an unbound variable, which we don't want. When CTPX creates a model like this, we need to detect it and discard the model.

When CTPX builds the models, it first builds a causal model m0, then calls the method CTPX::build_requirement to build the related requirement model m1. This pull request updates this method as follows to check if the RHS of m0 has a free variable.

1. Iterate through the variables of the RHS of m0. In the example above these are X and P1. (We ignore the timing variables like T2 and T3).
2. Check if the variable is mentioned in the LHS of m0. In the example above, this is the reused imdl such as (imdl mdl_displace [P0: (ti T0: T1:)] [H: DeltaP: T2B: T2B:]). If it is mentioned then it is not a free variable, so proceed to keep the model.
3. Otherwise, check if the variable is mentioned elsewhere in m0, most notably in the assignment guards. (This is not the case in the examples above.) If it is mentioned then it is not a free variable, so proceed to keep the model.
4. Otherwise, find the variable in the exposed variables of the requirement on the RHS of m1, then check if this variable is mentioned in the LHS of m1. In mdl_displace_reuse_req above, the exposed variables are [H: DeltaP: T2B: T2B: X:]. Note that X is also mentioned in the icst on the LHS, but P1 is not in the exposed variables (nor mentioned in the LHS). If the variable is mentioned in the exposed args and also in the LHS of m1 then it is not a free variable, so proceed to keep the model.
5. Otherwise, it is a free variable so return false which discards the model.

If you are still following, there is one more point to clarify. In the examples above we use meaningful variable names like X. But CTPX uses variables like v8 and v9. Furthermore, suppose we are checking variable v9 from m0. The corresponding variable in the exposed variables of m1 may be different, such as v8. Therefore we use the utility function get_ihlp_exposed_args_position which performs this mapping.

[Leo-Nogismus]

Nice catch! I'm just pinging @arashsheikhlar because I think he should have a look at this. He could do a similar check with his created composite states and requirement models to see whether there is a variable mismatch between his newly created requirement model and the causal model that it instantiates.