/*************************************************** * File automatically generated by IMITATOR 2.6.1 snapshot for model 'examples/Flipflop/flipflop.imi' * * The following pi0 was considered: tHI = 24 & tLO = 15 & tSetup = 10 & tHold = 17 & dG1_l = 7 & dG1_u = 7 & dG2_l = 5 & dG2_u = 6 & dG3_l = 8 & dG3_u = 10 & dG4_l = 3 & dG4_u = 7 * * 9 states and 9 transitions * * Program terminated after 0.057 second * File generated: Fri Apr 19, 2013 10:32:48 ***************************************************/ DESCRIPTION OF THE STATES STATE 0: input: Input0, g1: G10011, g2: G2101, g3: G30011, g4: G410, observer: locobs_0, qLevel = 0 ==> & tSetup > dG1_u & tHold > dG3_u & dG1_l > 0 & tHI >= tHold & tLO >= tSetup + s & tHI > dG3_u + dG4_u & dG2_l >= 0 & dG3_l >= 0 & dG4_l >= 0 & s >= 0 & ckG1 >= s & ckG2 >= s & ckG3 >= s & ckG4 >= s & dG4_u >= dG4_l & dG3_u >= dG3_l & dG2_u >= dG2_l & dG1_u >= dG1_l STATE 1: input: Input1, g1: G11011, g2: G2101, g3: G30011, g4: G410, observer: locobs_0, qLevel = 0 ==> & tHold > dG3_u & dG1_l > 0 & tHI >= tHold & tSetup > dG1_u & tLO + dG1_u >= tSetup + s & tLO >= tSetup & tHI > dG3_u + dG4_u & dG2_l >= 0 & dG3_l >= 0 & dG4_l >= 0 & ckG2 >= s & ckG3 >= s & ckG4 >= s & dG4_u >= dG4_l & dG3_u >= dG3_l & dG2_u >= dG2_l & dG1_u >= dG1_l & tSetup + s >= tLO & tLO + ckG1 = tSetup + s STATE 2: input: Input1, g1: G11010, g2: G2001, g3: G30011, g4: G410, observer: locobs_0, qLevel = 0 ==> & tHold > dG3_u & dG1_l > 0 & tHI >= tHold & tLO >= s & tLO >= tSetup & tSetup > dG1_u & tHI > dG3_u + dG4_u & dG2_l >= 0 & dG3_l >= 0 & dG4_l >= 0 & ckG2 >= s & ckG3 >= s & ckG4 >= s & dG4_u >= dG4_l & dG3_u >= dG3_l & dG2_u >= dG2_l & dG1_u >= dG1_l & tSetup + s >= tLO + dG1_l & tLO + ckG1 = tSetup + s STATE 3: input: Input2, g1: G11110, g2: G2011, g3: G30111, g4: G410, observer: locobs_0, qLevel = 0 ==> & dG1_l > 0 & tHI >= tHold & tHI > dG3_u + dG4_u & tLO + dG3_u >= s & tLO >= tSetup & tSetup > dG1_u & tHold > dG3_u & dG2_l >= 0 & dG3_l >= 0 & dG4_l >= 0 & ckG2 >= s & ckG4 >= s & dG4_u >= dG4_l & dG3_u >= dG3_l & dG2_u >= dG2_l & dG1_u >= dG1_l & s >= tLO & tLO + ckG1 = tSetup + s & tLO + ckG3 = s STATE 4: input: Input2, g1: G11110, g2: G2011, g3: G30110, g4: G400, observer: locobs_0, qLevel = 0 ==> & dG1_l > 0 & tHI >= tHold & tLO + tHold >= s & tLO + dG3_u + ckG4 >= s & tLO >= tSetup & tSetup > dG1_u & tHold > dG3_u & tHI > dG3_u + dG4_u & dG2_l >= 0 & dG3_l >= 0 & dG4_l >= 0 & dG4_u >= ckG4 & ckG4 >= 0 & ckG2 >= s & dG4_u >= dG4_l & dG2_u >= dG2_l & dG1_u >= dG1_l & s >= tLO + dG3_l + ckG4 & tLO + ckG1 = tSetup + s & tLO + ckG3 = s STATE 5: input: Input3, g1: G10110, g2: G2011, g3: G30110, g4: G400, observer: locobs_0, qLevel = 0 ==> & tHI > dG3_u + dG4_u & tLO + dG3_u + ckG4 >= s & tLO >= tSetup & tSetup > dG1_u & tHold > dG3_u & dG1_l > 0 & dG2_l >= 0 & dG3_l >= 0 & dG4_l >= 0 & dG4_u >= ckG4 & ckG2 >= s & dG4_u >= dG4_l & dG2_u >= dG2_l & dG1_u >= dG1_l & s >= tLO + dG3_l + ckG4 & s >= tLO + tHold & tLO + ckG1 = tSetup + s & tLO + ckG3 = s STATE 6: input: Input2, g1: G11110, g2: G2011, g3: G31110, g4: G401, observer: locobs_1, qLevel = 1 ==> & dG1_l > 0 & tHI >= tHold & tLO + tHold >= s & tLO + dG3_u + ckG4 >= s & tLO >= tSetup & tSetup > dG1_u & tHold > dG3_u & tHI > dG3_u + dG4_u & dG2_l >= 0 & dG3_l >= 0 & dG4_l >= 0 & ckG2 >= s & dG4_u >= dG4_l & ckG4 >= dG4_l & dG2_u >= dG2_l & dG1_u >= dG1_l & s >= tLO + dG3_l + ckG4 & tLO + ckG1 = tSetup + s & tLO + ckG3 = s STATE 7: input: Input3, g1: G10110, g2: G2011, g3: G31110, g4: G401, observer: locobs_1, qLevel = 1 ==> & tHI + tLO >= s & tHI > dG3_u + dG4_u & tLO + dG3_u + ckG4 >= s & tLO >= tSetup & tSetup > dG1_u & tHold > dG3_u & dG1_l > 0 & dG2_l >= 0 & dG3_l >= 0 & dG4_l >= 0 & ckG2 >= s & dG4_u >= dG4_l & ckG4 >= dG4_l & dG2_u >= dG2_l & dG1_u >= dG1_l & s >= tLO + dG3_l + ckG4 & s >= tLO + tHold & tLO + ckG1 = tSetup + s & tLO + ckG3 = s STATE 9: input: Input4, g1: G10010, g2: G2001, g3: G31010, g4: G401, observer: locobs_1, qLevel = 1 ==> & tHI > dG3_u + dG4_u & tHI >= dG3_l + ckG4 & tHI >= tHold & tLO >= tSetup & tSetup > dG1_u & tHold > dG3_u & dG1_l > 0 & dG2_l >= 0 & dG3_l >= 0 & dG4_l >= 0 & dG4_u >= dG4_l & dG2_u >= dG2_l & dG1_u >= dG1_l & dG3_u + ckG4 >= tHI & ckG2 >= tHI + tLO & s = 0 & ckG1 = 0 & tHI = ckG3 DESCRIPTION OF THE TRANSITIONS s_0 -> s_1 via "dUp" s_3 -> s_4 via "qG3Down" s_4 -> s_6 via "qUp" s_5 -> s_7 via "qUp" s_2 -> s_3 via "ckUp" s_1 -> s_2 via "qG1Down" s_4 -> s_5 via "dDown" s_6 -> s_7 via "dDown" s_7 -> s_9 via "ckDown"