e42.smv

   1 MODULE phil(leftfork, rightfork)
   2 VAR
   3         state: {none, left, both};
   4 ASSIGN
   5         init(state) := none;
   6         next(state) := case
   7                 state=none: case
   8                         leftfork=inuse: none;
   9                         TRUE: {none, left};
  10                 esac;
  11                 state=left: case
  12 --                      rightfork=inuse: left;
  13                         rightfork=inuse: {none, left};
  14 --                      TRUE: {left, both};
  15                         TRUE: {none, left, both};
  16                 esac;
  17                 TRUE: none;
  18         esac;
  19 JUSTICE state=both
  20
  21 MODULE main
  22 VAR
  23         f: array 0..6 of {free, inuse};
  24         ph0: phil(f[6], f[1]);
  25         ph1: phil(f[0], f[2]);
  26         ph2: phil(f[1], f[3]);
  27         ph3: phil(f[2], f[4]);
  28         ph4: phil(f[3], f[5]);
  29         ph5: phil(f[4], f[6]);
  30         ph6: phil(f[5], f[0]);
  31 ASSIGN
  32         init(f[0]) := free;
  33         init(f[1]) := free;
  34         init(f[2]) := free;
  35         init(f[3]) := free;
  36         init(f[4]) := free;
  37         init(f[5]) := free;
  38         init(f[6]) := free;
  39
  40         next(f[0]) := case
  41                 next(ph6.state)=both | next(ph1.state)=left | next(ph0.state)=both: inuse;
  42                 TRUE: free;
  43         esac;
  44         next(f[1]) := case
  45                 next(ph0.state)=both | next(ph2.state)=left | next(ph2.state)=both: inuse;
  46                 TRUE: free;
  47         esac;
  48         next(f[2]) := case
  49                 next(ph1.state)=both | next(ph3.state)=left | next(ph3.state)=both: inuse;
  50                 TRUE: free;
  51         esac;
  52         next(f[3]) := case
  53                 next(ph2.state)=both | next(ph4.state)=left | next(ph4.state)=both: inuse;
  54                 TRUE: free;
  55         esac;
  56         next(f[4]) := case
  57                 next(ph3.state)=both | next(ph5.state)=left | next(ph5.state)=both: inuse;
  58                 TRUE: free;
  59         esac;
  60         next(f[5]) := case
  61                 next(ph4.state)=both | next(ph6.state)=left | next(ph6.state)=both: inuse;
  62                 TRUE: free;
  63         esac;
  64         next(f[6]) := case
  65                 next(ph5.state)=both | next(ph0.state)=left | next(ph0.state)=both: inuse;
  66                 TRUE: free;
  67         esac;
  68 --This finds a deadlock
  69 LTLSPEC F(
  70         ph0.state=left &
  71         ph1.state=left &
  72         ph2.state=left &
  73         ph3.state=left &
  74         ph4.state=left &
  75         ph5.state=left &
  76         ph6.state=left)
  77
  78 --Checks starvation
  79 CTLSPEC AG(
  80         (EF (ph0.state=both)) &
  81         (EF (ph1.state=both)) &
  82         (EF (ph2.state=both)) &
  83         (EF (ph3.state=both)) &
  84         (EF (ph4.state=both)) &
  85         (EF (ph5.state=both)) &
  86         (EF (ph6.state=both)))