#define success		(statusA == ok && statusB == ok)
#define aliceBob	partnerA == bob
#define bobAlice	partnerB == alice
#define knowNA		knowNA
#define knowNB		knowNB

	/*
	 * Formula As Typed: []  (success -> (aliceBob -> bobAlice))
	 */

never {    /* ([]  (success -> (aliceBob -> bobAlice))) */
accept_init:
T0_init:
	if
	:: (((! ((aliceBob))) || (((! ((success))) || ((bobAlice)))))) -> goto T0_init
	fi;
}

#ifdef NOTES
[]  (success -> (aliceBob -> bobAlice))   authentification of Bob to Alice
[]  (success -> (bobAlice -> aliceBob))   authentification of Alice to Bob
[]  (success -> (aliceBob -> !knowNA))    non-disclosure of keyA
[]  (success -> (bobAlice -> !knowNB))    non-disclosure of keyB


#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)
pan: acceptance cycle (at depth 16)
pan: wrote pan_in.trail
(Spin Version 3.3.10 -- 15 March 2000)
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 endstates	- (disabled by never-claim)

State-vector 52 byte, depth reached 17, errors: 1
       8 states, stored (9 visited)
       1 states, matched
      10 transitions (= visited+matched)
       0 atomic steps
hash conflicts: 0 (resolved)
(max size 2^19 states)

2.542 	memory usage (Mbyte)

0.01user 0.01system 0:00.08elapsed 24%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+0outputs (123major+589minor)pagefaults 0swaps

#endif