/*************************************************** * File automatically generated by IMITATOR 2.6.1 snapshot for model 'examples/Latch/latchValmem.imi' * * The following pi0 was considered: dClockHigh = 1000 & dClockLow = 1000 & dSetup = 1 & dHold = 350 & dNot1Down = 147 & dNot1Up = 219 & dNot2Down = 163 & dNot2Up = 155 & dXorDown1Up = 416 & dXorUp2Up = 147 & dAndUp2 = 80 & dAndDown1 = 155 & dLatchUp = 240 * * 12 states and 12 transitions * * Program terminated after 0.069 second * File generated: Fri Apr 19, 2013 10:37:23 ***************************************************/ DESCRIPTION OF THE STATES STATE 0: clock1: ClockLow1, d1: DLow1, not1: Not1High1, not2: Not2Low1, xor1: XorLow1, and1: AndLow1, latch1: LatchD0E0, q = 2 ==> & dHold > dAndUp2 + dLatchUp & dNot1Down > dAndUp2 & dXorUp2Up > dAndUp2 & dAndUp2 + dLatchUp > dXorUp2Up & dAndUp2 + dLatchUp > dNot1Down & dAndUp2 + dLatchUp > dNot1Down + dNot2Up & dNot1Down + dNot2Up + dXorDown1Up > dHold & dClockLow >= s & dClockLow >= dSetup + s & s >= 0 & s = ckClock & s = ckD & s = ckNot1 & s = ckNot2 & s = ckXor & s = ckAnd & s = ckLatch STATE 1: clock1: ClockLow1, d1: DHigh1, not1: Not1High1, not2: Not2Low1, xor1: XorLow1, and1: AndLow1, latch1: LatchD1E0, q = 2 ==> & dHold > dAndUp2 + dLatchUp & dNot1Down > dAndUp2 & dXorUp2Up > dAndUp2 & dAndUp2 + dLatchUp > dXorUp2Up & dAndUp2 + dLatchUp > dNot1Down & dAndUp2 + dLatchUp > dNot1Down + dNot2Up & dNot1Down + dNot2Up + dXorDown1Up > dHold & dClockLow >= s & dClockLow >= dSetup & dSetup + s >= dClockLow & s = ckClock & dClockLow + ckD = dSetup + s & s = ckNot1 & s = ckNot2 & s = ckXor & s = ckAnd & s = ckLatch STATE 2: clock1: ClockHigh1, d1: DHigh2, not1: Not1High1bis, not2: Not2Low1, xor1: XorLow1bis, and1: AndLow1bis, latch1: LatchD1E0, q = 2 ==> & dAndUp2 + dLatchUp > dXorUp2Up & dAndUp2 + dLatchUp > dNot1Down & dAndUp2 + dLatchUp > dNot1Down + dNot2Up & dNot1Down + dNot2Up + dXorDown1Up > dHold & dClockHigh + dClockLow >= s & dXorUp2Up > dAndUp2 & dNot1Down > dAndUp2 & dHold > dAndUp2 + dLatchUp & dClockLow + dAndUp2 >= s & dClockLow >= dSetup & dSetup >= 0 & s >= dClockLow & dClockLow + ckClock = s & dClockLow + ckD = s & dClockLow + ckNot1 = s & s = ckNot2 & dClockLow + ckXor = s & dClockLow + ckAnd = s & s = ckLatch STATE 3: clock1: ClockHigh1, d1: DHigh2, not1: Not1High1bis, not2: Not2Low1, xor1: XorLow1bis, and1: AndHigh1, latch1: LatchD1E1, q = 2 ==> & dAndUp2 + dLatchUp > dNot1Down & dAndUp2 + dLatchUp > dNot1Down + dNot2Up & dNot1Down + dNot2Up + dXorDown1Up > dHold & dClockHigh + dClockLow >= s & dClockLow + dNot1Down >= s & dClockLow + dXorUp2Up >= s & dAndUp2 + dLatchUp > dXorUp2Up & dClockLow >= dSetup & dSetup >= 0 & dHold > dAndUp2 + dLatchUp & dNot1Down > dAndUp2 & dXorUp2Up > dAndUp2 & dAndUp2 >= 0 & s >= dClockLow + dAndUp2 & dClockLow + ckClock = s & dClockLow + ckD = s & dClockLow + ckNot1 = s & s = ckNot2 & dClockLow + ckXor = s & dClockLow + ckAnd = s & dClockLow + dAndUp2 + ckLatch = s STATE 4: clock1: ClockHigh1, d1: DHigh2, not1: Not1Low1, not2: Not2Low1bis, xor1: XorLow1bis, and1: AndHigh1, latch1: LatchD1E1, q = 2 ==> & dAndUp2 + dLatchUp > dNot1Down + dNot2Up & dNot1Down + dNot2Up + dXorDown1Up > dHold & dClockHigh + dClockLow >= s & dClockLow + dNot1Down + dNot2Up >= s & dClockLow + dXorUp2Up >= s & dAndUp2 + dLatchUp > dXorUp2Up & dClockLow >= dSetup & dSetup >= 0 & dHold > dAndUp2 + dLatchUp & dNot1Down > dAndUp2 & dAndUp2 >= 0 & s >= dClockLow + dNot1Down & dClockLow + ckClock = s & dClockLow + ckD = s & dClockLow + ckNot1 = s & dClockLow + dNot1Down + ckNot2 = s & dClockLow + ckXor = s & dClockLow + ckAnd = s & dClockLow + dAndUp2 + ckLatch = s STATE 5: clock1: ClockHigh1, d1: DHigh2, not1: Not1High1bis, not2: Not2Low1, xor1: XorHigh1, and1: AndHigh1, latch1: LatchD1E1, q = 2 ==> & dNot1Down + dNot2Up + dXorDown1Up > dHold & dClockHigh + dClockLow >= s & dAndUp2 + dLatchUp > dNot1Down + dNot2Up & dClockLow + dNot1Down >= s & dAndUp2 + dLatchUp > dNot1Down & dClockLow >= dSetup & dSetup >= 0 & dHold > dAndUp2 + dLatchUp & dXorUp2Up > dAndUp2 & dAndUp2 >= 0 & s >= dClockLow + dXorUp2Up & dClockLow + ckClock = s & dClockLow + ckD = s & dClockLow + ckNot1 = s & s = ckNot2 & dClockLow + ckXor = s & dClockLow + ckAnd = s & dClockLow + dAndUp2 + ckLatch = s STATE 6: clock1: ClockHigh1, d1: DHigh2, not1: Not1Low1, not2: Not2Low1bis, xor1: XorHigh1, and1: AndHigh1, latch1: LatchD1E1, q = 2 ==> & dClockLow + dNot1Down + dNot2Up >= s & dClockLow >= dSetup & dSetup >= 0 & dClockHigh + dClockLow >= s & dNot1Down + dNot2Up + dXorDown1Up > dHold & dNot1Down > dAndUp2 & dXorUp2Up > dAndUp2 & dAndUp2 >= 0 & dAndUp2 + dLatchUp > dNot1Down + dNot2Up & dHold > dAndUp2 + dLatchUp & s >= dClockLow + dXorUp2Up & s >= dClockLow + dNot1Down & dClockLow + ckClock = s & dClockLow + ckD = s & dClockLow + ckNot1 = s & dClockLow + dNot1Down + ckNot2 = s & dClockLow + ckXor = s & dClockLow + ckAnd = s & dClockLow + dAndUp2 + ckLatch = s STATE 8: clock1: ClockHigh1, d1: DHigh2, not1: Not1Low1, not2: Not2High1, xor1: XorHigh1bis, and1: AndHigh1, latch1: LatchD1E1, q = 2 ==> & dClockHigh + dClockLow >= s & dClockLow + dAndUp2 + dLatchUp >= s & dClockLow >= dSetup & dSetup >= 0 & dNot1Down + dNot2Up + dXorDown1Up > dHold & dNot1Down + dNot2Up >= dXorUp2Up & dNot1Down > dAndUp2 & dNot2Up >= 0 & dXorUp2Up > dAndUp2 & dAndUp2 >= 0 & dAndUp2 + dLatchUp > dNot1Down + dNot2Up & dHold > dAndUp2 + dLatchUp & s >= dClockLow + dNot1Down + dNot2Up & dClockLow + ckClock = s & dClockLow + ckD = s & dClockLow + ckNot1 = s & dClockLow + dNot1Down + ckNot2 = s & dClockLow + dNot1Down + dNot2Up + ckXor = s & dClockLow + ckAnd = s & dClockLow + dAndUp2 + ckLatch = s STATE 9: clock1: ClockHigh1, d1: DHigh2, not1: Not1Low1, not2: Not2High1, xor1: XorHigh1bis, and1: AndHigh1, latch1: LatchD1E1B, q = 1 ==> & dClockLow + dHold >= s & dClockHigh + dClockLow >= s & dClockLow >= dSetup & dSetup >= 0 & dHold > dAndUp2 + dLatchUp & dNot1Down + dNot2Up + dXorDown1Up > dHold & dNot1Down + dNot2Up >= dXorUp2Up & dNot1Down > dAndUp2 & dNot2Up >= 0 & dXorUp2Up > dAndUp2 & dAndUp2 >= 0 & dAndUp2 + dLatchUp > dNot1Down + dNot2Up & s >= dClockLow + dAndUp2 + dLatchUp & dClockLow + ckClock = s & dClockLow + ckD = s & dClockLow + ckNot1 = s & dClockLow + dNot1Down + ckNot2 = s & dClockLow + dNot1Down + dNot2Up + ckXor = s & dClockLow + ckAnd = s & dClockLow + dAndUp2 + ckLatch = s STATE 10: clock1: ClockHigh1, d1: DLow2, not1: Not1Low1, not2: Not2High1, xor1: XorHigh1bis, and1: AndHigh1, latch1: LatchD0E1, q = 1 ==> & dNot1Down + dNot2Up + dXorDown1Up > dHold & dClockHigh + dClockLow >= s & dClockLow + dNot1Down + dNot2Up + dXorDown1Up >= s & dClockLow >= dSetup & dSetup >= 0 & dHold > dAndUp2 + dLatchUp & dNot1Down + dNot2Up >= dXorUp2Up & dNot1Down > dAndUp2 & dNot2Up >= 0 & dXorUp2Up > dAndUp2 & dAndUp2 >= 0 & dAndUp2 + dLatchUp > dNot1Down + dNot2Up & s >= dClockLow + dHold & dClockLow + ckClock = s & dClockLow + ckD = s & dClockLow + ckNot1 = s & dClockLow + dNot1Down + ckNot2 = s & dClockLow + dNot1Down + dNot2Up + ckXor = s & dClockLow + ckAnd = s & dClockLow + dAndUp2 + ckLatch = s STATE 11: clock1: ClockHigh1, d1: DLow2, not1: Not1Low1, not2: Not2High1, xor1: XorLow2, and1: AndHigh1bis, latch1: LatchD0E1, q = 1 ==> & dClockLow + dNot1Down + dNot2Up + dXorDown1Up + dAndDown1 >= s & dClockLow >= dSetup & dSetup >= 0 & dHold > dAndUp2 + dLatchUp & dNot1Down + dNot2Up >= dXorUp2Up & dNot1Down > dAndUp2 & dNot2Up >= 0 & dXorUp2Up > dAndUp2 & dAndUp2 >= 0 & dClockHigh + dClockLow >= s & dAndUp2 + dLatchUp > dNot1Down + dNot2Up & s >= dClockLow + dNot1Down + dNot2Up + dXorDown1Up & dNot1Down + dNot2Up + dXorDown1Up > dHold & dClockLow + ckD = s & dClockLow + ckNot1 = s & dClockLow + dNot1Down + ckNot2 = s & dClockLow + dNot1Down + dNot2Up + ckXor = s & dClockLow + dNot1Down + dNot2Up + dXorDown1Up + ckAnd = s & dClockLow + dAndUp2 + ckLatch = s & dClockLow + ckClock = s STATE 12: clock1: ClockHigh1, d1: DLow2, not1: Not1Low1, not2: Not2High1, xor1: XorLow2, and1: AndLow2, latch1: LatchD0E0, q = 1 ==> & dClockHigh + dClockLow >= s & dClockLow >= dSetup & dSetup >= 0 & dHold > dAndUp2 + dLatchUp & dNot1Down + dNot2Up >= dXorUp2Up & dNot1Down > dAndUp2 & dNot2Up >= 0 & dXorUp2Up > dAndUp2 & dAndUp2 >= 0 & dAndDown1 >= 0 & dAndUp2 + dLatchUp > dNot1Down + dNot2Up & s >= dClockLow + dNot1Down + dNot2Up + dXorDown1Up + dAndDown1 & dNot1Down + dNot2Up + dXorDown1Up > dHold & dClockLow + ckD = s & dClockLow + ckNot1 = s & dClockLow + dNot1Down + ckNot2 = s & dClockLow + dNot1Down + dNot2Up + ckXor = s & dClockLow + dNot1Down + dNot2Up + dXorDown1Up + ckAnd = s & dClockLow + dAndUp2 + ckLatch = s & dClockLow + ckClock = s DESCRIPTION OF THE TRANSITIONS s_1 -> s_2 via "clockUp1" s_3 -> s_5 via "xorUp1" s_4 -> s_6 via "xorUp1" s_6 -> s_8 via "not2Up1" s_8 -> s_9 via "latchUp1" s_3 -> s_4 via "not1Down1" s_5 -> s_6 via "not1Down1" s_11 -> s_12 via "andDown1" s_9 -> s_10 via "dDown1" s_2 -> s_3 via "andUp1" s_0 -> s_1 via "dUp1" s_10 -> s_11 via "xorDown1"