trunk/verif/Spin/Test/mobile1.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_S17
  17         :: (! ((q)) && (p)) -> goto T0_S44
  18         :: (! ((q))) -> goto T0_S58
  19         :: (! ((r))) -> goto T0_S91
  20         :: (1) -> goto T0_init
  21         fi;
  22 accept_S8:
  23         if
  24         :: (! ((q)) && ! ((r))) -> goto accept_S8
  25         fi;
  26 T0_S17:
  27         if
  28         :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
  29         :: (! ((q)) && ! ((r))) -> goto T0_S17
  30         fi;
  31 T0_S44:
  32         if
  33         :: (! ((q)) && ! ((r))) -> goto accept_S8
  34         :: (! ((q))) -> goto T0_S44
  35         fi;
  36 T0_S58:
  37         if
  38         :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
  39         :: (! ((q)) && ! ((r))) -> goto T0_S17
  40         :: (! ((q)) && (p)) -> goto T0_S44
  41         :: (! ((q))) -> goto T0_S58
  42         fi;
  43 T0_S91:
  44         if
  45         :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
  46         :: (! ((q)) && ! ((r))) -> goto T0_S17
  47         :: (! ((r))) -> goto T0_S91
  48         fi;
  49 }
  50
  51 #ifdef NOTES
  52 Use Load to open a file or a template.
  53
  54
  55 #endif
  56 #ifdef RESULT
  57 warning: for p.o. reduction to be valid the never claim must be stutter-closed
  58 (never claims generated from LTL formulae are stutter-closed)
  59 (Spin Version 3.4.0 -- 7 August 2000)
  60         + Partial Order Reduction
  61
  62 Full statespace search for:
  63         never-claim             +
  64         assertion violations    + (if within scope of claim)
  65         acceptance   cycles     + (fairness disabled)
  66         invalid endstates       - (disabled by never-claim)
  67
  68 State-vector 128 byte, depth reached 1833, errors: 0
  69    44455 states, stored (48719 visited)
  70   137737 states, matched
  71   186456 transitions (= visited+matched)
  72      241 atomic steps
  73 hash conflicts: 8962 (resolved)
  74 (max size 2^19 states)
  75
  76 Stats on memory usage (in Megabytes):
  77 6.046   equivalent memory usage for states (stored*(State-vector + overhead))
  78 3.379   actual memory usage for states (compression: 55.89%)
  79         State-vector as stored = 68 byte + 8 byte overhead
  80 2.097   memory used for hash-table (-w19)
  81 0.240   memory used for DFS stack (-m10000)
  82 5.819   total actual memory usage
  83
  84 unreached in proctype CC
  85         line 49, state 25, "-end-"
  86         (1 of 25 states)
  87 unreached in proctype HC
  88         line 56, state 6, "-end-"
  89         (1 of 6 states)
  90 unreached in proctype MSC
  91         (0 of 4 states)
  92 unreached in proctype BS
  93         line 95, state 31, "-end-"
  94         (1 of 31 states)
  95 unreached in proctype MS
  96         line 108, state 14, "-end-"
  97         (1 of 14 states)
  98 unreached in proctype P
  99         (0 of 4 states)
 100 unreached in proctype Q
 101         (0 of 4 states)
 102 unreached in proctype System
 103         (0 of 4 states)
 104 unreached in proctype top
 105         line 143, state 7, "-end-"
 106         (1 of 7 states)
 107 unreached in proctype bot
 108         line 149, state 7, "-end-"
 109         (1 of 7 states)
 110 5.1u 0.1s 5r     ./pan -X -m10000 -w19 -a ...
 111
 112 #endif