#define running  (blocked == false)
#define p1       (roadB[0] == true)
#define p2       (roadB[1] == true)
#define p3       (roadB[2] == true)
#define p4       (roadB[3] == true)

	/*
	 * Formula As Typed: []running
	 * The Never Claim Below Corresponds
	 * To The Negated Formula !([]running)
	 * (formalizing violations of the original)
	 */

never {    /* !([]running) */
T0_init:
	if
	:: (! ((running))) -> 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 63)
pan: wrote pan_in.trail
(Spin Version 4.2.2 -- 12 December 2004)
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 24 byte, depth reached 63, errors: 1
      34 states, stored
       1 states, matched
      35 transitions (= stored+matched)
       0 atomic steps
hash conflicts: 0 (resolved)

Stats on memory usage (in Megabytes):
0.001 	equivalent memory usage for states (stored*(State-vector + overhead))
0.301 	actual memory usage for states (unsuccessful compression: 27629.04%)
	State-vector as stored = 8833 byte + 8 byte overhead
2.097 	memory used for hash table (-w19)
0.320 	memory used for DFS stack (-m10000)
0.128 	other (proc and chan stacks)
0.096 	memory lost to fragmentation
2.622 	total actual memory usage

unreached in proctype traffic
	line 27, "pan.___", state 10, "roadA[3] = 1"
	line 32, "pan.___", state 19, "roadA[0] = 1"
	line 33, "pan.___", state 21, "roadA[1] = 0"
	line 33, "pan.___", state 22, "roadA[2] = 1"
	line 34, "pan.___", state 24, "roadA[1] = 0"
	line 37, "pan.___", state 27, "roadB[1] = 0"
	line 38, "pan.___", state 30, "roadB[1] = 0"
	line 38, "pan.___", state 31, "roadB[2] = 1"
	line 39, "pan.___", state 33, "roadB[1] = 0"
	line 39, "pan.___", state 34, "roadA[2] = 1"
	line 42, "pan.___", state 36, "roadB[3] = 0"
	line 42, "pan.___", state 37, "roadB[0] = 1"
	line 43, "pan.___", state 39, "roadB[3] = 0"
	line 43, "pan.___", state 40, "roadB[2] = 1"
	line 44, "pan.___", state 42, "roadB[3] = 0"
	line 44, "pan.___", state 43, "roadA[0] = 1"
	line 47, "pan.___", state 46, "roadA[0] = 1"
	line 48, "pan.___", state 48, "roadA[3] = 0"
	line 48, "pan.___", state 49, "roadA[2] = 1"
	line 49, "pan.___", state 51, "roadA[3] = 0"
	line 49, "pan.___", state 52, "roadB[0] = 1"
	(21 of 59 states)
unreached in proctype :never:
	line 78, "pan.___", state 8, "-end-"
	(1 of 8 states)
0.00user 0.03system 0:00.03elapsed 96%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+0outputs (0major+734minor)pagefaults 0swaps

#endif