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