/**
@Begin
@Global_define:
- @DeclareVar:
+ @DeclareStruct:
typedef struct tag_elem {
Tag id;
unsigned int data;
data = _data;
}
} tag_elem_t;
-
+ @DeclareVar:
spec_queue<tag_elem_t> queue;
Tag tag;
@InitVar:
@Action:
# __ID__ is an internal macro that refers to the id of the current
# interface call
- @Code:
__sequential.queue.enqueue(tag_elem_t(__ID__, val));
@End
*/
@Commit_point_set: Dequeue_Success_Point
@ID: __sequential.queue.peak().tag
@Action:
- @Code:
unsigned int _Old_Val = __sequential.queue.dequeue().data;
@Post_check:
_Old_Val == __RET__