Non-null state accepted as final state

[treiher]

The following session specification must not be accepted, as the final state is not a null state. A final state is never executed, so it doesn't make sense to define actions or transitions for it.

package Test is

   type T is mod 2 ** 16;

   type Message is
      message
         F : T;
      end message;

   generic
      Input : Channel with Readable;
      Output : Channel with Writable;
   session Validator with
      Initial => Validate,
      Final => Forward
   is
      Message : Test::Message;
   begin
      state Validate
      is
      begin
         Input'Read (Message);
      transition
         goto Forward
            if Message'Valid
         goto Validate
      end Validate;

      state Forward
      is
      begin
         Output'Write (Message);
      transition
         goto Validate
      end Forward;
   end Validator;

end Test;

[senier]

This raises the question what we do with sessions that don't end (e.g. a proxy)?

[treiher]

I think we should implement #700 where we decided to remove the need for an explicit definition of a final state.

[senier]

I forgot about #700 - I agree.