trunk/verif/Spin/Test/leader.ltl

   1 #define elected         (nr_leaders >  0)
   2 #define noLeader        (nr_leaders == 0)
   3 #define oneLeader       (nr_leaders == 1)
   4
   5         /*
   6          * Formula As Typed: <>[]oneLeader
   7          * The Never Claim Below Corresponds
   8          * To The Negated Formula !(<>[]oneLeader)
   9          * (formalizing violations of the original)
  10          */
  11
  12 never {    /* !(<>[]oneLeader) */
  13 T0_init:
  14         if
  15         :: (1) -> goto T0_init
  16         :: (! ((oneLeader))) -> goto accept_S5
  17         fi;
  18 accept_S5:
  19         if
  20         :: (1) -> goto T0_init
  21         fi;
  22 accept_all:
  23         skip
  24 }
  25
  26 #ifdef NOTES
  27 Some other properties:
  28         ![] noLeader
  29         <>  elected
  30         [] (noLeader U oneLeader)
  31
  32
  33
  34
  35
  36
  37 #endif
  38 #ifdef RESULT
  39 warning: for p.o. reduction to be valid the never claim must be stutter-closed
  40 (never claims generated from LTL formulae are stutter-closed)
  41 (Spin Version 3.1.2 -- 14 March 1998)
  42         + Partial Order Reduction
  43
  44 Full statespace search for:
  45         never-claim             +
  46         assertion violations    + (if within scope of claim)
  47         acceptance   cycles     + (fairness disabled)
  48         invalid endstates       - (disabled by never-claim)
  49
  50 State-vector 200 byte, depth reached 233, errors: 0
  51      202 states, stored (402 visited)
  52      281 states, matched
  53      683 transitions (= visited+matched)
  54       36 atomic steps
  55 hash conflicts: 0 (resolved)
  56 (max size 2^19 states)
  57
  58 2.542   memory usage (Mbyte)
  59
  60 unreached in proctype node
  61         line 105, state 28, "out!two,nr"
  62         (1 of 49 states)
  63 unreached in proctype :init:
  64         (0 of 11 states)
  65
  66 real 0.13
  67 user 0.04
  68 sys  0.09
  69
  70 #endif