[Civl] Anonymous actions in refinement specification of yield procedures #972
Conversation
|
Yes, I like it. It is also easier to read the file because the atomic specification is close to the yield procedure. |
| right action {:layer 1, 9} Atomic_Mutex_Alloc() returns ({:linear} one_loc_l: One Loc) | ||
| modifies MutexPool; | ||
| yield procedure {:layer 0} Mutex_Alloc() returns ({:linear} one_loc_l: One Loc); | ||
| refines right action {:layer 1, 9} _ |
There was a problem hiding this comment.
How hard would it be to eliminate the name from the grammar in the anonymous case? My understanding is that anything can be put, which might be confusing.
There was a problem hiding this comment.
It is so hard that I don't even know how to do it right now :-). The problem is that I need to allow attributes as well as the action body both of which begin with {. Take a look at BoogiePL.atg when you find some time. In any case, the convention of using _ for the name of the anonymous action feels nice to me.
|
The current behavior is that the name of the anonymous action could be an arbitrary string (including Any preference? |
This sounds like a good solution to me that will avoids potential confusion. |
It is occasionally tedious to invent names of atomic actions whose only purpose is to serve as refinement specification of a yield procedure. This PR enables such specifications to be specified via anonymous actions. The new test file added in this PR provides a good illustration.