Context Navigation

minMax.ltl @ 11

Last change on this file since 11 was 11, checked in by cecile, 14 years ago
Add vis
File size: 718 bytes

Rev	Line
[11]	1	#FAIL: a specified reset state must eventually be reached from every state.
	2	# This formula fails in spite of the fairness conditions.
	3	G(F(min[8:0]=b111111111 * last[8:0]=0 * max[8:0]=0));
	4
	5	#PASS: The non-reset states reachable in one clock cycle from the reset
	6	# states have min == last == max.
	7	G(min[8:0]=b111111111 * max[8:0]=b000000000 ->
	8	X(min[8:0]=b111111111 * max[8:0]=b000000000 +
	9	min[8:0] == last[8:0] * last[8:0] == max[8:0]));
	10
	11	#PASS: The non-reset states reachable in two clock cycles from the reset
	12	# states have either min == last or last == max.
	13	G(min[8:0]=b111111111 * max[8:0]=b000000000 ->
	14	X:2(min[8:0]=b111111111 * max[8:0]=b000000000 +
	15	min[8:0] == last[8:0] + last[8:0] == max[8:0]));

Note: See TracBrowser for help on using the repository browser.