[lttv.git] / trunk / verif / Spin / Test / leader.ltl

#define elected		(nr_leaders >  0)
#define noLeader	(nr_leaders == 0)
#define oneLeader	(nr_leaders == 1)

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

never {    /* !(<>[]oneLeader) */
T0_init:
	if
	:: (1) -> goto T0_init
	:: (! ((oneLeader))) -> goto accept_S5
	fi;
accept_S5:
	if
	:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}

#ifdef NOTES
Some other properties:
	![] noLeader
	<>  elected
	[] (noLeader U oneLeader)


#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.1.2 -- 14 March 1998)
	+ 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 200 byte, depth reached 233, errors: 0
     202 states, stored (402 visited)
     281 states, matched
     683 transitions (= visited+matched)
      36 atomic steps
hash conflicts: 0 (resolved)
(max size 2^19 states)

2.542 	memory usage (Mbyte)

unreached in proctype node
	line 105, state 28, "out!two,nr"
	(1 of 49 states)
unreached in proctype :init:
	(0 of 11 states)

real 0.13
user 0.04
sys  0.09

#endif
Commit	Line	Data
0b55f123	1	#define elected (nr_leaders > 0)
	2	#define noLeader (nr_leaders == 0)
	3	#define oneLeader (nr_leaders == 1)
	4
	5	/*
	6	* Formula As Typed: <>[]oneLeader
	7	* The Never Claim Below Corresponds
	8	* To The Negated Formula !(<>[]oneLeader)
	9	* (formalizing violations of the original)
	10	*/
	11
	12	never { /* !(<>[]oneLeader) */
	13	T0_init:
	14	if
	15	:: (1) -> goto T0_init
	16	:: (! ((oneLeader))) -> goto accept_S5
	17	fi;
	18	accept_S5:
	19	if
	20	:: (1) -> goto T0_init
	21	fi;
	22	accept_all:
	23	skip
	24	}
	25
	26	#ifdef NOTES
	27	Some other properties:
	28	![] noLeader
	29	<> elected
	30	[] (noLeader U oneLeader)
	31
	32
	33
	34
	35
	36
	37	#endif
	38	#ifdef RESULT
	39	warning: for p.o. reduction to be valid the never claim must be stutter-closed
	40	(never claims generated from LTL formulae are stutter-closed)
	41	(Spin Version 3.1.2 -- 14 March 1998)
	42	+ Partial Order Reduction
	43
	44	Full statespace search for:
	45	never-claim +
	46	assertion violations + (if within scope of claim)
	47	acceptance cycles + (fairness disabled)
	48	invalid endstates - (disabled by never-claim)
	49
	50	State-vector 200 byte, depth reached 233, errors: 0
	51	202 states, stored (402 visited)
	52	281 states, matched
	53	683 transitions (= visited+matched)
	54	36 atomic steps
	55	hash conflicts: 0 (resolved)
	56	(max size 2^19 states)
	57
	58	2.542 memory usage (Mbyte)
	59
	60	unreached in proctype node
	61	line 105, state 28, "out!two,nr"
	62	(1 of 49 states)
	63	unreached in proctype :init:
	64	(0 of 11 states)
65
66	real 0.13
67	user 0.04
68	sys 0.09
69
70	#endif