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