sema_explicit.smv 669 Bytes
MODULE main
VAR 
  p0 : {sleep, wait, work};
  p1 : {sleep, wait, work};
  s  : {free, occ}; 
INIT p0=sleep 
INIT p1=sleep 
INIT s=free

TRANS
  p0=sleep & next(p0)=wait & next(s)=s & next(p1)=p1
  | p1=sleep & next(p1)=wait & next(s)=s & next(p0)=p0
  | p0=wait & s=free & next(p0)=work & next(s)=occ & next(p1)=p1
  | p1=wait & s=free & next(p1)=work & next(s)=occ & next(p0)=p0
  | p0=work & next(p0)=sleep & next(s)=free & next(p1)=p1
  | p1=work & next(p1)=sleep & next(s)=free & next(p0)=p0

SPEC
  AG(!(p0=work & p1=work))
SPEC
  AG(p0=wait -> AF p0=work)
SPEC
  AG(p0=wait -> EF p0=work)
SPEC
  EF(p0=work & E[p0=work U (!(p0=work) & E[!(p1=work) U p0=work])])