trunk/verif/Spin/Test/mobile2.ltl

   1 #define p       in?[red]
   2 #define q       out?[red]
   3 #define r       (BS[a_id]@progress || BS[p_id]@progress)
   4
   5         /*
   6          * Formula As Typed: (![]<>(r)) -> [](<>p -> <>q)
   7          * The Never Claim Below Corresponds
   8          * To The Negated Formula !((![]<>(r)) -> [](<>p -> <>q))
   9          * (formalizing violations of the original)
  10          */
  11
  12 never {    /*  !((![]<>(r)) -> [](<>p -> <>q))  */
  13 T0_init:
  14         if
  15         :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
  16         :: (! ((q)) && ! ((r))) -> goto T0_S13
  17         :: (! ((q)) && (p)) -> goto T0_S26
  18         :: (! ((q))) -> goto T0_S32
  19         :: (! ((r))) -> goto T0_S44
  20         :: (1) -> goto T0_init
  21         fi;
  22 accept_S8:
  23         if
  24         :: (! ((q)) && ! ((r))) -> goto T0_S8
  25         fi;
  26 T0_S8:
  27         if
  28         :: (! ((q)) && ! ((r))) -> goto accept_S8
  29         fi;
  30 T0_S13:
  31         if
  32         :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
  33         :: (! ((q)) && ! ((r))) -> goto T0_S13
  34         fi;
  35 T0_S26:
  36         if
  37         :: (! ((q)) && ! ((r))) -> goto accept_S8
  38         :: (! ((q))) -> goto T0_S26
  39         fi;
  40 T0_S32:
  41         if
  42         :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
  43         :: (! ((q)) && ! ((r))) -> goto T0_S13
  44         :: (! ((q)) && (p)) -> goto T0_S26
  45         :: (! ((q))) -> goto T0_S32
  46         fi;
  47 T0_S44:
  48         if
  49         :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
  50         :: (! ((q)) && ! ((r))) -> goto T0_S13
  51         :: (! ((r))) -> goto T0_S44
  52         fi;
  53 accept_all:
  54         skip
  55 }
  56
  57 #ifdef NOTES
  58 Use Load to open a file or a template.
  59 #endif
  60 #ifdef RESULT
  61 warning: for p.o. reduction to be valid the never claim must be stutter-closed
  62 (never claims generated from LTL formulae are stutter-closed)
  63 (Spin Version 3.2.4 -- 16 October 1998)
  64         + Partial Order Reduction
  65
  66 Full statespace search for:
  67         never-claim             +
  68         assertion violations    + (if within scope of claim)
  69         acceptance   cycles     + (fairness disabled)
  70         invalid endstates       - (disabled by never-claim)
  71
  72 State-vector 96 byte, depth reached 1944, errors: 0
  73    16191 states, stored (18994 visited)
  74    46781 states, matched
  75    65775 transitions (= visited+matched)
  76       16 atomic steps
  77 hash conflicts: 1713 (resolved)
  78 (max size 2^19 states)
  79
  80 Stats on memory usage (in Megabytes):
  81 1.684   equivalent memory usage for states (stored*(State-vector + overhead))
  82 0.998   actual memory usage for states (compression: 59.24%)
  83         State-vector as stored = 54 byte + 8 byte overhead
  84 2.097   memory used for hash-table (-w19)
  85 0.240   memory used for DFS stack (-m10000)
  86 3.464   total actual memory usage
  87
  88 unreached in proctype CC
  89         line 28, state 25, "-end-"
  90         (1 of 25 states)
  91 unreached in proctype HC
  92         line 35, state 6, "-end-"
  93         (1 of 6 states)
  94 unreached in proctype BS
  95         line 65, state 31, "-end-"
  96         (1 of 31 states)
  97 unreached in proctype MS
  98         line 78, state 14, "-end-"
  99         (1 of 14 states)
 100 unreached in proctype System
 101         line 98, state 13, "-end-"
 102         (1 of 13 states)
 103 unreached in proctype Out
 104         line 105, state 7, "-end-"
 105         (1 of 7 states)
 106
 107 #endif