/*************************************************** * File automatically generated by IMITATOR 2.6.1 for model 'examples/Train/TrainAHV93.imi' * * The following pi0 was considered: a = 4 & b = 6 & c = 1 & d = 2 & e = 2 & f = 3 * * 78 states and 94 transitions * * Program terminated after 0.109000000001 second * File generated: Sun May 5, 2013 09:30:06 ***************************************************/ DESCRIPTION OF THE STATES STATE 0: train: train0, gate: gate0, controller: controller0 ==> & a >= d & a >= f STATE 1: train: train1, gate: gate0, controller: controller1 ==> & a >= d & a >= f & x >= 0 & x = z STATE 2: train: train2, gate: gate0, controller: controller1 ==> & a >= d & a >= f & x >= 0 & x > a & x = z STATE 3: train: train1, gate: gate1, controller: controller2 ==> & a >= d & a >= f & f + y > x & x >= y & y >= 0 & x > e + y & x = z STATE 4: train: train3, gate: gate0, controller: controller1 ==> & a >= f & a >= d & x >= 0 & x > a & x = z STATE 5: train: train2, gate: gate1, controller: controller2 ==> & a >= d & a >= f & f + y > x & x >= y & x > e + y & x > a & x = z STATE 6: train: train1, gate: gate2, controller: controller2 ==> & a >= d & a >= f & d > 0 & f + y > x & x >= y & y >= 0 & x > e + y & d > c & y > c & x = z STATE 7: train: train3, gate: gate1, controller: controller2 ==> & a >= d & a >= f & f + y > x & x >= y & x > e + y & x > a & x = z STATE 8: train: train2, gate: gate2, controller: controller2 ==> & a >= f & f + y > x & a >= d & x > e + y & d > c & y > c & d + x > a + y & x > a & x = z STATE 9: train: train2, gate: gate2, controller: controller2 ==> & a >= d & a >= f & d > 0 & f + y > x & x >= y & x > e + y & d > c & y > c & x > a & x = z STATE 10: train: train3, gate: gate2, controller: controller2 ==> & a >= f & f + y > x & a >= d & x > e + y & d > c & y > c & d + x > a + y & x > a & x = z STATE 11: train: train0, gate: gate1, controller: controller3 ==> & a >= d & a >= f & b + z > x & f + y > x & x >= y & z >= 0 & x > e + y & x > a + z STATE 12: train: train3, gate: gate2, controller: controller2 ==> & a >= d & a >= f & d > 0 & f + y > x & x >= y & x > e + y & d > c & y > c & x > a & x = z STATE 13: train: train0, gate: gate2, controller: controller3 ==> & a >= f & b + z > x & d + z > y & f + y > x & a >= d & z >= 0 & x > e + y & d > c & y > c & x > a + z STATE 14: train: train0, gate: gate2, controller: controller3 ==> & a >= f & b + z > x & f + y > x & a >= d & z >= 0 & x > e + y & d > c & y > c + z & d + x > a + y & x > a + z STATE 15: train: train0, gate: gate2, controller: controller3 ==> & a >= d & a >= f & b + z > x & d > 0 & f + y > x & x >= y & z >= 0 & x > e + y & d > c & y > c + z & x > a + z STATE 16: train: train0, gate: gate3, controller: controller0 ==> & a >= f & b + z > x & f + y > z & y >= 0 & z >= y & z > e + y & d > c & a >= d & x > c + e + z & d + f > a & x > a + z STATE 17: train: train0, gate: gate3, controller: controller0 ==> & b + z > x & d + f + z > x & f + y > z & y >= 0 & z >= y & z > e + y & d > c & a >= f & a >= d & x > a + z STATE 18: train: train0, gate: gate3, controller: controller0 ==> & a >= f & b + z > x & d > 0 & f + y > z & y >= 0 & z >= y & z > e + y & d > c & a >= d & x > c + e + z & x > a + z STATE 19: train: train1, gate: gate3, controller: controller1 ==> & a >= f & a >= d & y >= x & x >= 0 & f > e & d > c & b > a & d + f > a & x = z STATE 20: train: train0, gate: gate0, controller: controller0 ==> & b + z > x & d + f + z > x & f + y > z & y >= 0 & z >= y & z > e + y & d > c & a >= f & y > c & a >= d & x > a + z STATE 21: train: train1, gate: gate3, controller: controller1 ==> & a >= f & b > c + e & a >= d & y >= x & x >= 0 & f > e & d > c & b > a & d + f > a & x = z STATE 22: train: train0, gate: gate0, controller: controller0 ==> & a >= f & b + z > x & f + y > z & y >= 0 & z >= y & z > e + y & d > c & a >= d & y > c & x > c + e + z & d + f > a & x > a + z STATE 23: train: train1, gate: gate3, controller: controller1 ==> & a >= f & a >= d & b > c + e & d > 0 & f > 0 & y >= x & x >= 0 & f > e & d > c & b > a & x = z STATE 24: train: train0, gate: gate0, controller: controller0 ==> & a >= f & b + z > x & d > 0 & f + y > z & y >= 0 & z >= y & z > e + y & d > c & a >= d & y > c & x > c + e + z & x > a + z STATE 25: train: train1, gate: gate0, controller: controller1 ==> & a >= f & b > c + e & a >= d & y >= x & x >= 0 & f > e & d > c & y > c + x & b > a & d + f > a & x = z STATE 26: train: train2, gate: gate3, controller: controller1 ==> & a >= f & b > c + e & a >= d & y >= x & f > e & d > c & b > a & d + f > a & x > a & x = z STATE 27: train: train1, gate: gate0, controller: controller1 ==> & a >= f & b > c + e & d + x > y & a >= d & x >= 0 & y >= x & f > e & d > c & y > c & b > a & d + f > a & x = z STATE 28: train: train2, gate: gate3, controller: controller1 ==> & a >= f & a >= d & y >= x & f > e & d > c & b > a & d + f > a & x > a & x = z STATE 29: train: train1, gate: gate0, controller: controller1 ==> & a >= f & d + x > y & a >= d & x >= 0 & y >= x & f > e & d > c & y > c & b > a & d + f > a & x = z STATE 30: train: train1, gate: gate0, controller: controller1 ==> & a >= f & a >= d & y >= x & x >= 0 & f > e & d > c & y > c + x & b > a & d + f > a & x = z STATE 31: train: train2, gate: gate3, controller: controller1 ==> & a >= f & a >= d & b > c + e & d > 0 & f > 0 & y >= x & f > e & d > c & b > a & x > a & x = z STATE 32: train: train1, gate: gate0, controller: controller1 ==> & a >= f & a >= d & b > c + e & d + x > y & f > 0 & x >= 0 & y >= x & f > e & d > c & y > c & b > a & x = z STATE 33: train: train1, gate: gate0, controller: controller1 ==> & a >= f & a >= d & b > c + e & d > 0 & f > 0 & y >= x & x >= 0 & f > e & d > c & y > c + x & b > a & x = z STATE 34: train: train2, gate: gate0, controller: controller1 ==> & a >= f & b > c + e & d + x > y & f > 0 & y >= x & f > e & d > c & a >= d & b > a & x > a & x = z STATE 35: train: train1, gate: gate1, controller: controller2 ==> & a >= f & a >= d & b > c + e & d > 0 & f + y > x & x >= y & y >= 0 & x > e + y & d > c & b > a & x = z STATE 36: train: train3, gate: gate3, controller: controller1 ==> & a >= f & a >= d & b > c + e & d > 0 & f > 0 & y >= x & f > e & d > c & b > a & x > a & x = z STATE 37: train: train2, gate: gate0, controller: controller1 ==> & a >= f & a >= d & d + x > y & y >= x & f > e & d > c & b > a & d + f > a & x > a & x = z STATE 38: train: train1, gate: gate1, controller: controller2 ==> & a >= f & a >= d & f + y > x & x >= y & y >= 0 & x > e + y & d > c & b > a & d + f > a & x = z STATE 39: train: train3, gate: gate3, controller: controller1 ==> & a >= f & a >= d & y >= x & f > e & d > c & b > a & d + f > a & x > a & x = z STATE 40: train: train2, gate: gate0, controller: controller1 ==> & a >= f & a >= d & b > c + e & y >= x & f > e & d > c & y > c + x & b > a & d + f > a & x > a & x = z STATE 41: train: train1, gate: gate1, controller: controller2 ==> & a >= f & a >= d & b > c + e & f + y > x & x >= y & y >= 0 & x > e + y & d > c & b > a & d + f > a & x = z STATE 42: train: train3, gate: gate3, controller: controller1 ==> & a >= f & a >= d & b > c + e & y >= x & f > e & d > c & b > a & d + f > a & x > a & x = z STATE 43: train: train2, gate: gate0, controller: controller1 ==> & a >= f & a >= d & b > c + e & d + x > y & y >= x & f > e & d > c & b > a & d + f > a & x > a & x = z STATE 44: train: train2, gate: gate0, controller: controller1 ==> & a >= f & a >= d & y >= x & f > e & d > c & y > c + x & b > a & d + f > a & x > a & x = z STATE 45: train: train2, gate: gate0, controller: controller1 ==> & a >= f & a >= d & b > c + e & d > 0 & f > 0 & y >= x & f > e & d > c & y > c + x & b > a & x > a & x = z STATE 46: train: train3, gate: gate0, controller: controller1 ==> & a >= f & a >= d & y >= x & f > e & d > c & y > c + x & b > a & d + f > a & x > a & x = z STATE 47: train: train3, gate: gate0, controller: controller1 ==> & a >= f & a >= d & b > c + e & d + x > y & f > 0 & y >= x & f > e & d > c & b > a & x > a & x = z STATE 48: train: train2, gate: gate1, controller: controller2 ==> & a >= f & a >= d & b > c + e & d > 0 & f + y > x & x >= y & x > e + y & d > c & b > a & x > a & x = z STATE 49: train: train1, gate: gate2, controller: controller2 ==> & a >= f & a >= d & b > c + e & d > 0 & f + y > x & x >= y & y >= 0 & x > e + y & d > c & y > c & b > a & x = z STATE 50: train: train3, gate: gate0, controller: controller1 ==> & a >= f & a >= d & d + x > y & y >= x & f > e & d > c & b > a & d + f > a & x > a & x = z STATE 51: train: train2, gate: gate1, controller: controller2 ==> & a >= f & a >= d & f + y > x & x >= y & x > e + y & d > c & b > a & d + f > a & x > a & x = z STATE 52: train: train1, gate: gate2, controller: controller2 ==> & a >= f & a >= d & f + y > x & x >= y & y >= 0 & x > e + y & d > c & y > c & b > a & d + f > a & x = z STATE 53: train: train3, gate: gate0, controller: controller1 ==> & a >= f & a >= d & b > c + e & y >= x & f > e & d > c & y > c + x & b > a & d + f > a & x > a & x = z STATE 54: train: train2, gate: gate1, controller: controller2 ==> & a >= f & a >= d & b > c + e & f + y > x & x >= y & x > e + y & d > c & b > a & d + f > a & x > a & x = z STATE 55: train: train1, gate: gate2, controller: controller2 ==> & a >= f & a >= d & b > c + e & f + y > x & x >= y & y >= 0 & x > e + y & d > c & y > c & b > a & d + f > a & x = z STATE 56: train: train3, gate: gate0, controller: controller1 ==> & a >= f & a >= d & b > c + e & d + x > y & y >= x & f > e & d > c & b > a & d + f > a & x > a & x = z STATE 57: train: train3, gate: gate0, controller: controller1 ==> & a >= f & a >= d & b > c + e & d > 0 & f > 0 & y >= x & f > e & d > c & y > c + x & b > a & x > a & x = z STATE 58: train: train3, gate: gate1, controller: controller2 ==> & a >= f & a >= d & b > c + e & d > 0 & f + y > x & x >= y & x > e + y & d > c & b > a & x > a & x = z STATE 59: train: train2, gate: gate2, controller: controller2 ==> & a >= f & a >= d & b > c + e & f + y > x & x > e + y & d > c & y > c & b > a & d + x > a + y & x > a & x = z STATE 60: train: train2, gate: gate2, controller: controller2 ==> & a >= f & a >= d & b > c + e & d > 0 & f + y > x & x >= y & x > e + y & d > c & y > c & b > a & x > a & x = z STATE 61: train: train3, gate: gate1, controller: controller2 ==> & a >= f & a >= d & f + y > x & x >= y & x > e + y & d > c & b > a & d + f > a & x > a & x = z STATE 62: train: train2, gate: gate2, controller: controller2 ==> & a >= f & a >= d & f + y > x & x > e + y & d > c & y > c & b > a & d + x > a + y & x > a & x = z STATE 63: train: train2, gate: gate2, controller: controller2 ==> & a >= f & a >= d & f + y > x & x >= y & x > e + y & d > c & y > c & b > a & d + f > a & x > a & x = z STATE 64: train: train3, gate: gate1, controller: controller2 ==> & a >= f & a >= d & b > c + e & f + y > x & x >= y & x > e + y & d > c & b > a & d + f > a & x > a & x = z STATE 65: train: train2, gate: gate2, controller: controller2 ==> & a >= f & a >= d & b > c + e & f + y > x & x >= y & x > e + y & d > c & y > c & b > a & d + f > a & x > a & x = z STATE 66: train: train3, gate: gate2, controller: controller2 ==> & a >= f & a >= d & b > c + e & f + y > x & x >= y & x > e + y & d > c & y > c & b > a & d + f > a & x > a & x = z STATE 67: train: train3, gate: gate2, controller: controller2 ==> & a >= f & a >= d & f + y > x & x >= y & x > e + y & d > c & y > c & b > a & d + f > a & x > a & x = z STATE 68: train: train3, gate: gate2, controller: controller2 ==> & a >= f & a >= d & b > c + e & d > 0 & f + y > x & x >= y & x > e + y & d > c & y > c & b > a & x > a & x = z STATE 69: train: train0, gate: gate1, controller: controller3 ==> & a >= f & a >= d & b + z > x & b > c + e & d > 0 & f + y > x & x >= y & z >= 0 & x > e + y & d > c & x > a + z STATE 70: train: train3, gate: gate2, controller: controller2 ==> & a >= f & a >= d & b > c + e & f + y > x & x > e + y & d > c & y > c & b > a & d + x > a + y & x > a & x = z STATE 71: train: train0, gate: gate1, controller: controller3 ==> & a >= f & a >= d & b + z > x & f + y > x & x >= y & z >= 0 & x > e + y & d > c & d + f > a & x > a + z STATE 72: train: train3, gate: gate2, controller: controller2 ==> & a >= f & a >= d & f + y > x & x > e + y & d > c & y > c & b > a & d + x > a + y & x > a & x = z STATE 73: train: train0, gate: gate1, controller: controller3 ==> & a >= f & a >= d & b + z > x & b > c + e & f + y > x & x >= y & z >= 0 & x > e + y & d > c & d + f > a & x > a + z STATE 74: train: train0, gate: gate2, controller: controller3 ==> & a >= f & a >= d & b + z > x & f + y > x & x >= y & z >= 0 & x > e + y & d > c & y > c + z & d + f > a & x > a + z STATE 75: train: train0, gate: gate2, controller: controller3 ==> & a >= f & a >= d & b + z > x & b > c + e & d + z > y & f + y > x & z >= 0 & x > e + y & d > c & y > c & x > a + z STATE 76: train: train0, gate: gate3, controller: controller0 ==> & a >= f & a >= d & b + z > x & b > c + e & d + f + z > x & f + y > z & y >= 0 & z >= y & z > e + y & d > c & x > a + z STATE 77: train: train0, gate: gate0, controller: controller0 ==> & a >= f & a >= d & b + z > x & b > c + e & d + f + z > x & f + y > z & y >= 0 & z >= y & z > e + y & d > c & y > c & x > a + z DESCRIPTION OF THE TRANSITIONS s_2 -> s_4 via "out" s_1 -> s_2 via "inn" s_0 -> s_1 via "approach" s_7 -> s_10 via "down" s_3 -> s_5 via "inn" s_5 -> s_7 via "out" s_7 -> s_11 via "exit" s_11 -> s_13 via "down" s_6 -> s_9 via "inn" s_13 -> s_17 via "raise" s_8 -> s_10 via "out" s_14 -> s_16 via "raise" s_10 -> s_14 via "exit" s_9 -> s_12 via "out" s_15 -> s_18 via "raise" s_12 -> s_15 via "exit" s_16 -> s_22 via "up" s_17 -> s_20 via "up" s_18 -> s_24 via "up" s_19 -> s_29 via "up" s_21 -> s_27 via "up" s_16 -> s_21 via "approach" s_17 -> s_19 via "approach" s_23 -> s_32 via "up" s_19 -> s_28 via "inn" s_18 -> s_23 via "approach" s_20 -> s_30 via "approach" s_21 -> s_26 via "inn" s_25 -> s_41 via "lower" s_23 -> s_31 via "inn" s_22 -> s_25 via "approach" s_27 -> s_41 via "lower" s_26 -> s_42 via "out" s_25 -> s_40 via "inn" s_24 -> s_33 via "approach" s_29 -> s_38 via "lower" s_30 -> s_38 via "lower" s_27 -> s_43 via "inn" s_28 -> s_39 via "out" s_29 -> s_37 via "inn" s_32 -> s_35 via "lower" s_35 -> s_49 via "down" s_33 -> s_35 via "lower" s_30 -> s_44 via "inn" s_31 -> s_36 via "out" s_32 -> s_34 via "inn" s_38 -> s_52 via "down" s_34 -> s_47 via "out" s_33 -> s_45 via "inn" s_35 -> s_48 via "inn" s_41 -> s_55 via "down" s_37 -> s_50 via "out" s_38 -> s_51 via "inn" s_40 -> s_53 via "out" s_41 -> s_54 via "inn" s_43 -> s_56 via "out" s_48 -> s_59 via "down" s_44 -> s_46 via "out" s_45 -> s_57 via "out" s_51 -> s_62 via "down" s_48 -> s_58 via "out" s_54 -> s_59 via "down" s_49 -> s_60 via "inn" s_51 -> s_61 via "out" s_52 -> s_63 via "inn" s_58 -> s_70 via "down" s_54 -> s_64 via "out" s_55 -> s_65 via "inn" s_61 -> s_72 via "down" s_58 -> s_69 via "exit" s_59 -> s_70 via "out" s_64 -> s_70 via "down" s_61 -> s_71 via "exit" s_60 -> s_68 via "out" s_62 -> s_72 via "out" s_64 -> s_73 via "exit" s_63 -> s_67 via "out" s_69 -> s_75 via "down" s_66 -> s_74 via "exit" s_65 -> s_66 via "out" s_67 -> s_74 via "exit" s_71 -> s_13 via "down" s_68 -> s_15 via "exit" s_74 -> s_16 via "raise" s_73 -> s_75 via "down" s_70 -> s_14 via "exit" s_75 -> s_76 via "raise" s_72 -> s_14 via "exit" s_76 -> s_77 via "up" s_76 -> s_21 via "approach" s_77 -> s_25 via "approach" s_3 -> s_6 via "down" s_1 -> s_3 via "lower" s_5 -> s_8 via "down"