/*************************************************** * File automatically generated by IMITATOR 2.5.0 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 * 31 states and 40 transitions * Program terminated after 0.162 second ***************************************************/ DESCRIPTION OF THE STATES STATE 0: act_Ptp: WFO, act_Audio: WFO, Audio_Checker: idle ==> & C2 > 0 & D2 >= driftDelta + C2 & audOff >= ptpOff & 2*ptpOff + C1 + C2 > 10 + 2*audOff & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpOff >= cPtp & ptpOff + driftDelta + C1 + C2 > audOff + D2 & cPtp >= 0 & ptpPeriod = 40 & audPeriod = 10 & cPtp = cAudio & rAudioChecker = 0 & cPtp = cAudioChecker STATE 1: act_Ptp: WFP, act_Audio: WFO, Audio_Checker: busy ==> & C2 > 0 & D2 >= driftDelta + C2 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & 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 ==> & D2 >= driftDelta + C2 & C2 > 0 & 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 ==> & D2 >= driftDelta + C2 & C2 > 0 & 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 8: 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 >= 10 + audOff & C2 > 0 & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 20 >= ptpOff + cPtp & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = 10 + audOff + cAudio & ptpOff + C1 + C2 = audOff + rAudioChecker & cPtp = cAudioChecker STATE 9: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: error ==> & 2*ptpOff + C1 + C2 > 10 + 2*audOff & ptpOff >= 0 & ptpOff + D2 >= audOff + driftDelta & driftDelta + cPtp >= D2 & C2 > 0 & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 10 >= ptpOff + cPtp & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = audOff + cAudio & ptpOff + C1 + C2 = audOff + rAudioChecker & cPtp = cAudioChecker STATE 10: 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 >= 10 + audOff & C2 > 0 & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 20 >= ptpOff + cPtp & audOff + 20 >= ptpOff + C1 + 2*C2 & 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 ==> & 2*ptpOff + C1 + C2 > 10 + 2*audOff & ptpOff >= 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & ptpOff + cPtp >= 10 + audOff & C2 > 0 & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 20 >= ptpOff + cPtp & audOff + 20 >= ptpOff + C1 + 2*C2 & 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 ==> & 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 + C2 = audOff + rAudioChecker & cPtp = cAudioChecker STATE 13: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: error ==> & ptpOff >= 0 & ptpOff + driftDelta + C1 + C2 > audOff + D2 & ptpOff + D2 >= 10 + audOff + driftDelta & driftDelta + cPtp >= D2 & C2 > 0 & audOff >= ptpOff & audOff + 20 >= ptpOff + cPtp & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = 10 + audOff + cAudio & ptpOff + C1 + C2 = audOff + rAudioChecker & cPtp = cAudioChecker STATE 14: 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 15: 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 16: 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 17: 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 18: 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 19: 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 20: 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 23: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & 20 >= C1 + 2*C2 & D2 >= driftDelta + C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 40 & cAudio = 0 & C1 + 2*C2 = 10 + rAudioChecker & cAudioChecker = 40 STATE 24: act_Ptp: WFP, act_Audio: WFP, Audio_Checker: check ==> & ptpOff >= 0 & driftDelta + C1 + C2 > D2 & C1 + C2 > 10 & C2 > 0 & 20 >= C1 + 2*C2 & D2 >= driftDelta + C2 & ptpPeriod = 40 & ptpOff = audOff & audPeriod = 10 & cPtp = 40 & cAudio = 0 & C1 + C2 = rAudioChecker & cAudioChecker = 40 STATE 25: 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 26: 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 27: 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 28: 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 29: 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 30: 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 31: 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 32: 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 33: 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 34: 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 35: 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 >= audOff & C2 > 0 & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 10 >= ptpOff + cPtp & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = audOff + cAudio & ptpOff + C1 + C2 = audOff + rAudioChecker & cPtp = cAudioChecker STATE 36: 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 >= audOff & C2 > 0 & D2 >= driftDelta + C2 & audOff >= ptpOff & audOff + 10 >= ptpOff + cPtp & audOff + 20 >= ptpOff + C1 + 2*C2 & ptpPeriod = 40 & audPeriod = 10 & ptpOff + cPtp = audOff + cAudio & C1 + C2 = rAudioChecker & cPtp = cAudioChecker DESCRIPTION OF THE TRANSITIONS s_1 -> s_35 via "Release_Audio" s_1 -> s_36 via "Release_Audio" s_0 -> s_1 via "Release_PTP" s_2 -> s_35 via "Release_PTP" s_3 -> s_36 via "Release_PTP" s_8 -> s_13 s_8 -> s_12 via "Release_Audio" s_10 -> s_14 via "Ending_Audio" s_11 -> s_16 via "Ending_Audio" s_11 -> s_15 via "Release_Audio" s_12 -> s_19 via "Release_Audio" s_14 -> s_18 via "Release_Audio" s_14 -> s_17 via "Release_Audio" s_15 -> s_20 via "Release_Audio" s_17 -> s_26 via "Ending_Audio" s_16 -> s_18 via "Release_Audio" s_16 -> s_17 via "Release_Audio" s_18 -> s_26 via "Ending_Audio" s_17 -> s_25 via "Release_Audio" s_19 -> s_24 via "Release_Audio" s_20 -> s_23 via "Release_Audio" s_25 -> s_29 via "Release_Audio" s_27 -> s_30 via "Ending_Audio" s_26 -> s_28 via "Release_Audio" s_26 -> s_27 via "Release_Audio" s_27 -> s_31 via "Release_Audio" s_28 -> s_30 via "Ending_Audio" s_30 -> s_34 via "Release_Audio" s_30 -> s_33 via "Release_Audio" s_30 -> s_32 via "Release_PTP" s_32 -> s_35 via "Release_Audio" s_32 -> s_36 via "Release_Audio" s_35 -> s_9 s_33 -> s_35 via "Release_PTP" s_35 -> s_8 via "Release_Audio" s_34 -> s_36 via "Release_PTP" s_36 -> s_11 via "Release_Audio" s_36 -> s_10 via "Release_Audio" s_0 -> s_3 via "Release_Audio" s_0 -> s_2 via "Release_Audio"