Unaccessible conditional fields in message types

[senier]

package Test is
   type M1 is
      message
         F1 : Boolean
            then F2
               if F1 = True
            then null
               if F1 = False;
         F2 : Boolean;
      end message;
   type M2 is
      message
         F3 : M1
            then null if F3_F1 = True and F3_F2 = False;
      end message;
end Test;

$ rflx check test.rflx 
Parsing test.rflx
Processing Test
test.rflx:14:43: model: error: subsequent field "F3_F2" referenced

[senier]

This is not strictly a bug. The resulting substituted message M2 is:

type M2 is
   message
      F3_F1 : Boolean
         then F3_F2
            if F3_F1 = True
         then null
            if F3_F1 = False
               and F3_F1 = True
               and F3_F2 = False;
      F3_F2 : Boolean
         then null
            if F3_F1 = True
               and F3_F2 = False;
   end message

The replacement algorithm adds the condition present between F3 and Final to every edge to Final present in M1. Consequently, the condition must be compatible with all those edges an mention no fields that come after the first of those transitions. While the reason is clear, this is a usability issue as well as a sever limitation.

Idea: Prune edges with conditions that are statically false (like the second condition of F3_F1 in the above example) when merging messages.

[treiher]

Idea: Prune edges with conditions that are statically false (like the second condition of F3_F1 in the above example) when merging messages.

I'm not sure if that is a good idea. I suppose there are cases which are hard to handle correctly and could lead to unexpected results (e.g., fields with no successor or no path to FINAL). Would this approach even work in general? Is a condition referencing a subsequent field detected as statically false?

Maybe it would be better to only remove all references to subsequent fields (e.g., replace all such relations by TRUE), but this is probably also not easy to implement correctly.