Return statements should not be allowed inside actions

[pglvdm]

A model such as

channels

a

process SmartGrid =
begin

actions

  SERVER_COMPUTE = ss : nat @ a -> (
  dcl as : seq of nat @ as := [];
    for all m in set inds as do Skip;
  return as
  ); SERVER_COMPUTE(ss + 1)

@ SERVER_COMPUTE(1)

end

is syntax and type correct but naturally it fails when you try to debug it since one should not be allowed to have a return statement inside an action!? right?

[joey-coleman]

That should be an error; I had thought we had a visitor that checked actions for returns and flagged them.

[lausdahl]

So the test case for this is:

process P2 = begin 
@ return  //error, return not allowed outside operations
end

Please provide the simplest model possible with the error. We need to add it as a test case.

[joey-coleman]

That is about as simple of a test case as you can get, but we should probably also have:

Process P3 = begin
actions
  Ret_action = return
@ Ret_action
end

just to make sure that we handle both defined actions and "body" actions correctly