Skip to content
Snippets Groups Projects
Commit 01075315 authored by Justin Loew's avatar Justin Loew
Browse files

Add ability to count the items in a task queue

parent c5be37d8
No related branches found
No related tags found
No related merge requests found
......@@ -24,10 +24,14 @@ mod TASK-QUEUE is
op mt : -> TaskQueue .
op __ : TaskQueue TaskQueue -> TaskQueue [ctor assoc id: mt] .
op insert : TaskQueue Task -> TaskQueue [left id: mt] .
op count : TaskQueue -> Nat .
var Q : TaskQueue . var J K : Task .
vars N M : Oid . vars T1 T2 : Nat .
ceq insert(Q J, K) = insert(Q, K) J if K < J .
eq insert(Q J, K) = Q J K [owise] .
eq count(mt) = 0 .
eq count(Q J) = s(count(Q)) .
endm
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment