Cross-Features possibility determination

[Chris Ortiz]

Hi TLAplus google group,

Is it correctly to say that the CONSTANT and VARIABLES of SpecA (which describe FeatureA) are the Domain of Discourse of SpecA (or FeatureA)? If I have another FeatureB which described in SpecB, to say that FeatureA can be cross-featured with FeatureB, then there should be atleast a StepA and StepB that Intersect (logical AND) a stateC of FeatureA and FeatureB with Fairness that to cross from SpecA to SpecB, then there should be a Fairness condition that StepB should eventually happen when it is possibly enabled at stateC. On that stateC, SpecB should have the same Domain of Discourse common also from SpecA (maybe with Refinement Mapping if needed).

I am finding a way given 2 specs, to immediately determine if they can be cross-featured to guide our implementation testing. I am thinking if I have a TLA+ parser that parses 2 specs (SpecA and SpecB) of their CONSTANT, VARIABLES, and WITH (refinement mapping) and found common Domain of Discourse, and then TLC find common stateC between them, and then find the steps from SpecA and SpecB that are ENABLED from the stateC. Then these steps is something we can target for Fairness Condition to make sure we can cross-feature SpecA to SpecB.

I just like to know if my reasoning is correct.

Thanks,

Zitro