verif/Spin/Test/wordcount

   1 /*
   2         Example of property-based slicing.
   3         Try:    spin -A wordcount
   4         Requires Spin version 3.4 or later
   5  */
   6
   7 chan STDIN;
   8 int c, nl, nw, nc;
   9
  10 init {
  11         bool inword = false;
  12
  13         do
  14         :: STDIN?c ->
  15                 if
  16                 :: c == -1 ->   break   /* EOF */
  17                 :: c == '\n' -> nc++; nl++
  18                 :: else ->      nc++
  19                 fi;
  20                 if
  21                 :: c == ' ' || c == '\t' || c == '\n' ->
  22                         inword = false
  23                 :: else ->
  24                         if
  25                         :: !inword ->
  26                                 nw++; inword = true
  27                         :: else /* do nothing */
  28                         fi
  29                 fi
  30         od;
  31         assert(nc >= nl);
  32         printf("%d\t%d\t%d\n", nl, nw, nc)
  33 }