home *** CD-ROM | disk | FTP | other *** search
/ cs.rhul.ac.uk / www.cs.rhul.ac.uk.zip / www.cs.rhul.ac.uk / pub / CS375 / scheduler.fdr2 < prev    next >
Text File  |  1999-03-05  |  1KB  |  53 lines
  1. -- The Cyclic Scheduler
  2. -- Define a constant for the largest cell number
  3. n = 5
  4.  
  5. channel start, finish, c : {0..n}
  6.  
  7. -- Define increment modulo (n+1)
  8. inc(x) = (x+1) % (n+1)
  9.  
  10. STARTCELL(i) = start.i -> c.inc(i) -> 
  11.                 (  finish.i -> c.i -> STARTCELL(i)
  12.                 [] c.i -> finish.i -> STARTCELL(i) )
  13.  
  14. WAITCELL(i) = c.i -> STARTCELL(i)
  15.  
  16. CELL(i) = if i==0 then STARTCELL(i) else WAITCELL(i)
  17.  
  18. SCHED = (|| i:{0..n} @ [ {|start.i, finish.i, c.i, c.inc(i) |} ] CELL(i) )
  19.         \ {|c|}
  20.  
  21. -- The specifications
  22.  
  23. ALT(i) = start.i -> finish.i -> ALT(i)
  24.  
  25. ALTSPEC = || i:{0..n} @ [ {|start.i, finish.i |} ] ALT(i)
  26.  
  27. CYCLE(i) = start.i -> CYCLE(inc(i))
  28.  
  29. -- The assertions
  30.  
  31. assert ALTSPEC [T= SCHED
  32. assert CYCLE(0) [T= (SCHED \ {|finish|})
  33.  
  34. -- The alternative definition of the scheduler
  35.  
  36. SCH(s,R) = (if not(union(R,{s}) == R) 
  37.             then start.s -> SCH(inc(s),union(R,{s}))
  38.             else STOP)
  39.          [] ([] i:R @ finish.i -> SCH(s,diff(R,{i})))
  40.  
  41. NEWSCHED = SCH(0,{})
  42.  
  43. -- Assertions for the new scheduler
  44.  
  45. assert ALTSPEC [T= NEWSCHED
  46. assert CYCLE(0) [T= (NEWSCHED \ {|finish|})
  47.  
  48. -- Trace equivalence of the two schedulers
  49.  
  50. assert SCHED [T= NEWSCHED
  51. assert NEWSCHED [T= SCHED
  52.  
  53.