+++ /dev/null
-#define p in?[red]
-#define q out?[red]
-#define r (BS[a_id]@progress || BS[p_id]@progress)
-
- /*
- * Formula As Typed: (![]<>(r)) -> [](<>p -> <>q)
- * The Never Claim Below Corresponds
- * To The Negated Formula !((![]<>(r)) -> [](<>p -> <>q))
- * (formalizing violations of the original)
- */
-
-never { /* !((![]<>(r)) -> [](<>p -> <>q)) */
-T0_init:
- if
- :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
- :: (! ((q)) && ! ((r))) -> goto T0_S17
- :: (! ((q)) && (p)) -> goto T0_S44
- :: (! ((q))) -> goto T0_S58
- :: (! ((r))) -> goto T0_S91
- :: (1) -> goto T0_init
- fi;
-accept_S8:
- if
- :: (! ((q)) && ! ((r))) -> goto accept_S8
- fi;
-T0_S17:
- if
- :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
- :: (! ((q)) && ! ((r))) -> goto T0_S17
- fi;
-T0_S44:
- if
- :: (! ((q)) && ! ((r))) -> goto accept_S8
- :: (! ((q))) -> goto T0_S44
- fi;
-T0_S58:
- if
- :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
- :: (! ((q)) && ! ((r))) -> goto T0_S17
- :: (! ((q)) && (p)) -> goto T0_S44
- :: (! ((q))) -> goto T0_S58
- fi;
-T0_S91:
- if
- :: (! ((q)) && ! ((r)) && (p)) -> goto accept_S8
- :: (! ((q)) && ! ((r))) -> goto T0_S17
- :: (! ((r))) -> goto T0_S91
- fi;
-}
-
-#ifdef NOTES
-Use Load to open a file or a template.
-
-
-#endif
-#ifdef RESULT
-warning: for p.o. reduction to be valid the never claim must be stutter-closed
-(never claims generated from LTL formulae are stutter-closed)
-(Spin Version 3.4.0 -- 7 August 2000)
- + Partial Order Reduction
-
-Full statespace search for:
- never-claim +
- assertion violations + (if within scope of claim)
- acceptance cycles + (fairness disabled)
- invalid endstates - (disabled by never-claim)
-
-State-vector 128 byte, depth reached 1833, errors: 0
- 44455 states, stored (48719 visited)
- 137737 states, matched
- 186456 transitions (= visited+matched)
- 241 atomic steps
-hash conflicts: 8962 (resolved)
-(max size 2^19 states)
-
-Stats on memory usage (in Megabytes):
-6.046 equivalent memory usage for states (stored*(State-vector + overhead))
-3.379 actual memory usage for states (compression: 55.89%)
- State-vector as stored = 68 byte + 8 byte overhead
-2.097 memory used for hash-table (-w19)
-0.240 memory used for DFS stack (-m10000)
-5.819 total actual memory usage
-
-unreached in proctype CC
- line 49, state 25, "-end-"
- (1 of 25 states)
-unreached in proctype HC
- line 56, state 6, "-end-"
- (1 of 6 states)
-unreached in proctype MSC
- (0 of 4 states)
-unreached in proctype BS
- line 95, state 31, "-end-"
- (1 of 31 states)
-unreached in proctype MS
- line 108, state 14, "-end-"
- (1 of 14 states)
-unreached in proctype P
- (0 of 4 states)
-unreached in proctype Q
- (0 of 4 states)
-unreached in proctype System
- (0 of 4 states)
-unreached in proctype top
- line 143, state 7, "-end-"
- (1 of 7 states)
-unreached in proctype bot
- line 149, state 7, "-end-"
- (1 of 7 states)
-5.1u 0.1s 5r ./pan -X -m10000 -w19 -a ...
-
-#endif