home *** CD-ROM | disk | FTP | other *** search
/ cs.rhul.ac.uk / www.cs.rhul.ac.uk.zip / www.cs.rhul.ac.uk / pub / CS375 / spec2.fdr2 < prev    next >
Text File  |  1999-02-01  |  640b  |  30 lines
  1. channel year1, year2, year3, pass, fail, graduate, prize
  2.  
  3. S = {| year1, year2, year3, pass, fail, graduate |}
  4.  
  5. C = {| pass, fail, prize |}
  6.  
  7. STUDENT = year1 -> (pass -> YEAR2 [] fail -> STUDENT)
  8. YEAR2 = year2 -> (pass -> YEAR3 [] fail -> YEAR2)
  9. YEAR3 = year3 -> (pass -> graduate -> STOP [] fail -> YEAR3)
  10.  
  11. COLLEGE = fail -> STOP [] pass -> C1
  12. C1 = fail -> STOP [] pass -> C2
  13. C2 = fail -> STOP [] pass -> prize -> STOP
  14.  
  15. SYSTEM = STUDENT [ S || C ] COLLEGE
  16.  
  17. SPECP = pass -> S1 [] fail -> SPECF
  18. S1 = pass -> S2 [] fail -> SPECF
  19. S2 = pass -> prize -> STOP [] fail -> SPECF
  20.  
  21. SPECF = pass -> SPECF [] fail -> SPECF
  22.  
  23. assert SPECP [T= SYSTEM
  24.  
  25.  
  26.  
  27.  
  28.  
  29.  
  30.