Issue 410: Only merge satifiable final conditions

[senier]

Ref. #410

[senier]

Reworked handling of conditions in merged messages. Data types and whole path condition are now used properly. The merged message is now filtered for dangling states, as they may become unreachable by additional constraints (which would then be detected when constructing the message).

[treiher]

I have not yet looked at the changes, but I found an issue when I tried to check a specification. Z3 seems to run forever when checking the following specification (I stopped after running it about 3 minutes on lab):

package Test is

   type M1 is
      message
         F1 : Boolean
            then F2
               if F1 = True
            then null
               if F1 = False;
         F2 : Boolean
            then null
               if F2 = True;
      end message;

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

end Test;

[senier]

I have not yet looked at the changes, but I found an issue when I tried to check a specification. Z3 seems to run forever when checking the following specification (I stopped after running it about 3 minutes on lab):

Good catch! It's not actually a Z3 issue, but as your resulting message is empty (you outer constraint contradicts with all paths and thus all fields get pruned) the substitution algorithm is stuck in an infinite loop. Of cause we need to detect this and throw an error. Fixed in be6644e.