-- 1 #######################################################################
-- 2 ##########################QUEUE_FCN.CSP################################
-- 3 #######################################################################
-- CopyRight(r) CURUPIRA Inc, 10/2000, version 1
-- Adolfo Duran - aad@cin.ufpe.br
-- Leonardo Freitas - ljsf@cin.ufpe.br
-- THIS FILE IS BEST VIEWED WITH TABSTOPS = 4
-- 10 %%%%%%%%%%%%%%%%%%%%%%%%%%INCLUDE SECTION%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-- This file does not depend on any other.
-- 14 %%%%%%%%%%%%%%%%%%%%%%%%%%DOCUMENTATION SECTION%%%%%%%%%%%%%%%%%%%%%%%%%%%
-- Auxiliary timmed queue functions
-- get(time, sequence) = (x=operation,l=length,d=data).
--
-- This function will "get" the tuple of s (returned as a sequence for the guard
-- test - there exist a better way ?) where the time is t or return a null sequence
-- if such tuple does not exists in s.
--
--
-- insert_queue(tuple,sequence) = ^sequence
-- where tuple = (x=operation,l=length,d=data,t=time).
--
-- This function will "insert" the given tuple into queue in such a way that
-- when we try to insert a duplicate tuple for the time t, it will just replace
-- the elements which forms the tuple information, (x,l,d) for this time t,
-- meaning a tuple update.
-- extract_queue(time,sequence) = sequence except items of time
--
-- This "extract" function will extract the selected item from the queue,
-- that is the one marked to be executed at the given time.
-- One should also note that there exists a precondition in the queue
-- construction (see insert_queue above) that states:
--
-- "There MUST exists at most one tuple at time t."
--
-- extract_queue(t,s) = < (x,l,d,t') | (x,l,d,t') <- s, ( t != t' ) >
--
-- We are uncertain about the expressiveness of this construction will
-- behave as we might expect, so we came up with another one:
--
-- retrieve_queue(t,s) = < (x,l,d,t') | (x,l,d,t') <- s, not check(t,s) >
--
-- check(t,<>) = false
-- check(t,<(x,l,d,t')>^s) = ( t == t' ) or check(t,s)
--
-- After all we found other (simple) solution:
--
-- Note: If the stated precondition does not hold the extract function will
-- extract all repetitions of t. (only t != t', please).
-- We can simple eliminate this redundancy check by just avoiding
-- the call to extract_queue(s) and just return s.
--
-- If we found problems in the above syntax we can try this other way
--
-- getT((x,l,d,t)) = t
-- get(^s, t) =
-- 64 %%%%%%%%%%%%%%%%%%%%%%%%%%IMPLEMENTATION SECTION%%%%%%%%%%%%%%%%%%%%%%%%%%
MAX_QUEUE_SIZE = 2
get_queue(t, <>) = <>
get_queue(t, <(x,l,d,t')>^s) = if ( t' == t ) then else get_queue(t,s)
insert_queue((x,l,d,t),<>) = <(x,l,d,t)>
insert_queue((x,l,d,t),<(x',l',d',t')>^s) =
if ( ( (#s+2) == MAX_QUEUE_SIZE ) and ( t == t' ) ) then
<(x,l,d,t)>^s
else if ( (#s+2) > MAX_QUEUE_SIZE ) then
<(x',l',d',t')>^s
else if ( t == t' ) then
<(x,l,d,t)>^s
else
<(x',l',d',t')>^insert_queue((x,l,d,t),s)
extract_queue(t, <>) = <> -- should never be used ? And for the case of an empty sequence ?
extract_queue(t, <(x,l,d,t')>) = if ( t == t' ) then <> else <(x,l,d,t')>
extract_queue(t, <(x,l,d,t')>^s) =
if ( t == t' ) then
s -- extract_queue(t,s) -- redundant check!
else
<(x,l,d,t')>^extract_queue(t,s)
extract_queue2(t, <(x,l,d,t')>^s) =
if ( t == t' ) then
extract_queue(t,s) -- redundant check!
else
<(x,l,d,t')>^extract_queue(t,s)
extract_queue3(t,s) = < (x',l',d',t') | (x',l',d',t') <- s, ( t!=t' ) >
-- 101 %%%%%%%%%%%%%%%%%%%%%%%%%%ASSERTION SECTION%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-- See the similar asserts from queue_fcn_simple_test.csp
-- 105 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%