1/*
2 * input: days elapsed since Jan 1, 1980
3 * intended output: year and daynr in current year
4 *
5 * a bug caused all Zune-30 players to freeze on Dec 31, 2008
6 * http://www.zuneboards.com/forums/zune-news/38143-cause-zune-30-leapyear-problem-isolated.html
7 *
8 * Wikepedia:
9 * The bug was in the firmware clock-driver, which was written by Freescale
10 * for their MC13783 PMIC processor. The same bug froze up Toshiba Gigabeat S
11 * media players that share the same hardware and driver.
12 */
13
14#define IsLeapYear(y)	(((y%4 == 0) && (y%100 != 0)) || (y%400 == 0))
15
16chan q = [0] of { short };
17
18active proctype zune()
19{	short year = 1980;
20	short days;
21
22end:	do
23	:: q?days ->
24S:		do
25		:: days > 365 ->
26			if
27			:: IsLeapYear(year) ->
28				if
29				:: days > 366 ->
30					days = days - 366;
31					year++
32				:: else
33#ifdef FIX
34					-> break
35#endif
36				fi
37			:: else ->
38				days = days - 365;
39				year++
40			fi
41		:: else ->
42			break
43		od;
44E:		printf("Year: %d, Day %d\n", year, days)
45	od;
46	/* check that the date is in a valid range */
47	assert(days >= 1 && days <= 366);
48	assert(days < 366 || IsLeapYear(year))
49}
50
51init {
52	/* jan 1, 2008 */
53	short days = (2008 - 1980) * 365 + (2008-1980)/4;
54
55	if
56	:: q!days + 365
57	:: q!days + 366
58	:: q!days + 367
59	fi
60}
61
62ltl p1 { [] (( zune@S ) -> ( <> zune@E ) ) }
63
64/* sample analysis:
65	spin -a zune.pml	# spin version 6 or later
66	cc -o pan pan.c		# compile
67	./pan -a -N p1		# find matches of formula
68	spin -t -p -l zune.pml	# replay error sequence
69 */
70
71