[lttv.git] / trunk / verif / md / pan.otl

#define p	(write_off - read_off >= 0)
#define q	(write_off - read_off < HALF_UCHAR)

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

never {    /* !([] (p && q)) */
T0_init:
	if
	:: (((! ((p))) || (! ((q))))) -> 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)
depth 0: Claim reached state 5 (line 321)
Running verification -- waiting for output
	(kill background process 'pan' to abort run)
	(use /bin/ps to find pid; then: kill -2 pid)

#endif
Commit	Line	Data
dc45444e	1	#define p (write_off - read_off >= 0)
	2	#define q (write_off - read_off < HALF_UCHAR)
	3
	4	/*
	5	* Formula As Typed: [] (p && q)
	6	* The Never Claim Below Corresponds
	7	* To The Negated Formula !([] (p && q))
	8	* (formalizing violations of the original)
	9	*/
	10
	11	never { /* !([] (p && q)) */
	12	T0_init:
	13	if
	14	:: (((! ((p))) \|\| (! ((q))))) -> goto accept_all
	15	:: (1) -> goto T0_init
	16	fi;
	17	accept_all:
	18	skip
	19	}
	20
	21	#ifdef NOTES
	22	Use Load to open a file or a template.
	23	#endif
	24	#ifdef RESULT
	25	warning: for p.o. reduction to be valid the never claim must be stutter-invariant
	26	(never claims generated from LTL formulae are stutter-invariant)
	27	depth 0: Claim reached state 5 (line 321)
	28	Running verification -- waiting for output
	29	(kill background process 'pan' to abort run)
	30	(use /bin/ps to find pid; then: kill -2 pid)
	31
	32	#endif