/*************************************************** * File automatically generated for file 'hppr10_audio.imi' * The following pi0 was considered: ptpOff = 0 & ptpPeriod = 40 & audOff = 0 & audPeriod = 10 & D1 = 10 & driftDelta = 0 & D2 = 10 & C1 = 10 & C2 = 5 * 60 states and 103 transitions * Program terminated after 2.112 seconds ***************************************************/ /* DESCRIPTION OF THE STATES STATE 0: act_Ptp: WFO, act_Audio: WFO, Audio_Checker: idle ==> ptpPeriod >= 3*audPeriod & audPeriod + driftDelta >= D2 & C2 > 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & 2*audPeriod >= C1 + 2*C2 & 5*audPeriod >= ptpPeriod + C2 & ptpOff >= cPtp & audOff >= cAudio STATE 101: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> 5*audPeriod >= ptpPeriod + C2 & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C1 + cAudio > cPtp & C2 > 0 & cPtp >= cAudio & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & ptpPeriod >= 3*audPeriod & C1 + C2 = rAudioChecker & cPtp = cAudioChecker STATE 1: act_Ptp: WFP, act_Audio: WFO, Audio_Checker: busy ==> C1 + C2 > audPeriod & 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= cPtp & ptpPeriod >= 3*audPeriod & audOff >= cAudio & audPeriod + driftDelta >= D2 & 2*audPeriod >= C1 + 2*C2 & C2 > 0 & cPtp >= 0 & D2 >= driftDelta + C2 & C1 = rAudioChecker & cPtp = cAudioChecker STATE 103: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> ptpPeriod >= cPtp & 4*audPeriod + cAudio > cPtp & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & C2 + cPtp > 4*audPeriod + cAudio & 5*audPeriod >= ptpPeriod + C2 & 3*audPeriod + cAudio = cAudioChecker STATE 106: act_Ptp: WFO, act_Audio: WFP, Audio_Checker: check ==> audPeriod >= cAudio & ptpOff >= cPtp & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & C2 > 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & cAudio >= 0 & 5*audPeriod >= ptpPeriod + C2 & 6*audPeriod + cAudio = cAudioChecker STATE 6: act_Ptp: WFP, act_Audio: WFO, Audio_Checker: idle ==> 2*audPeriod >= C1 + 2*C2 & C2 > 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & audPeriod + driftDelta >= D2 & 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= cPtp & audOff >= cAudio & ptpPeriod >= 3*audPeriod & cPtp >= C1 & cPtp = cAudioChecker STATE 107: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> ptpPeriod >= cPtp & 5*audPeriod >= ptpPeriod + C2 & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod + C1 + cAudio > cPtp & audPeriod >= cAudio & C2 > 0 & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & cPtp >= audPeriod + cAudio & ptpPeriod >= 3*audPeriod & cPtp = cAudioChecker STATE 8: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 + cPtp > cAudio & cPtp >= 0 & cAudio > cPtp & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & 5*audPeriod >= ptpPeriod + C2 & cAudio = cAudioChecker STATE 9: act_Ptp: WFO, act_Audio: WFP, Audio_Checker: check ==> 5*audPeriod >= ptpPeriod + C2 & ptpOff >= cPtp & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 > 0 & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & audPeriod + cAudio = cAudioChecker STATE 10: act_Ptp: WFO, act_Audio: WFP, Audio_Checker: idle ==> ptpOff >= cPtp & 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 > 0 & cAudio >= C2 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & cAudio = cAudioChecker STATE 111: act_Ptp: WFO, act_Audio: WFP, Audio_Checker: check ==> audPeriod >= cAudio & ptpOff >= cPtp & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & C2 > 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & cAudio >= 0 & 5*audPeriod >= ptpPeriod + C2 & 7*audPeriod + cAudio = cAudioChecker STATE 11: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 + cPtp > cAudio & cPtp >= 0 & cAudio >= cPtp & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & 5*audPeriod >= ptpPeriod + C2 & C1 + C2 = rAudioChecker & cAudio = cAudioChecker STATE 112: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod >= cAudio & audPeriod + cAudio >= cPtp & cAudio >= 0 & C1 + C2 > audPeriod & C2 + cPtp > audPeriod + cAudio & 5*audPeriod >= ptpPeriod + C2 & audPeriod + driftDelta = D2 & audPeriod + cAudio = cAudioChecker STATE 12: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 > 0 & cPtp >= 0 & cAudio >= C2 + cPtp & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & C1 = rAudioChecker & cPtp = cAudioChecker STATE 113: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: error ==> ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod >= cAudio & audPeriod + cAudio >= cPtp & cAudio >= 0 & C1 + C2 > audPeriod & C2 + cPtp > audPeriod + cAudio & 5*audPeriod >= ptpPeriod + C2 & audPeriod + driftDelta = D2 & audPeriod + cAudio = cAudioChecker STATE 114: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> 5*audPeriod >= ptpPeriod + C2 & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod + C1 + C2 >= rAudioChecker + cPtp & C1 + C2 >= rAudioChecker & C2 > 0 & rAudioChecker > C2 & rAudioChecker + cPtp >= C1 + C2 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & ptpPeriod >= 3*audPeriod & C1 + C2 + cAudio = rAudioChecker + cPtp & cPtp = cAudioChecker STATE 115: act_Ptp: WFO, act_Audio: WFP, Audio_Checker: check ==> audPeriod >= cAudio & ptpOff >= cPtp & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & C2 > 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & cAudio >= 0 & 5*audPeriod >= ptpPeriod + C2 & 8*audPeriod + cAudio = cAudioChecker STATE 15: act_Ptp: WFO, act_Audio: WFP, Audio_Checker: check ==> 5*audPeriod >= ptpPeriod + C2 & ptpOff >= cPtp & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 > 0 & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & 2*audPeriod + cAudio = cAudioChecker STATE 116: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> ptpPeriod >= cPtp & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 > 0 & cAudio >= 0 & cPtp >= C1 + cAudio & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & 5*audPeriod >= ptpPeriod + C2 & C2 = rAudioChecker & cAudio = cAudioChecker STATE 16: act_Ptp: WFO, act_Audio: WFP, Audio_Checker: idle ==> 5*audPeriod >= ptpPeriod + C2 & ptpOff >= cPtp & 2*audPeriod >= C1 + 2*C2 & audPeriod >= cAudio & ptpPeriod >= 3*audPeriod & C2 > 0 & cAudio >= 0 & C1 + C2 > audPeriod & audPeriod + driftDelta = D2 & audPeriod + cAudio = cAudioChecker STATE 117: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> ptpPeriod >= cPtp & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 > 0 & cAudio >= 0 & cPtp >= C1 + cAudio & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & 5*audPeriod >= ptpPeriod + C2 & C2 = rAudioChecker & cAudio = cAudioChecker STATE 17: act_Ptp: WFO, act_Audio: WFP, Audio_Checker: error ==> C1 + C2 > audPeriod & 5*audPeriod >= ptpPeriod + C2 & ptpOff >= cPtp & 2*audPeriod >= C1 + 2*C2 & audPeriod >= cAudio & ptpPeriod >= 3*audPeriod & C2 > 0 & cAudio >= 0 & audPeriod + driftDelta = D2 & audPeriod + cAudio = cAudioChecker STATE 118: act_Ptp: WFO, act_Audio: WFP, Audio_Checker: check ==> audPeriod >= cAudio & ptpOff >= cPtp & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & C2 > 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & cAudio >= 0 & 5*audPeriod >= ptpPeriod + C2 & 9*audPeriod + cAudio = cAudioChecker STATE 18: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & audPeriod + cAudio > cPtp & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & C2 + cPtp > audPeriod + cAudio & audPeriod + cAudio = cAudioChecker STATE 19: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 + cPtp > cAudio & cPtp >= 0 & cAudio > cPtp & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & cAudio = cAudioChecker STATE 20: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: error ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod >= cAudio & driftDelta + cAudio >= D2 & C2 + cPtp > cAudio & cAudio >= cPtp & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & cAudio = cAudioChecker STATE 23: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C1 + C2 + cAudio > cPtp & C2 > 0 & cAudio >= 0 & D2 >= driftDelta + C2 & cPtp >= audPeriod + cAudio & C1 + 2*C2 = rAudioChecker & cPtp = cAudioChecker STATE 25: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C1 + cAudio > cPtp & C2 > 0 & cPtp >= C1 + C2 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & cPtp = cAudioChecker STATE 27: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C1 + C2 + 2*cAudio >= 2*cPtp & C1 + cAudio > cPtp & C2 > 0 & 2*cPtp >= C1 + C2 + cAudio & D2 + cPtp >= driftDelta + C1 + C2 + cAudio & C1 + C2 > audPeriod & 5*audPeriod >= ptpPeriod + C2 & cPtp = cAudioChecker STATE 28: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: error ==> ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & driftDelta + C1 + C2 + cAudio > D2 + cPtp & driftDelta + cPtp >= D2 & C2 > 0 & cPtp >= cAudio & D2 + cAudio >= driftDelta + cPtp & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & 5*audPeriod >= ptpPeriod + C2 & cPtp = cAudioChecker STATE 31: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & audPeriod + cAudio >= cPtp & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & C2 + cPtp > audPeriod + cAudio & C1 + 2*C2 = rAudioChecker & audPeriod + cAudio = cAudioChecker STATE 32: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & audPeriod + cAudio >= cPtp & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & C2 + cPtp > audPeriod + cAudio & audPeriod + rAudioChecker = C1 + 2*C2 & audPeriod + cAudio = cAudioChecker STATE 33: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> ptpPeriod >= cPtp & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 > 0 & cAudio >= C2 & cPtp >= C1 + cAudio & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & 5*audPeriod >= ptpPeriod + C2 & cAudio = cAudioChecker STATE 34: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> ptpPeriod >= cPtp & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 > 0 & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & cPtp >= audPeriod + C1 + cAudio & 5*audPeriod >= ptpPeriod + C2 & audPeriod + cAudio = cAudioChecker STATE 37: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> ptpPeriod >= cPtp & ptpPeriod >= 3*audPeriod & 2*audPeriod + C1 + cAudio > cPtp & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 > 0 & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & cPtp >= 2*audPeriod + cAudio & 5*audPeriod >= ptpPeriod + C2 & cPtp = cAudioChecker STATE 40: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C1 + C2 + cAudio > cPtp & C2 > 0 & cPtp >= C1 + 2*C2 & D2 >= driftDelta + C2 & cPtp >= audPeriod + cAudio & cPtp = cAudioChecker STATE 41: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & audPeriod + cAudio > cPtp & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & C2 + cPtp > audPeriod + cAudio & C2 = rAudioChecker & cAudio = cAudioChecker STATE 42: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & audPeriod + cAudio > cPtp & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & C2 + cPtp > audPeriod + cAudio & C2 = rAudioChecker & cAudio = cAudioChecker STATE 43: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod + cAudio >= cPtp & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & C2 + cPtp > 2*audPeriod + cAudio & 2*audPeriod + cAudio = cAudioChecker STATE 48: act_Ptp: WFO, act_Audio: WFP, Audio_Checker: check ==> 5*audPeriod >= ptpPeriod + C2 & ptpOff >= cPtp & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 > 0 & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & 3*audPeriod + cAudio = cAudioChecker STATE 50: act_Ptp: WFO, act_Audio: WFP, Audio_Checker: check ==> 5*audPeriod >= ptpPeriod + C2 & ptpOff >= cPtp & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 > 0 & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & C2 = rAudioChecker & cAudio = cAudioChecker STATE 51: act_Ptp: WFO, act_Audio: WFP, Audio_Checker: busy ==> ptpOff >= cPtp & 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 > 0 & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & C2 = rAudioChecker & cAudio = cAudioChecker STATE 54: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & audPeriod + cAudio >= cPtp & audPeriod + cAudio >= C1 + 2*C2 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & C2 + cPtp > audPeriod + cAudio & audPeriod + cAudio = cAudioChecker STATE 62: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> 5*audPeriod >= ptpPeriod + C2 & 2*audPeriod >= C1 + 2*C2 & audPeriod >= cAudio & cAudio >= cPtp & cPtp >= C1 & C1 + C2 > audPeriod & ptpPeriod >= 3*audPeriod & audPeriod + driftDelta = D2 & cPtp = cAudioChecker STATE 64: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & audPeriod + cAudio > cPtp & cAudio >= C2 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & C2 + cPtp > audPeriod + cAudio & cAudio = cAudioChecker STATE 65: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod + cAudio > cPtp & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & C2 + cPtp > 2*audPeriod + cAudio & audPeriod + cAudio = cAudioChecker STATE 70: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> ptpPeriod >= 3*audPeriod & 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= cPtp & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 > 0 & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & cPtp >= 2*audPeriod + C1 + cAudio & 2*audPeriod + cAudio = cAudioChecker STATE 71: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= cPtp & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod >= cAudio & C2 > 0 & cAudio >= 0 & C1 + C2 > audPeriod & cPtp >= audPeriod + C1 + cAudio & audPeriod + driftDelta = D2 & audPeriod + cAudio = cAudioChecker STATE 72: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: error ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= cPtp & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod >= cAudio & C2 > 0 & cAudio >= 0 & C1 + C2 > audPeriod & cPtp >= audPeriod + C1 + cAudio & audPeriod + driftDelta = D2 & audPeriod + cAudio = cAudioChecker STATE 73: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= cPtp & 3*audPeriod + C1 + cAudio > cPtp & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 > 0 & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & cPtp >= 3*audPeriod + cAudio & cPtp = cAudioChecker STATE 76: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> ptpPeriod >= 3*audPeriod & 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= cPtp & 3*audPeriod + cAudio >= cPtp & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & C2 + cPtp > 3*audPeriod + cAudio & 3*audPeriod + cAudio = cAudioChecker STATE 77: act_Ptp: WFO, act_Audio: WFP, Audio_Checker: check ==> 5*audPeriod >= ptpPeriod + C2 & ptpOff >= cPtp & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 > 0 & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & 4*audPeriod + cAudio = cAudioChecker STATE 78: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> ptpPeriod >= cPtp & 4*audPeriod + cAudio >= cPtp & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & 5*audPeriod >= ptpPeriod + C2 & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & C2 + cPtp > 4*audPeriod + cAudio & 4*audPeriod + cAudio = cAudioChecker STATE 80: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod >= cAudio & C2 > 0 & cPtp >= 0 & cAudio >= cPtp & C1 + C2 > audPeriod & audPeriod + driftDelta = D2 & C1 = rAudioChecker & cPtp = cAudioChecker STATE 83: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> ptpPeriod >= cPtp & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & 5*audPeriod >= ptpPeriod + C2 & C2 > 0 & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & cPtp >= 3*audPeriod + C1 + cAudio & 3*audPeriod + cAudio = cAudioChecker STATE 91: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> ptpPeriod >= 3*audPeriod & 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= cPtp & 3*audPeriod + cAudio > cPtp & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & C2 + cPtp > 3*audPeriod + cAudio & 2*audPeriod + cAudio = cAudioChecker STATE 92: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod + cAudio > cPtp & 2*audPeriod >= C1 + 2*C2 & audPeriod >= cAudio & cAudio >= 0 & C1 + C2 > audPeriod & C2 + cPtp > 2*audPeriod + cAudio & audPeriod + driftDelta = D2 & audPeriod + cAudio = cAudioChecker STATE 93: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: error ==> 5*audPeriod >= ptpPeriod + C2 & ptpPeriod >= 3*audPeriod & 2*audPeriod + cAudio > cPtp & 2*audPeriod >= C1 + 2*C2 & audPeriod >= cAudio & cAudio >= 0 & C1 + C2 > audPeriod & C2 + cPtp > 2*audPeriod + cAudio & audPeriod + driftDelta = D2 & audPeriod + cAudio = cAudioChecker STATE 94: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> ptpPeriod >= cPtp & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & 5*audPeriod >= ptpPeriod + C2 & C2 > 0 & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & cPtp >= 4*audPeriod + cAudio & cPtp = cAudioChecker STATE 95: act_Ptp: WFO, act_Audio: WFP, Audio_Checker: check ==> 5*audPeriod >= ptpPeriod + C2 & ptpOff >= cPtp & ptpPeriod >= 3*audPeriod & 2*audPeriod >= C1 + 2*C2 & audPeriod + driftDelta >= D2 & audPeriod >= cAudio & C2 > 0 & cAudio >= 0 & D2 >= driftDelta + C2 & C1 + C2 > audPeriod & 5*audPeriod + cAudio = cAudioChecker */ digraph G { s0 -> s51 [label="Release_Audio"]; s0 -> s50 [label="Release_Audio"]; s0 -> s1 [label="Release_PTP"]; s1 -> s6 [label="Ending_Audio"]; s1 -> s114 [label="Release_Audio"]; s1 -> s101 [label="Release_Audio"]; s6 -> s117 [label="Release_Audio"]; s6 -> s116 [label="Release_Audio"]; s6 -> s1 [label="Release_PTP"]; s8 -> s20; s8 -> s19 [label="Ending_Audio"]; s8 -> s18 [label="Release_Audio"]; s9 -> s17; s9 -> s16 [label="Ending_Audio"]; s9 -> s15 [label="Release_Audio"]; s10 -> s51 [label="Release_Audio"]; s10 -> s50 [label="Release_Audio"]; s10 -> s12 [label="Release_PTP"]; s11 -> s32 [label="Release_Audio"]; s11 -> s31 [label="Release_Audio"]; s12 -> s114 [label="Release_Audio"]; s12 -> s101 [label="Release_Audio"]; s15 -> s48 [label="Release_Audio"]; s16 -> s51 [label="Release_Audio"]; s16 -> s50 [label="Release_Audio"]; s16 -> s80 [label="Release_PTP"]; s18 -> s113; s18 -> s112 [label="Ending_Audio"]; s18 -> s43 [label="Release_Audio"]; s19 -> s42 [label="Release_Audio"]; s19 -> s41 [label="Release_Audio"]; s23 -> s40 [label="Ending_Audio"]; s25 -> s117 [label="Release_Audio"]; s25 -> s116 [label="Release_Audio"]; s27 -> s117 [label="Release_Audio"]; s27 -> s116 [label="Release_Audio"]; s31 -> s54 [label="Ending_Audio"]; s32 -> s112 [label="Ending_Audio"]; s32 -> s43 [label="Release_Audio"]; s33 -> s12 [label="Release_PTP"]; s33 -> s116 [label="Release_Audio"]; s33 -> s117 [label="Release_Audio"]; s34 -> s70 [label="Release_Audio"]; s34 -> s71 [label="Ending_Audio"]; s34 -> s72; s37 -> s73 [label="Release_Audio"]; s40 -> s116 [label="Release_Audio"]; s40 -> s117 [label="Release_Audio"]; s41 -> s65 [label="Release_Audio"]; s41 -> s64 [label="Ending_Audio"]; s42 -> s64 [label="Ending_Audio"]; s43 -> s76 [label="Release_Audio"]; s48 -> s77 [label="Release_Audio"]; s50 -> s10 [label="Ending_Audio"]; s50 -> s9 [label="Release_Audio"]; s50 -> s8 [label="Release_PTP"]; s50 -> s114 [label="Release_PTP"]; s51 -> s10 [label="Ending_Audio"]; s51 -> s11 [label="Release_PTP"]; s54 -> s116 [label="Release_Audio"]; s54 -> s117 [label="Release_Audio"]; s62 -> s117 [label="Release_Audio"]; s62 -> s116 [label="Release_Audio"]; s64 -> s117 [label="Release_Audio"]; s64 -> s116 [label="Release_Audio"]; s65 -> s93; s65 -> s92 [label="Ending_Audio"]; s65 -> s91 [label="Release_Audio"]; s70 -> s83 [label="Release_Audio"]; s71 -> s117 [label="Release_Audio"]; s71 -> s116 [label="Release_Audio"]; s71 -> s80 [label="Release_PTP"]; s73 -> s94 [label="Release_Audio"]; s76 -> s78 [label="Release_Audio"]; s77 -> s95 [label="Release_Audio"]; s80 -> s101 [label="Release_Audio"]; s80 -> s62 [label="Ending_Audio"]; s80 -> s114 [label="Release_Audio"]; s91 -> s103 [label="Release_Audio"]; s92 -> s116 [label="Release_Audio"]; s92 -> s117 [label="Release_Audio"]; s95 -> s106 [label="Release_Audio"]; s101 -> s107 [label="Release_Audio"]; s101 -> s25 [label="Ending_Audio"]; s101 -> s23 [label="Release_Audio"]; s106 -> s111 [label="Release_Audio"]; s107 -> s37 [label="Release_Audio"]; s107 -> s112 [label="Ending_Audio"]; s107 -> s113; s111 -> s115 [label="Release_Audio"]; s112 -> s116 [label="Release_Audio"]; s112 -> s117 [label="Release_Audio"]; s114 -> s28; s114 -> s27 [label="Ending_Audio"]; s114 -> s107 [label="Release_Audio"]; s114 -> s20; s115 -> s118 [label="Release_Audio"]; s116 -> s33 [label="Ending_Audio"]; s116 -> s34 [label="Release_Audio"]; s116 -> s8 [label="Release_PTP"]; s116 -> s114 [label="Release_PTP"]; s117 -> s33 [label="Ending_Audio"]; s117 -> s11 [label="Release_PTP"]; s0[color=red, style=filled]; s101[color=green, style=filled]; s1[color=blue, style=filled]; s103[color=yellow, style=filled]; s106[color=cyan, style=filled]; s6[color=magenta, style=filled]; s107[color=yellow, style=filled]; s8[color=yellow, style=filled]; s9[color=cyan, style=filled]; s10[color=paleturquoise2, style=filled]; s111[color=cyan, style=filled]; s11[color=green, style=filled]; s112[color=indianred1, style=filled]; s12[color=green, style=filled]; s113[color=goldenrod3, style=filled]; s114[color=yellow, style=filled]; s115[color=cyan, style=filled]; s15[color=cyan, style=filled]; s116[color=yellow, style=filled]; s16[color=paleturquoise2, style=filled]; s117[color=green, style=filled]; s17[color=darkolivegreen4, style=filled]; s118[color=cyan, style=filled]; s18[color=yellow, style=filled]; s19[color=indianred1, style=filled]; s20[color=goldenrod3, style=filled]; s23[color=green, style=filled]; s25[color=indianred1, style=filled]; s27[color=indianred1, style=filled]; s28[color=goldenrod3, style=filled]; s31[color=green, style=filled]; s32[color=yellow, style=filled]; s33[color=indianred1, style=filled]; s34[color=yellow, style=filled]; s37[color=yellow, style=filled]; s40[color=indianred1, style=filled]; s41[color=yellow, style=filled]; s42[color=green, style=filled]; s43[color=yellow, style=filled]; s48[color=cyan, style=filled]; s50[color=cyan, style=filled]; s51[color=slategray4, style=filled]; s54[color=indianred1, style=filled]; s62[color=indianred1, style=filled]; s64[color=indianred1, style=filled]; s65[color=yellow, style=filled]; s70[color=yellow, style=filled]; s71[color=indianred1, style=filled]; s72[color=goldenrod3, style=filled]; s73[color=yellow, style=filled]; s76[color=yellow, style=filled]; s77[color=cyan, style=filled]; s78[color=yellow, style=filled]; s80[color=green, style=filled]; s83[color=yellow, style=filled]; s91[color=yellow, style=filled]; s92[color=indianred1, style=filled]; s93[color=goldenrod3, style=filled]; s94[color=yellow, style=filled]; s95[color=cyan, style=filled]; }