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