/*************************************************** * File automatically generated by IMITATOR 2.6.1 for model 'examples/Scheduling/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 * * 78 states and 102 transitions * * Program terminated after 0.376000000001 second * File generated: Sun May 5, 2013 12:01:09 ***************************************************/ DESCRIPTION OF THE STATES STATE 0: act_Ptp: WFO, act_Audio: WFO, Audio_Checker: idle ==> & 2*ptpOff + C1 + C2 > 10 + 2*audOff & ptpOff + driftDelta + C1 + C2 > audOff + D2 & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpOff >= cPtp & C2 > 0 & cPtp >= 0 & ptpPeriod = 40 & audPeriod = 10 & cPtp = cAudio & rAudioChecker = 0 & cPtp = cAudioChecker STATE 1: act_Ptp: WFP, act_Audio: WFO, Audio_Checker: busy ==> & ptpOff + driftDelta + C1 + C2 > audOff + D2 & C2 > 0 & D2 >= driftDelta + C2 & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpOff >= 0 & cPtp >= 0 & 2*ptpOff + C1 + C2 > 10 + 2*audOff & audOff >= ptpOff + cPtp & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = cAudio & C1 = rAudioChecker & cPtp = cAudioChecker STATE 2: act_Ptp: WFO, act_Audio: WFP, Audio_Checker: check ==> & C2 > 0 & D2 >= driftDelta + C2 & 20 >= C1 + 2*C2 & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & ptpOff = cPtp & cAudio = 0 & C2 = rAudioChecker & cAudioChecker = 0 STATE 3: act_Ptp: WFO, act_Audio: WFP, Audio_Checker: busy ==> & C2 > 0 & D2 >= driftDelta + C2 & 20 >= C1 + 2*C2 & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & ptpOff = cPtp & cAudio = 0 & C2 = rAudioChecker & cAudioChecker = 0 STATE 4: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> & ptpOff >= 0 & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpOff + cPtp >= audOff & C2 > 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & 2*ptpOff + C1 + C2 > 10 + 2*audOff & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 10 >= ptpOff + cPtp & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = audOff + cAudio & C1 + C2 = rAudioChecker & cPtp = cAudioChecker STATE 5: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & D2 >= driftDelta + C2 & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpOff >= 0 & C2 > 0 & ptpOff + cPtp >= audOff & ptpOff + driftDelta + C1 + C2 > audOff + D2 & 2*ptpOff + C1 + C2 > 10 + 2*audOff & audOff >= ptpOff & audOff + 10 >= ptpOff + cPtp & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = audOff + cAudio & ptpOff + C1 + C2 = audOff + rAudioChecker & cPtp = cAudioChecker STATE 6: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & C2 > 0 & D2 >= driftDelta + C2 & 20 >= C1 + 2*C2 & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & cPtp >= 0 & 10 >= cPtp & C1 + C2 > 10 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = cAudio & C1 + C2 = rAudioChecker & cPtp = cAudioChecker STATE 7: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> & 20 >= C1 + 2*C2 & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C2 > 0 & cPtp >= 0 & 10 >= cPtp & C1 + C2 > 10 & D2 >= driftDelta + C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = cAudio & C1 + C2 = rAudioChecker & cPtp = cAudioChecker STATE 8: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & 20 >= C1 + 2*C2 & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C2 > 0 & cPtp >= 10 & 20 >= cPtp & C1 + C2 > 10 & D2 >= driftDelta + C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 10 + cAudio & C1 + C2 = rAudioChecker & cPtp = cAudioChecker STATE 9: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: error ==> & 20 >= C1 + 2*C2 & driftDelta + cPtp >= D2 & D2 >= driftDelta + C2 & C2 > 0 & 10 >= cPtp & C1 + C2 > 10 & ptpOff >= 0 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = cAudio & C1 + C2 = rAudioChecker & cPtp = cAudioChecker STATE 10: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> & ptpOff >= 0 & D2 >= driftDelta + C2 & ptpOff + cPtp >= 10 + audOff & 2*ptpOff + C1 + C2 > 10 + 2*audOff & C2 > 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & audOff + 20 >= ptpOff + C1 + 2*C2 & audOff >= ptpOff & audOff + 20 >= ptpOff + cPtp & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = 10 + audOff + cAudio & C1 + 2*C2 = rAudioChecker & cPtp = cAudioChecker STATE 11: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & D2 >= driftDelta + C2 & ptpOff + cPtp >= 10 + audOff & 2*ptpOff + C1 + C2 > 10 + 2*audOff & C2 > 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & audOff + 20 >= ptpOff + C1 + 2*C2 & audOff >= ptpOff & audOff + 20 >= ptpOff + cPtp & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = 10 + audOff + cAudio & ptpOff + C1 + 2*C2 = 10 + audOff + rAudioChecker & cPtp = cAudioChecker STATE 12: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & D2 >= driftDelta + C2 & ptpOff + cPtp >= 10 + audOff & ptpOff >= 0 & C2 > 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & 2*ptpOff + C1 + C2 > 10 + 2*audOff & audOff + 20 >= ptpOff + C1 + 2*C2 & audOff >= ptpOff & audOff + 20 >= ptpOff + cPtp & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = 10 + audOff + cAudio & ptpOff + C1 + C2 = audOff + rAudioChecker & cPtp = cAudioChecker STATE 13: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: error ==> & ptpOff >= 0 & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpOff + D2 >= audOff + driftDelta & driftDelta + cPtp >= D2 & C2 > 0 & D2 >= driftDelta + C2 & 2*ptpOff + C1 + C2 > 10 + 2*audOff & audOff >= ptpOff & audOff + 10 >= ptpOff + cPtp & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = audOff + cAudio & ptpOff + C1 + C2 = audOff + rAudioChecker & cPtp = cAudioChecker STATE 14: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & 20 >= C1 + 2*C2 & C2 > 0 & cPtp >= 10 & 20 >= cPtp & D2 >= driftDelta + C2 & ptpOff >= 0 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 10 + cAudio & C1 + 2*C2 = rAudioChecker & cPtp = cAudioChecker STATE 15: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & 20 >= C1 + 2*C2 & C2 > 0 & cPtp >= 10 & 20 >= cPtp & D2 >= driftDelta + C2 & ptpOff >= 0 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 10 + cAudio & C1 + 2*C2 = 10 + rAudioChecker & cPtp = cAudioChecker STATE 16: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff + driftDelta + C1 + C2 > audOff + D2 & 2*ptpOff + C1 + C2 > 10 + 2*audOff & ptpOff + cPtp >= 20 + audOff & C2 > 0 & audOff + 20 >= ptpOff + C1 + 2*C2 & D2 >= driftDelta + C2 & ptpOff >= 0 & audOff >= ptpOff & audOff + 30 >= ptpOff + cPtp & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = 20 + audOff + cAudio & ptpOff + C1 + C2 = audOff + rAudioChecker & cPtp = cAudioChecker STATE 17: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: error ==> & ptpOff + driftDelta + C1 + C2 > audOff + D2 & ptpOff >= 0 & ptpOff + D2 >= 10 + audOff + driftDelta & driftDelta + cPtp >= D2 & C2 > 0 & audOff + 20 >= ptpOff + C1 + 2*C2 & audOff >= ptpOff & audOff + 20 >= ptpOff + cPtp & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = 10 + audOff + cAudio & ptpOff + C1 + C2 = audOff + rAudioChecker & cPtp = cAudioChecker STATE 18: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & 20 >= C1 + 2*C2 & C2 > 0 & cPtp >= 20 & 30 >= cPtp & D2 >= driftDelta + C2 & ptpOff >= 0 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 20 + cAudio & C1 + C2 = rAudioChecker & cPtp = cAudioChecker STATE 19: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: error ==> & driftDelta + C1 + C2 > D2 & driftDelta + cPtp >= D2 & ptpOff >= 0 & C2 > 0 & 20 >= cPtp & 20 >= C1 + 2*C2 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 10 + cAudio & C1 + C2 = rAudioChecker & cPtp = cAudioChecker STATE 20: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> & 2*ptpOff + C1 + C2 > 10 + 2*audOff & ptpOff >= 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & C2 > 0 & cPtp >= C1 + 2*C2 & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 20 >= ptpOff + cPtp & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = 10 + audOff + cAudio & C1 + 2*C2 = rAudioChecker & cPtp = cAudioChecker STATE 21: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & 2*ptpOff + C1 + C2 > 10 + 2*audOff & ptpOff >= 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & ptpOff + cPtp >= 20 + audOff & C2 > 0 & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 30 >= ptpOff + cPtp & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = 20 + audOff + cAudio & ptpOff + C1 + 2*C2 = 10 + audOff + rAudioChecker & cPtp = cAudioChecker STATE 22: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & cPtp >= 10 & 20 >= cPtp & 20 > C1 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 10 + cAudio & rAudioChecker = 10 & cPtp = cAudioChecker STATE 23: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & 20 >= cPtp & cPtp >= C1 + 2*C2 & D2 >= driftDelta + C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 10 + cAudio & C1 + 2*C2 = rAudioChecker & cPtp = cAudioChecker STATE 24: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & cPtp >= 20 & 30 >= cPtp & 20 >= C1 + 2*C2 & D2 >= driftDelta + C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 20 + cAudio & C1 + 2*C2 = 10 + rAudioChecker & cPtp = cAudioChecker STATE 25: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & cPtp >= 20 & 30 >= cPtp & 20 >= C1 + 2*C2 & D2 >= driftDelta + C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 20 + cAudio & C2 = rAudioChecker & cPtp = 20 + cAudioChecker STATE 26: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & cPtp >= 20 & 30 >= cPtp & 20 >= C1 + 2*C2 & D2 >= driftDelta + C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 20 + cAudio & C2 = rAudioChecker & cPtp = 20 + cAudioChecker STATE 27: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & 2*ptpOff + C1 + C2 > 10 + 2*audOff & ptpOff >= 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & ptpOff + cPtp >= 20 + audOff & C2 > 0 & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 30 >= ptpOff + cPtp & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = 20 + audOff + cAudio & C2 = rAudioChecker & ptpOff + cPtp = 20 + audOff + cAudioChecker STATE 28: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> & 2*ptpOff + C1 + C2 > 10 + 2*audOff & ptpOff >= 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & ptpOff + cPtp >= 20 + audOff & C2 > 0 & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 30 >= ptpOff + cPtp & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = 20 + audOff + cAudio & C2 = rAudioChecker & ptpOff + cPtp = 20 + audOff + cAudioChecker STATE 29: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & 2*ptpOff + C1 + C2 > 10 + 2*audOff & ptpOff >= 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & ptpOff + cPtp >= 30 + audOff & C2 > 0 & 40 >= cPtp & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = 30 + audOff + cAudio & ptpOff + C1 + C2 = audOff + rAudioChecker & cPtp = cAudioChecker STATE 30: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & cPtp >= 30 & 40 >= cPtp & 20 >= C1 + 2*C2 & D2 >= driftDelta + C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 30 + cAudio & C1 + C2 = rAudioChecker & cPtp = cAudioChecker STATE 31: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & 2*ptpOff + C1 + C2 > 10 + 2*audOff & ptpOff >= 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & ptpOff + cPtp >= 30 + audOff & C2 > 0 & 40 >= cPtp & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = 30 + audOff + cAudio & ptpOff + C1 + 2*C2 = 10 + audOff + rAudioChecker & cPtp = cAudioChecker STATE 32: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & cPtp >= 20 & 30 >= cPtp & 20 > C1 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 20 + cAudio & C1 + 2*rAudioChecker = 20 & cPtp = 20 + cAudioChecker STATE 33: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & cPtp >= 20 & 30 >= cPtp & 20 > C1 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 20 + cAudio & C1 + 2*rAudioChecker = 20 & cPtp = 20 + cAudioChecker STATE 34: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & cPtp >= 30 & 40 >= cPtp & 20 >= C1 + 2*C2 & D2 >= driftDelta + C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 30 + cAudio & C1 + 2*C2 = 10 + rAudioChecker & cPtp = cAudioChecker STATE 35: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & C1 + 2*cPtp >= 60 & 30 >= cPtp & 20 > C1 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 20 + cAudio & C1 + 2*rAudioChecker = 20 & cPtp = 20 + cAudioChecker STATE 36: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & cPtp >= 30 & 40 >= cPtp & 20 > C1 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 30 + cAudio & C1 + 2*rAudioChecker = 20 & cPtp = 20 + cAudioChecker STATE 37: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> & 2*ptpOff + C1 + C2 > 10 + 2*audOff & ptpOff >= 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & ptpOff + cPtp >= 20 + audOff + C2 & C2 > 0 & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 30 >= ptpOff + cPtp & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = 20 + audOff + cAudio & C2 = rAudioChecker & ptpOff + cPtp = 20 + audOff + cAudioChecker STATE 38: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & 2*ptpOff + C1 + C2 > 10 + 2*audOff & ptpOff >= 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & ptpOff + cPtp >= 30 + audOff & C2 > 0 & 40 >= cPtp & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = 30 + audOff + cAudio & C2 = rAudioChecker & ptpOff + cPtp = 20 + audOff + cAudioChecker STATE 39: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> & 2*ptpOff + C1 + C2 > 10 + 2*audOff & ptpOff >= 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & ptpOff + cPtp >= 20 + audOff + C2 & C2 > 0 & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 30 >= ptpOff + cPtp & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpOff + cPtp = 20 + audOff + cAudioChecker & ptpOff + cPtp = 20 + audOff + cAudio & ptpPeriod = 40 & audPeriod = 10 & C2 = rAudioChecker STATE 40: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & 40 >= cPtp & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & cPtp >= 30 & 20 >= C1 + 2*C2 & D2 >= driftDelta + C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 30 + cAudio & C2 = rAudioChecker & cPtp = 20 + cAudioChecker STATE 41: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> & 30 >= cPtp & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & cPtp >= 20 + C2 & 20 >= C1 + 2*C2 & D2 >= driftDelta + C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 20 + cAudio & C2 = rAudioChecker & cPtp = 20 + cAudioChecker STATE 42: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & D2 >= driftDelta + C2 & 20 >= C1 + 2*C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 40 & cAudio = 0 & C1 + C2 = rAudioChecker & cAudioChecker = 40 STATE 43: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & D2 >= driftDelta + C2 & 20 >= C1 + 2*C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 40 & cAudio = 0 & C1 + 2*C2 = 10 + rAudioChecker & cAudioChecker = 40 STATE 44: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & 40 >= cPtp & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & cPtp >= 30 & 20 >= C1 + 2*C2 & D2 >= driftDelta + C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 30 + cAudio & C2 = rAudioChecker & cPtp = 30 + cAudioChecker STATE 45: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> & 40 >= cPtp & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & cPtp >= 30 & 20 >= C1 + 2*C2 & D2 >= driftDelta + C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 30 + cAudio & C2 = rAudioChecker & cPtp = 30 + cAudioChecker STATE 46: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & D2 >= driftDelta + C2 & 20 >= C1 + 2*C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 40 & cAudio = 0 & C2 = rAudioChecker & cAudioChecker = 20 STATE 47: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & 40 >= cPtp & 2*ptpOff + C1 + C2 > 10 + 2*audOff & ptpOff >= 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & C2 > 0 & ptpOff + cPtp >= 30 + audOff & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = 30 + audOff + cAudio & C2 = rAudioChecker & ptpOff + cPtp = 30 + audOff + cAudioChecker STATE 48: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> & 40 >= cPtp & 2*ptpOff + C1 + C2 > 10 + 2*audOff & ptpOff >= 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & C2 > 0 & ptpOff + cPtp >= 30 + audOff & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = 30 + audOff + cAudio & C2 = rAudioChecker & ptpOff + cPtp = 30 + audOff + cAudioChecker STATE 49: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & 40 >= cPtp & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & cPtp >= 30 & 20 > C1 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 30 + cAudio & C1 + 2*rAudioChecker = 20 & cPtp = 30 + cAudioChecker STATE 50: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> & 40 >= cPtp & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & cPtp >= 30 & 20 > C1 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 30 + cAudio & C1 + 2*rAudioChecker = 20 & cPtp = 30 + cAudioChecker STATE 51: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & D2 >= 10 + driftDelta & 20 > C1 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 40 & cAudio = 0 & C1 + 2*rAudioChecker = 20 & cAudioChecker = 20 STATE 52: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> & 40 >= cPtp & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & C1 + 2*cPtp >= 80 & 20 > C1 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 30 + cAudio & C1 + 2*rAudioChecker = 20 & cPtp = 30 + cAudioChecker STATE 53: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & D2 >= 10 + driftDelta & 20 > C1 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 40 & cAudio = 0 & C1 + 2*rAudioChecker = 20 & cAudioChecker = 10 STATE 54: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & D2 >= driftDelta + C2 & 20 >= C1 + 2*C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 40 & cAudio = 0 & C2 = rAudioChecker & cAudioChecker = 10 STATE 55: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> & 40 >= cPtp & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & cPtp >= 30 + C2 & 20 >= C1 + 2*C2 & D2 >= driftDelta + C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 30 + cAudio & C2 = rAudioChecker & cPtp = 30 + cAudioChecker STATE 56: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> & 40 >= cPtp & 2*ptpOff + C1 + C2 > 10 + 2*audOff & ptpOff >= 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & C2 > 0 & ptpOff + cPtp >= 30 + audOff + C2 & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = 30 + audOff + cAudio & C2 = rAudioChecker & ptpOff + cPtp = 30 + audOff + cAudioChecker STATE 57: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & D2 >= 10 + driftDelta & 20 > C1 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 0 & cAudio = 10 & C1 = rAudioChecker & cAudioChecker = 0 STATE 58: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & D2 >= 10 + driftDelta & 20 > C1 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 40 & cAudio = 0 & C1 + 2*rAudioChecker = 20 & cAudioChecker = 0 STATE 59: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & D2 >= 10 + driftDelta & 20 > C1 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 40 & cAudio = 0 & C1 + 2*rAudioChecker = 20 & cAudioChecker = 0 STATE 60: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & D2 >= driftDelta + C2 & 20 >= C1 + 2*C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 0 & cAudio = 10 & C1 = rAudioChecker & cAudioChecker = 0 STATE 61: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & D2 >= driftDelta + C2 & 20 >= C1 + 2*C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 40 & cAudio = 0 & C2 = rAudioChecker & cAudioChecker = 0 STATE 62: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & D2 >= driftDelta + C2 & 20 >= C1 + 2*C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 40 & cAudio = 0 & C2 = rAudioChecker & cAudioChecker = 0 STATE 63: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> & 2*ptpOff + C1 + C2 > 10 + 2*audOff & ptpOff >= 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & C2 > 0 & cPtp >= 0 & D2 >= driftDelta + C2 & audOff >= ptpOff + cPtp & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp + 10 = audOff + cAudio & C1 = rAudioChecker & cPtp = cAudioChecker STATE 64: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> & 10 >= cPtp & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & cPtp >= 0 & 20 > C1 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = cAudio & C1 + 20 = 2*rAudioChecker & cPtp = cAudioChecker STATE 65: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & 10 >= cPtp & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & cPtp >= 0 & 20 > C1 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = cAudio & C1 + 20 = 2*rAudioChecker & cPtp = cAudioChecker STATE 66: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & 20 >= cPtp & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & cPtp >= 10 & 20 > C1 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 10 + cAudio & C1 + 20 = 2*rAudioChecker & cPtp = cAudioChecker STATE 67: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: error ==> & ptpOff >= 0 & C1 > 0 & 20 > C1 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & driftDelta + 10 = D2 & C1 + 2*C2 = 20 & cPtp = 10 & cAudio = 10 & C1 + 20 = 2*rAudioChecker & cAudioChecker = 10 STATE 68: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: busy ==> & 20 >= cPtp & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & cPtp >= 10 & 20 > C1 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 10 + cAudio & rAudioChecker = 20 & cPtp = cAudioChecker STATE 69: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & 20 >= cPtp & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & cPtp >= 10 & 20 > C1 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 10 + cAudio & rAudioChecker = 10 & cPtp = cAudioChecker STATE 70: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & 30 >= cPtp & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & cPtp >= 20 & 20 > C1 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 20 + cAudio & C1 + 20 = 2*rAudioChecker & cPtp = cAudioChecker STATE 71: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: error ==> & 20 >= cPtp & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & driftDelta + cPtp >= D2 & 20 > C1 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 10 + cAudio & C1 + 20 = 2*rAudioChecker & cPtp = cAudioChecker STATE 72: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: idle ==> & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & D2 >= 10 + driftDelta & 20 > C1 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 20 & cAudio = 10 & rAudioChecker = 20 & cAudioChecker = 20 STATE 73: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & 30 >= cPtp & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & cPtp >= 20 & 20 > C1 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 20 + cAudio & rAudioChecker = 10 & cPtp = cAudioChecker STATE 74: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & 40 >= cPtp & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & cPtp >= 30 & 20 > C1 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 30 + cAudio & C1 + 20 = 2*rAudioChecker & cPtp = cAudioChecker STATE 75: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & 40 >= cPtp & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & cPtp >= 30 & 20 > C1 & D2 >= 10 + driftDelta & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 30 + cAudio & rAudioChecker = 10 & cPtp = cAudioChecker STATE 76: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & D2 >= 10 + driftDelta & 20 > C1 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 40 & cAudio = 0 & C1 + 20 = 2*rAudioChecker & cAudioChecker = 40 STATE 77: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & 2*driftDelta + C1 + 20 > 2*D2 & D2 >= 10 + driftDelta & 20 > C1 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & C1 + 2*C2 = 20 & cPtp = 40 & cAudio = 0 & rAudioChecker = 10 & cAudioChecker = 40 DESCRIPTION OF THE TRANSITIONS s_1 -> s_5 via "Release_Audio" s_1 -> s_4 via "Release_Audio" s_0 -> s_1 via "Release_PTP" s_5 -> s_13 s_2 -> s_6 via "Release_PTP" s_4 -> s_11 via "Release_Audio" s_4 -> s_10 via "Release_Audio" s_6 -> s_9 s_3 -> s_7 via "Release_PTP" s_5 -> s_12 via "Release_Audio" s_8 -> s_19 s_6 -> s_8 via "Release_Audio" s_7 -> s_15 via "Release_Audio" s_7 -> s_14 via "Release_Audio" s_8 -> s_18 via "Release_Audio" s_10 -> s_20 via "Ending_Audio" s_11 -> s_22 via "Ending_Audio" s_12 -> s_17 s_11 -> s_21 via "Release_Audio" s_12 -> s_16 via "Release_Audio" s_14 -> s_23 via "Ending_Audio" s_15 -> s_22 via "Ending_Audio" s_15 -> s_24 via "Release_Audio" s_16 -> s_29 via "Release_Audio" s_18 -> s_30 via "Release_Audio" s_20 -> s_28 via "Release_Audio" s_20 -> s_27 via "Release_Audio" s_21 -> s_31 via "Release_Audio" s_22 -> s_33 via "Release_Audio" s_22 -> s_32 via "Release_Audio" s_23 -> s_26 via "Release_Audio" s_23 -> s_25 via "Release_Audio" s_25 -> s_41 via "Ending_Audio" s_24 -> s_34 via "Release_Audio" s_26 -> s_41 via "Ending_Audio" s_25 -> s_40 via "Release_Audio" s_27 -> s_39 via "Ending_Audio" s_27 -> s_38 via "Release_Audio" s_28 -> s_37 via "Ending_Audio" s_29 -> s_42 via "Release_Audio" s_30 -> s_42 via "Release_Audio" s_31 -> s_43 via "Release_Audio" s_32 -> s_35 via "Ending_Audio" s_32 -> s_36 via "Release_Audio" s_33 -> s_35 via "Ending_Audio" s_34 -> s_43 via "Release_Audio" s_35 -> s_50 via "Release_Audio" s_35 -> s_49 via "Release_Audio" s_36 -> s_51 via "Release_Audio" s_37 -> s_48 via "Release_Audio" s_37 -> s_47 via "Release_Audio" s_38 -> s_46 via "Release_Audio" s_39 -> s_48 via "Release_Audio" s_39 -> s_47 via "Release_Audio" s_40 -> s_46 via "Release_Audio" s_41 -> s_45 via "Release_Audio" s_41 -> s_44 via "Release_Audio" s_44 -> s_55 via "Ending_Audio" s_45 -> s_55 via "Ending_Audio" s_44 -> s_54 via "Release_Audio" s_47 -> s_56 via "Ending_Audio" s_48 -> s_56 via "Ending_Audio" s_47 -> s_54 via "Release_Audio" s_49 -> s_52 via "Ending_Audio" s_49 -> s_53 via "Release_Audio" s_50 -> s_52 via "Ending_Audio" s_52 -> s_59 via "Release_Audio" s_52 -> s_58 via "Release_Audio" s_52 -> s_57 via "Release_PTP" s_55 -> s_62 via "Release_Audio" s_55 -> s_61 via "Release_Audio" s_56 -> s_62 via "Release_Audio" s_56 -> s_61 via "Release_Audio" s_55 -> s_60 via "Release_PTP" s_57 -> s_65 via "Release_Audio" s_57 -> s_64 via "Release_Audio" s_56 -> s_63 via "Release_PTP" s_58 -> s_65 via "Release_PTP" s_59 -> s_64 via "Release_PTP" s_60 -> s_6 via "Release_Audio" s_60 -> s_7 via "Release_Audio" s_61 -> s_6 via "Release_PTP" s_65 -> s_67 s_63 -> s_5 via "Release_Audio" s_63 -> s_4 via "Release_Audio" s_62 -> s_7 via "Release_PTP" s_66 -> s_71 s_64 -> s_69 via "Release_Audio" s_64 -> s_68 via "Release_Audio" s_65 -> s_66 via "Release_Audio" s_66 -> s_70 via "Release_Audio" s_68 -> s_72 via "Ending_Audio" s_69 -> s_22 via "Ending_Audio" s_69 -> s_73 via "Release_Audio" s_70 -> s_74 via "Release_Audio" s_72 -> s_33 via "Release_Audio" s_72 -> s_32 via "Release_Audio" s_73 -> s_75 via "Release_Audio" s_74 -> s_76 via "Release_Audio" s_75 -> s_77 via "Release_Audio" s_0 -> s_3 via "Release_Audio" s_0 -> s_2 via "Release_Audio"