Given a list of n elements identified by a tag i, with i in 0..n-1
Given that a maintainer holds a list of priority targeting the identifiers, the first item being the most prioritized index.
When the maintainer is told to push back an id :
Then
the maintainer find the id in its list
the found item is removed from the list, the following elements are moved by one, and the removed item is put at the end of the list.
At any given time, the first item value is available at the output port.
to quickly perform the push back : there are n possible resulting lists from pushing back one of n element, that are precomputed. The selected result is pushed to the current state on pushing back one element.
Given a list of n elements identified by a tag i, with i in 0..n-1
Given that a maintainer holds a list of priority targeting the identifiers, the first item being the most prioritized index.
When the maintainer is told to push back an id :
Then
At any given time, the first item value is available at the output port.