/* */
#define p (M_knows_NB == true)
#define q (M_knows_NA == true)
#define r (B_partner == A)

	/*
	 * Formula As Typed: ! <> (p && q && r)
	 * The Never Claim Below Corresponds
	 * To The Negated Formula !(! <> (p && q && r))
	 * (formalizing violations of the original)
	 */

never {    /* !(! <> (p && q && r)) */
T0_init:
	if
	:: ((p) && (q) && (r)) -> goto accept_all
	:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}

#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-invariant
(never claims generated from LTL formulae are stutter-invariant)
pan: claim violated! (at depth 69)
pan: wrote pan_in.trail
(Spin Version 4.2.5 -- 2 April 2005)
Warning: Search not completed
	+ Partial Order Reduction

Full statespace search for:
	never claim         	+
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	- (disabled by never claim)

State-vector 56 byte, depth reached 101, errors: 1
   57265 states, stored
   32328 states, matched
   89593 transitions (= stored+matched)
    1827 atomic steps
hash conflicts: 1000 (resolved)

Stats on memory usage (in Megabytes):
3.665 	equivalent memory usage for states (stored*(State-vector + overhead))
2.957 	actual memory usage for states (compression: 80.68%)
	State-vector as stored = 44 byte + 8 byte overhead
2.097 	memory used for hash table (-w19)
0.320 	memory used for DFS stack (-m10000)
0.141 	other (proc and chan stacks)
0.090 	memory lost to fragmentation
5.284 	total actual memory usage

unreached in proctype A_proc
	(0 of 20 states)
unreached in proctype B_proc
	(0 of 18 states)
unreached in proctype M_proc
	line 146, "pan.___", state 76, "-end-"
	(1 of 76 states)
unreached in proctype :init:
	(0 of 4 states)
unreached in proctype :never:
	line 173, "pan.___", state 8, "-end-"
	(1 of 8 states)

#endif