e41.smv

   1 MODULE proc(i, s, yme, yother)
   2 VAR
   3         line: {l2, l3, l4, l7, l8};
   4 ASSIGN
   5         init(line):=l2;
   6         next(line):=case
   7                 line=l2: l3;
   8                 line=l3: l4;
   9                 line=l4: case
  10                         !(yother=0 | s!=i) : l4;
  11                         TRUE: l7;
  12                 esac;
  13                 line=l7: l8;
  14                 line=l8: l2;
  15         esac;
  16
  17 MODULE main
  18 VAR
  19         y0: 0..1;
  20         y1: 0..1;
  21         s: 0..1;
  22         proc0: proc(0, s, y0, y1);
  23         proc1: proc(1, s, y1, y0);
  24 ASSIGN
  25         next(y0):=case
  26                 proc0.line=l3: 1;
  27                 proc0.line=l8: 0;
  28                 TRUE: y0;
  29         esac;
  30         next(y1):=case
  31                 proc1.line=l3: 1;
  32                 proc1.line=l8: 0;
  33                 TRUE: y1;
  34         esac;
  35         next(s):=case
  36                 proc0.line=l3 & proc1.line=l3: {0,1};
  37                 proc0.line=l3: 0;
  38                 proc1.line=l3: 1;
  39                 TRUE: s;
  40         esac;
  41
  42 --Mutual exclusion
  43 LTLSPEC G(!(proc0.line=l7 & proc1.line=l7))
  44
  45 --Absence of starvation
  46 LTLSPEC G (F(proc0.line=l7) & F(proc1.line=l7))