{ "jani-version": 1, "name": "PTPM/blowup/blowup-200.imi", "type": "sha", "features": [ "derived-operators" ], "actions": [ { "name": "a" }, { "name": "b" }, { "name": "dollar" }, { "name": "start" } ], "variables": [ { "name": "x", "type": "clock", "initial_value": 0 }, { "name": "y", "type": "clock", "initial_value": 0 }, { "name": "xabs", "type": "clock", "initial_value": 0 }, { "name": "p1", "type": "real" }, { "name": "p2", "type": "real" }, { "name": "p3", "type": "real" }, { "name": "t", "type": "real" }, { "name": "tprime", "type": "real" } ], "properties": [], "automata": [ { "name": "pta", "locations": [ { "name": "pre_s0" }, { "name": "pre_s0_prime" }, { "name": "s0" }, { "name": "s1" }, { "name": "s2" }, { "name": "soon_end" }, { "name": "s3" } ], "initial_locations": [ "pre_s0" ], "edges": [ { "location": "pre_s0", "guard": { "op": "∧", "left": { "op": "=", "left": "xabs", "right": 0 }, "right": { "op": "=", "left": "t", "right": "xabs" } }, "destinations": [ { "location": "s0" } ] }, { "location": "pre_s0", "destinations": [ { "location": "pre_s0_prime", "assignments": [ { "ref": "x", "value": 0 }, { "ref": "y", "value": 0 } ] } ] }, { "location": "pre_s0", "destinations": [ { "location": "pre_s0_prime", "assignments": [ { "ref": "x", "value": 0 }, { "ref": "y", "value": 0 } ] } ] }, { "location": "pre_s0_prime", "destinations": [ { "location": "pre_s0_prime", "assignments": [ { "ref": "x", "value": 0 }, { "ref": "y", "value": 0 } ] } ] }, { "location": "pre_s0_prime", "destinations": [ { "location": "pre_s0_prime", "assignments": [ { "ref": "x", "value": 0 }, { "ref": "y", "value": 0 } ] } ] }, { "location": "pre_s0_prime", "guard": { "op": "∧", "left": { "op": "=", "left": "t", "right": "xabs" }, "right": { "op": "≥", "left": "x", "right": 0 } }, "destinations": [ { "location": "s0", "assignments": [ { "ref": "x", "value": 0 }, { "ref": "y", "value": 0 } ] } ] }, { "location": "s0", "destinations": [ { "location": "s1", "assignments": [ { "ref": "y", "value": 0 } ] } ] }, { "location": "s1", "guard": { "op": "≥", "left": "p1", "right": "x" }, "destinations": [ { "location": "s2" } ] }, { "location": "s2", "guard": { "op": "∧", "left": { "op": "=", "left": "p1", "right": "x" }, "right": { "op": "=", "left": "tprime", "right": "xabs" } }, "destinations": [ { "location": "soon_end", "assignments": [ { "ref": "x", "value": 0 } ] } ] }, { "location": "s2", "guard": { "op": "∧", "left": { "op": ">", "left": "y", "right": "p3" }, "right": { "op": "≥", "left": "p2", "right": "y" } }, "destinations": [ { "location": "s1", "assignments": [ { "ref": "y", "value": 0 } ] } ] }, { "location": "soon_end", "guard": { "op": "≥", "left": "x", "right": 0 }, "destinations": [ { "location": "s3" } ] } ] }, { "name": "word", "locations": [ { "name": "w0", "time-progress": { "exp": { "op": ">", "left": 1, "right": { "op": "*", "left": 20, "right": "xabs" } } } }, { "name": "w1", "time-progress": { "exp": { "op": ">", "left": 9, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w2", "time-progress": { "exp": { "op": ">", "left": 3, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w3", "time-progress": { "exp": { "op": ">", "left": 4, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w4", "time-progress": { "exp": { "op": ">", "left": 19, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w5", "time-progress": { "exp": { "op": ">", "left": 7, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w6", "time-progress": { "exp": { "op": ">", "left": 17, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w7", "time-progress": { "exp": { "op": ">", "left": 19, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w8", "time-progress": { "exp": { "op": ">", "left": 41, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w9", "time-progress": { "exp": { "op": ">", "left": 23, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w10", "time-progress": { "exp": { "op": ">", "left": 27, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w11", "time-progress": { "exp": { "op": ">", "left": 29, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w12", "time-progress": { "exp": { "op": ">", "left": 67, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w13", "time-progress": { "exp": { "op": ">", "left": 19, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w14", "time-progress": { "exp": { "op": ">", "left": 21, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w15", "time-progress": { "exp": { "op": ">", "left": 43, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w16", "time-progress": { "exp": { "op": ">", "left": 22, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w17", "time-progress": { "exp": { "op": ">", "left": 47, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w18", "time-progress": { "exp": { "op": ">", "left": 24, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w19", "time-progress": { "exp": { "op": ">", "left": 103, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w20", "time-progress": { "exp": { "op": ">", "left": 53, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w21", "time-progress": { "exp": { "op": ">", "left": 28, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w22", "time-progress": { "exp": { "op": ">", "left": 119, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w23", "time-progress": { "exp": { "op": ">", "left": 127, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w24", "time-progress": { "exp": { "op": ">", "left": 129, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w25", "time-progress": { "exp": { "op": ">", "left": 27, "right": { "op": "*", "left": 20, "right": "xabs" } } } }, { "name": "w26", "time-progress": { "exp": { "op": ">", "left": 7, "right": { "op": "*", "left": 5, "right": "xabs" } } } }, { "name": "w27", "time-progress": { "exp": { "op": ">", "left": 73, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w28", "time-progress": { "exp": { "op": ">", "left": 149, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w29", "time-progress": { "exp": { "op": ">", "left": 38, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w30", "time-progress": { "exp": { "op": ">", "left": 77, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w31", "time-progress": { "exp": { "op": ">", "left": 79, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w32", "time-progress": { "exp": { "op": ">", "left": 167, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w33", "time-progress": { "exp": { "op": ">", "left": 7, "right": { "op": "*", "left": 4, "right": "xabs" } } } }, { "name": "w34", "time-progress": { "exp": { "op": ">", "left": 9, "right": { "op": "*", "left": 5, "right": "xabs" } } } }, { "name": "w35", "time-progress": { "exp": { "op": ">", "left": 93, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w36", "time-progress": { "exp": { "op": ">", "left": 189, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w37", "time-progress": { "exp": { "op": ">", "left": 19, "right": { "op": "*", "left": 10, "right": "xabs" } } } }, { "name": "w38", "time-progress": { "exp": { "op": ">", "left": 199, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w39", "time-progress": { "exp": { "op": ">", "left": 207, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w40", "time-progress": { "exp": { "op": ">", "left": 21, "right": { "op": "*", "left": 10, "right": "xabs" } } } }, { "name": "w41", "time-progress": { "exp": { "op": ">", "left": 211, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w42", "time-progress": { "exp": { "op": ">", "left": 217, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w43", "time-progress": { "exp": { "op": ">", "left": 109, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w44", "time-progress": { "exp": { "op": ">", "left": 11, "right": { "op": "*", "left": 5, "right": "xabs" } } } }, { "name": "w45", "time-progress": { "exp": { "op": ">", "left": 221, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w46", "time-progress": { "exp": { "op": ">", "left": 56, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w47", "time-progress": { "exp": { "op": ">", "left": 9, "right": { "op": "*", "left": 4, "right": "xabs" } } } }, { "name": "w48", "time-progress": { "exp": { "op": ">", "left": 233, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w49", "time-progress": { "exp": { "op": ">", "left": 237, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w50", "time-progress": { "exp": { "op": ">", "left": 243, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w51", "time-progress": { "exp": { "op": ">", "left": 49, "right": { "op": "*", "left": 20, "right": "xabs" } } } }, { "name": "w52", "time-progress": { "exp": { "op": ">", "left": 127, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w53", "time-progress": { "exp": { "op": ">", "left": 257, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w54", "time-progress": { "exp": { "op": ">", "left": 53, "right": { "op": "*", "left": 20, "right": "xabs" } } } }, { "name": "w55", "time-progress": { "exp": { "op": ">", "left": 273, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w56", "time-progress": { "exp": { "op": ">", "left": 141, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w57", "time-progress": { "exp": { "op": ">", "left": 72, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w58", "time-progress": { "exp": { "op": ">", "left": 291, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w59", "time-progress": { "exp": { "op": ">", "left": 73, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w60", "time-progress": { "exp": { "op": ">", "left": 297, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w61", "time-progress": { "exp": { "op": ">", "left": 151, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w62", "time-progress": { "exp": { "op": ">", "left": 77, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w63", "time-progress": { "exp": { "op": ">", "left": 317, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w64", "time-progress": { "exp": { "op": ">", "left": 16, "right": { "op": "*", "left": 5, "right": "xabs" } } } }, { "name": "w65", "time-progress": { "exp": { "op": ">", "left": 329, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w66", "time-progress": { "exp": { "op": ">", "left": 333, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w67", "time-progress": { "exp": { "op": ">", "left": 171, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w68", "time-progress": { "exp": { "op": ">", "left": 351, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w69", "time-progress": { "exp": { "op": ">", "left": 179, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w70", "time-progress": { "exp": { "op": ">", "left": 367, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w71", "time-progress": { "exp": { "op": ">", "left": 187, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w72", "time-progress": { "exp": { "op": ">", "left": 377, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w73", "time-progress": { "exp": { "op": ">", "left": 383, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w74", "time-progress": { "exp": { "op": ">", "left": 98, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w75", "time-progress": { "exp": { "op": ">", "left": 79, "right": { "op": "*", "left": 20, "right": "xabs" } } } }, { "name": "w76", "time-progress": { "exp": { "op": ">", "left": 403, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w77", "time-progress": { "exp": { "op": ">", "left": 102, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w78", "time-progress": { "exp": { "op": ">", "left": 409, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w79", "time-progress": { "exp": { "op": ">", "left": 207, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w80", "time-progress": { "exp": { "op": ">", "left": 83, "right": { "op": "*", "left": 20, "right": "xabs" } } } }, { "name": "w81", "time-progress": { "exp": { "op": ">", "left": 21, "right": { "op": "*", "left": 5, "right": "xabs" } } } }, { "name": "w82", "time-progress": { "exp": { "op": ">", "left": 421, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w83", "time-progress": { "exp": { "op": ">", "left": 423, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w84", "time-progress": { "exp": { "op": ">", "left": 107, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w85", "time-progress": { "exp": { "op": ">", "left": 431, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w86", "time-progress": { "exp": { "op": ">", "left": 217, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w87", "time-progress": { "exp": { "op": ">", "left": 443, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w88", "time-progress": { "exp": { "op": ">", "left": 449, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w89", "time-progress": { "exp": { "op": ">", "left": 91, "right": { "op": "*", "left": 20, "right": "xabs" } } } }, { "name": "w90", "time-progress": { "exp": { "op": ">", "left": 457, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w91", "time-progress": { "exp": { "op": ">", "left": 93, "right": { "op": "*", "left": 20, "right": "xabs" } } } }, { "name": "w92", "time-progress": { "exp": { "op": ">", "left": 233, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w93", "time-progress": { "exp": { "op": ">", "left": 467, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w94", "time-progress": { "exp": { "op": ">", "left": 471, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w95", "time-progress": { "exp": { "op": ">", "left": 24, "right": { "op": "*", "left": 5, "right": "xabs" } } } }, { "name": "w96", "time-progress": { "exp": { "op": ">", "left": 97, "right": { "op": "*", "left": 20, "right": "xabs" } } } }, { "name": "w97", "time-progress": { "exp": { "op": ">", "left": 49, "right": { "op": "*", "left": 10, "right": "xabs" } } } }, { "name": "w98", "time-progress": { "exp": { "op": ">", "left": 499, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w99", "time-progress": { "exp": { "op": ">", "left": 251, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w100", "time-progress": { "exp": { "op": ">", "left": 126, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w101", "time-progress": { "exp": { "op": ">", "left": 509, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w102", "time-progress": { "exp": { "op": ">", "left": 103, "right": { "op": "*", "left": 20, "right": "xabs" } } } }, { "name": "w103", "time-progress": { "exp": { "op": ">", "left": 261, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w104", "time-progress": { "exp": { "op": ">", "left": 527, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w105", "time-progress": { "exp": { "op": ">", "left": 267, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w106", "time-progress": { "exp": { "op": ">", "left": 27, "right": { "op": "*", "left": 5, "right": "xabs" } } } }, { "name": "w107", "time-progress": { "exp": { "op": ">", "left": 549, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w108", "time-progress": { "exp": { "op": ">", "left": 138, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w109", "time-progress": { "exp": { "op": ">", "left": 553, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w110", "time-progress": { "exp": { "op": ">", "left": 557, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w111", "time-progress": { "exp": { "op": ">", "left": 561, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w112", "time-progress": { "exp": { "op": ">", "left": 57, "right": { "op": "*", "left": 10, "right": "xabs" } } } }, { "name": "w113", "time-progress": { "exp": { "op": ">", "left": 144, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w114", "time-progress": { "exp": { "op": ">", "left": 577, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w115", "time-progress": { "exp": { "op": ">", "left": 289, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w116", "time-progress": { "exp": { "op": ">", "left": 293, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w117", "time-progress": { "exp": { "op": ">", "left": 297, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w118", "time-progress": { "exp": { "op": ">", "left": 119, "right": { "op": "*", "left": 20, "right": "xabs" } } } }, { "name": "w119", "time-progress": { "exp": { "op": ">", "left": 149, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w120", "time-progress": { "exp": { "op": ">", "left": 6, "right": "xabs" } } }, { "name": "w121", "time-progress": { "exp": { "op": ">", "left": 301, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w122", "time-progress": { "exp": { "op": ">", "left": 303, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w123", "time-progress": { "exp": { "op": ">", "left": 613, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w124", "time-progress": { "exp": { "op": ">", "left": 123, "right": { "op": "*", "left": 20, "right": "xabs" } } } }, { "name": "w125", "time-progress": { "exp": { "op": ">", "left": 617, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w126", "time-progress": { "exp": { "op": ">", "left": 309, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w127", "time-progress": { "exp": { "op": ">", "left": 619, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w128", "time-progress": { "exp": { "op": ">", "left": 627, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w129", "time-progress": { "exp": { "op": ">", "left": 157, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w130", "time-progress": { "exp": { "op": ">", "left": 633, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w131", "time-progress": { "exp": { "op": ">", "left": 641, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w132", "time-progress": { "exp": { "op": ">", "left": 323, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w133", "time-progress": { "exp": { "op": ">", "left": 327, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w134", "time-progress": { "exp": { "op": ">", "left": 661, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w135", "time-progress": { "exp": { "op": ">", "left": 667, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w136", "time-progress": { "exp": { "op": ">", "left": 671, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w137", "time-progress": { "exp": { "op": ">", "left": 339, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w138", "time-progress": { "exp": { "op": ">", "left": 171, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w139", "time-progress": { "exp": { "op": ">", "left": 689, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w140", "time-progress": { "exp": { "op": ">", "left": 349, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w141", "time-progress": { "exp": { "op": ">", "left": 351, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w142", "time-progress": { "exp": { "op": ">", "left": 71, "right": { "op": "*", "left": 10, "right": "xabs" } } } }, { "name": "w143", "time-progress": { "exp": { "op": ">", "left": 719, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w144", "time-progress": { "exp": { "op": ">", "left": 182, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w145", "time-progress": { "exp": { "op": ">", "left": 367, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w146", "time-progress": { "exp": { "op": ">", "left": 741, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w147", "time-progress": { "exp": { "op": ">", "left": 149, "right": { "op": "*", "left": 20, "right": "xabs" } } } }, { "name": "w148", "time-progress": { "exp": { "op": ">", "left": 751, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w149", "time-progress": { "exp": { "op": ">", "left": 759, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w150", "time-progress": { "exp": { "op": ">", "left": 767, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w151", "time-progress": { "exp": { "op": ">", "left": 77, "right": { "op": "*", "left": 10, "right": "xabs" } } } }, { "name": "w152", "time-progress": { "exp": { "op": ">", "left": 771, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w153", "time-progress": { "exp": { "op": ">", "left": 777, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w154", "time-progress": { "exp": { "op": ">", "left": 779, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w155", "time-progress": { "exp": { "op": ">", "left": 157, "right": { "op": "*", "left": 20, "right": "xabs" } } } }, { "name": "w156", "time-progress": { "exp": { "op": ">", "left": 197, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w157", "time-progress": { "exp": { "op": ">", "left": 789, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w158", "time-progress": { "exp": { "op": ">", "left": 198, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w159", "time-progress": { "exp": { "op": ">", "left": 399, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w160", "time-progress": { "exp": { "op": ">", "left": 801, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w161", "time-progress": { "exp": { "op": ">", "left": 202, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w162", "time-progress": { "exp": { "op": ">", "left": 204, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w163", "time-progress": { "exp": { "op": ">", "left": 41, "right": { "op": "*", "left": 5, "right": "xabs" } } } }, { "name": "w164", "time-progress": { "exp": { "op": ">", "left": 411, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w165", "time-progress": { "exp": { "op": ">", "left": 831, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w166", "time-progress": { "exp": { "op": ">", "left": 837, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w167", "time-progress": { "exp": { "op": ">", "left": 841, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w168", "time-progress": { "exp": { "op": ">", "left": 421, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w169", "time-progress": { "exp": { "op": ">", "left": 17, "right": { "op": "*", "left": 2, "right": "xabs" } } } }, { "name": "w170", "time-progress": { "exp": { "op": ">", "left": 859, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w171", "time-progress": { "exp": { "op": ">", "left": 217, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w172", "time-progress": { "exp": { "op": ">", "left": 877, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w173", "time-progress": { "exp": { "op": ">", "left": 879, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w174", "time-progress": { "exp": { "op": ">", "left": 443, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w175", "time-progress": { "exp": { "op": ">", "left": 893, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w176", "time-progress": { "exp": { "op": ">", "left": 179, "right": { "op": "*", "left": 20, "right": "xabs" } } } }, { "name": "w177", "time-progress": { "exp": { "op": ">", "left": 226, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w178", "time-progress": { "exp": { "op": ">", "left": 907, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w179", "time-progress": { "exp": { "op": ">", "left": 909, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w180", "time-progress": { "exp": { "op": ">", "left": 913, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w181", "time-progress": { "exp": { "op": ">", "left": 46, "right": { "op": "*", "left": 5, "right": "xabs" } } } }, { "name": "w182", "time-progress": { "exp": { "op": ">", "left": 37, "right": { "op": "*", "left": 4, "right": "xabs" } } } }, { "name": "w183", "time-progress": { "exp": { "op": ">", "left": 232, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w184", "time-progress": { "exp": { "op": ">", "left": 187, "right": { "op": "*", "left": 20, "right": "xabs" } } } }, { "name": "w185", "time-progress": { "exp": { "op": ">", "left": 941, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w186", "time-progress": { "exp": { "op": ">", "left": 471, "right": { "op": "*", "left": 50, "right": "xabs" } } } }, { "name": "w187", "time-progress": { "exp": { "op": ">", "left": 949, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w188", "time-progress": { "exp": { "op": ">", "left": 953, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w189", "time-progress": { "exp": { "op": ">", "left": 48, "right": { "op": "*", "left": 5, "right": "xabs" } } } }, { "name": "w190", "time-progress": { "exp": { "op": ">", "left": 241, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w191", "time-progress": { "exp": { "op": ">", "left": 242, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w192", "time-progress": { "exp": { "op": ">", "left": 969, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w193", "time-progress": { "exp": { "op": ">", "left": 973, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w194", "time-progress": { "exp": { "op": ">", "left": 49, "right": { "op": "*", "left": 5, "right": "xabs" } } } }, { "name": "w195", "time-progress": { "exp": { "op": ">", "left": 247, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w196", "time-progress": { "exp": { "op": ">", "left": 989, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w197", "time-progress": { "exp": { "op": ">", "left": 248, "right": { "op": "*", "left": 25, "right": "xabs" } } } }, { "name": "w198", "time-progress": { "exp": { "op": ">", "left": 999, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w199", "time-progress": { "exp": { "op": ">", "left": 1007, "right": { "op": "*", "left": 100, "right": "xabs" } } } }, { "name": "w200" } ], "initial_locations": [ "w0" ], "edges": [ { "location": "w0", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "xabs" }, "right": 1 }, "destinations": [ { "location": "w1" } ] }, { "location": "w1", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 9 }, "destinations": [ { "location": "w2" } ] }, { "location": "w2", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 3 }, "destinations": [ { "location": "w3" } ] }, { "location": "w3", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 4 }, "destinations": [ { "location": "w4" } ] }, { "location": "w4", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 19 }, "destinations": [ { "location": "w5" } ] }, { "location": "w5", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 7 }, "destinations": [ { "location": "w6" } ] }, { "location": "w6", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 17 }, "destinations": [ { "location": "w7" } ] }, { "location": "w7", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 19 }, "destinations": [ { "location": "w8" } ] }, { "location": "w8", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 41 }, "destinations": [ { "location": "w9" } ] }, { "location": "w9", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 23 }, "destinations": [ { "location": "w10" } ] }, { "location": "w10", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 27 }, "destinations": [ { "location": "w11" } ] }, { "location": "w11", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 29 }, "destinations": [ { "location": "w12" } ] }, { "location": "w12", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 67 }, "destinations": [ { "location": "w13" } ] }, { "location": "w13", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 19 }, "destinations": [ { "location": "w14" } ] }, { "location": "w14", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 21 }, "destinations": [ { "location": "w15" } ] }, { "location": "w15", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 43 }, "destinations": [ { "location": "w16" } ] }, { "location": "w16", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 22 }, "destinations": [ { "location": "w17" } ] }, { "location": "w17", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 47 }, "destinations": [ { "location": "w18" } ] }, { "location": "w18", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 24 }, "destinations": [ { "location": "w19" } ] }, { "location": "w19", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 103 }, "destinations": [ { "location": "w20" } ] }, { "location": "w20", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 53 }, "destinations": [ { "location": "w21" } ] }, { "location": "w21", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 28 }, "destinations": [ { "location": "w22" } ] }, { "location": "w22", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 119 }, "destinations": [ { "location": "w23" } ] }, { "location": "w23", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 127 }, "destinations": [ { "location": "w24" } ] }, { "location": "w24", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 129 }, "destinations": [ { "location": "w25" } ] }, { "location": "w25", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "xabs" }, "right": 27 }, "destinations": [ { "location": "w26" } ] }, { "location": "w26", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "xabs" }, "right": 7 }, "destinations": [ { "location": "w27" } ] }, { "location": "w27", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 73 }, "destinations": [ { "location": "w28" } ] }, { "location": "w28", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 149 }, "destinations": [ { "location": "w29" } ] }, { "location": "w29", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 38 }, "destinations": [ { "location": "w30" } ] }, { "location": "w30", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 77 }, "destinations": [ { "location": "w31" } ] }, { "location": "w31", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 79 }, "destinations": [ { "location": "w32" } ] }, { "location": "w32", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 167 }, "destinations": [ { "location": "w33" } ] }, { "location": "w33", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "xabs" }, "right": 7 }, "destinations": [ { "location": "w34" } ] }, { "location": "w34", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "xabs" }, "right": 9 }, "destinations": [ { "location": "w35" } ] }, { "location": "w35", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 93 }, "destinations": [ { "location": "w36" } ] }, { "location": "w36", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 189 }, "destinations": [ { "location": "w37" } ] }, { "location": "w37", "guard": { "op": "=", "left": { "op": "*", "left": 10, "right": "xabs" }, "right": 19 }, "destinations": [ { "location": "w38" } ] }, { "location": "w38", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 199 }, "destinations": [ { "location": "w39" } ] }, { "location": "w39", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 207 }, "destinations": [ { "location": "w40" } ] }, { "location": "w40", "guard": { "op": "=", "left": { "op": "*", "left": 10, "right": "xabs" }, "right": 21 }, "destinations": [ { "location": "w41" } ] }, { "location": "w41", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 211 }, "destinations": [ { "location": "w42" } ] }, { "location": "w42", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 217 }, "destinations": [ { "location": "w43" } ] }, { "location": "w43", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 109 }, "destinations": [ { "location": "w44" } ] }, { "location": "w44", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "xabs" }, "right": 11 }, "destinations": [ { "location": "w45" } ] }, { "location": "w45", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 221 }, "destinations": [ { "location": "w46" } ] }, { "location": "w46", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 56 }, "destinations": [ { "location": "w47" } ] }, { "location": "w47", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "xabs" }, "right": 9 }, "destinations": [ { "location": "w48" } ] }, { "location": "w48", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 233 }, "destinations": [ { "location": "w49" } ] }, { "location": "w49", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 237 }, "destinations": [ { "location": "w50" } ] }, { "location": "w50", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 243 }, "destinations": [ { "location": "w51" } ] }, { "location": "w51", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "xabs" }, "right": 49 }, "destinations": [ { "location": "w52" } ] }, { "location": "w52", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 127 }, "destinations": [ { "location": "w53" } ] }, { "location": "w53", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 257 }, "destinations": [ { "location": "w54" } ] }, { "location": "w54", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "xabs" }, "right": 53 }, "destinations": [ { "location": "w55" } ] }, { "location": "w55", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 273 }, "destinations": [ { "location": "w56" } ] }, { "location": "w56", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 141 }, "destinations": [ { "location": "w57" } ] }, { "location": "w57", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 72 }, "destinations": [ { "location": "w58" } ] }, { "location": "w58", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 291 }, "destinations": [ { "location": "w59" } ] }, { "location": "w59", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 73 }, "destinations": [ { "location": "w60" } ] }, { "location": "w60", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 297 }, "destinations": [ { "location": "w61" } ] }, { "location": "w61", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 151 }, "destinations": [ { "location": "w62" } ] }, { "location": "w62", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 77 }, "destinations": [ { "location": "w63" } ] }, { "location": "w63", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 317 }, "destinations": [ { "location": "w64" } ] }, { "location": "w64", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "xabs" }, "right": 16 }, "destinations": [ { "location": "w65" } ] }, { "location": "w65", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 329 }, "destinations": [ { "location": "w66" } ] }, { "location": "w66", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 333 }, "destinations": [ { "location": "w67" } ] }, { "location": "w67", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 171 }, "destinations": [ { "location": "w68" } ] }, { "location": "w68", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 351 }, "destinations": [ { "location": "w69" } ] }, { "location": "w69", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 179 }, "destinations": [ { "location": "w70" } ] }, { "location": "w70", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 367 }, "destinations": [ { "location": "w71" } ] }, { "location": "w71", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 187 }, "destinations": [ { "location": "w72" } ] }, { "location": "w72", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 377 }, "destinations": [ { "location": "w73" } ] }, { "location": "w73", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 383 }, "destinations": [ { "location": "w74" } ] }, { "location": "w74", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 98 }, "destinations": [ { "location": "w75" } ] }, { "location": "w75", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "xabs" }, "right": 79 }, "destinations": [ { "location": "w76" } ] }, { "location": "w76", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 403 }, "destinations": [ { "location": "w77" } ] }, { "location": "w77", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 102 }, "destinations": [ { "location": "w78" } ] }, { "location": "w78", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 409 }, "destinations": [ { "location": "w79" } ] }, { "location": "w79", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 207 }, "destinations": [ { "location": "w80" } ] }, { "location": "w80", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "xabs" }, "right": 83 }, "destinations": [ { "location": "w81" } ] }, { "location": "w81", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "xabs" }, "right": 21 }, "destinations": [ { "location": "w82" } ] }, { "location": "w82", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 421 }, "destinations": [ { "location": "w83" } ] }, { "location": "w83", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 423 }, "destinations": [ { "location": "w84" } ] }, { "location": "w84", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 107 }, "destinations": [ { "location": "w85" } ] }, { "location": "w85", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 431 }, "destinations": [ { "location": "w86" } ] }, { "location": "w86", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 217 }, "destinations": [ { "location": "w87" } ] }, { "location": "w87", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 443 }, "destinations": [ { "location": "w88" } ] }, { "location": "w88", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 449 }, "destinations": [ { "location": "w89" } ] }, { "location": "w89", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "xabs" }, "right": 91 }, "destinations": [ { "location": "w90" } ] }, { "location": "w90", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 457 }, "destinations": [ { "location": "w91" } ] }, { "location": "w91", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "xabs" }, "right": 93 }, "destinations": [ { "location": "w92" } ] }, { "location": "w92", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 233 }, "destinations": [ { "location": "w93" } ] }, { "location": "w93", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 467 }, "destinations": [ { "location": "w94" } ] }, { "location": "w94", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 471 }, "destinations": [ { "location": "w95" } ] }, { "location": "w95", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "xabs" }, "right": 24 }, "destinations": [ { "location": "w96" } ] }, { "location": "w96", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "xabs" }, "right": 97 }, "destinations": [ { "location": "w97" } ] }, { "location": "w97", "guard": { "op": "=", "left": { "op": "*", "left": 10, "right": "xabs" }, "right": 49 }, "destinations": [ { "location": "w98" } ] }, { "location": "w98", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 499 }, "destinations": [ { "location": "w99" } ] }, { "location": "w99", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 251 }, "destinations": [ { "location": "w100" } ] }, { "location": "w100", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 126 }, "destinations": [ { "location": "w101" } ] }, { "location": "w101", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 509 }, "destinations": [ { "location": "w102" } ] }, { "location": "w102", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "xabs" }, "right": 103 }, "destinations": [ { "location": "w103" } ] }, { "location": "w103", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 261 }, "destinations": [ { "location": "w104" } ] }, { "location": "w104", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 527 }, "destinations": [ { "location": "w105" } ] }, { "location": "w105", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 267 }, "destinations": [ { "location": "w106" } ] }, { "location": "w106", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "xabs" }, "right": 27 }, "destinations": [ { "location": "w107" } ] }, { "location": "w107", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 549 }, "destinations": [ { "location": "w108" } ] }, { "location": "w108", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 138 }, "destinations": [ { "location": "w109" } ] }, { "location": "w109", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 553 }, "destinations": [ { "location": "w110" } ] }, { "location": "w110", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 557 }, "destinations": [ { "location": "w111" } ] }, { "location": "w111", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 561 }, "destinations": [ { "location": "w112" } ] }, { "location": "w112", "guard": { "op": "=", "left": { "op": "*", "left": 10, "right": "xabs" }, "right": 57 }, "destinations": [ { "location": "w113" } ] }, { "location": "w113", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 144 }, "destinations": [ { "location": "w114" } ] }, { "location": "w114", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 577 }, "destinations": [ { "location": "w115" } ] }, { "location": "w115", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 289 }, "destinations": [ { "location": "w116" } ] }, { "location": "w116", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 293 }, "destinations": [ { "location": "w117" } ] }, { "location": "w117", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 297 }, "destinations": [ { "location": "w118" } ] }, { "location": "w118", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "xabs" }, "right": 119 }, "destinations": [ { "location": "w119" } ] }, { "location": "w119", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 149 }, "destinations": [ { "location": "w120" } ] }, { "location": "w120", "guard": { "op": "=", "left": "xabs", "right": 6 }, "destinations": [ { "location": "w121" } ] }, { "location": "w121", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 301 }, "destinations": [ { "location": "w122" } ] }, { "location": "w122", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 303 }, "destinations": [ { "location": "w123" } ] }, { "location": "w123", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 613 }, "destinations": [ { "location": "w124" } ] }, { "location": "w124", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "xabs" }, "right": 123 }, "destinations": [ { "location": "w125" } ] }, { "location": "w125", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 617 }, "destinations": [ { "location": "w126" } ] }, { "location": "w126", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 309 }, "destinations": [ { "location": "w127" } ] }, { "location": "w127", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 619 }, "destinations": [ { "location": "w128" } ] }, { "location": "w128", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 627 }, "destinations": [ { "location": "w129" } ] }, { "location": "w129", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 157 }, "destinations": [ { "location": "w130" } ] }, { "location": "w130", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 633 }, "destinations": [ { "location": "w131" } ] }, { "location": "w131", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 641 }, "destinations": [ { "location": "w132" } ] }, { "location": "w132", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 323 }, "destinations": [ { "location": "w133" } ] }, { "location": "w133", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 327 }, "destinations": [ { "location": "w134" } ] }, { "location": "w134", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 661 }, "destinations": [ { "location": "w135" } ] }, { "location": "w135", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 667 }, "destinations": [ { "location": "w136" } ] }, { "location": "w136", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 671 }, "destinations": [ { "location": "w137" } ] }, { "location": "w137", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 339 }, "destinations": [ { "location": "w138" } ] }, { "location": "w138", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 171 }, "destinations": [ { "location": "w139" } ] }, { "location": "w139", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 689 }, "destinations": [ { "location": "w140" } ] }, { "location": "w140", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 349 }, "destinations": [ { "location": "w141" } ] }, { "location": "w141", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 351 }, "destinations": [ { "location": "w142" } ] }, { "location": "w142", "guard": { "op": "=", "left": { "op": "*", "left": 10, "right": "xabs" }, "right": 71 }, "destinations": [ { "location": "w143" } ] }, { "location": "w143", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 719 }, "destinations": [ { "location": "w144" } ] }, { "location": "w144", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 182 }, "destinations": [ { "location": "w145" } ] }, { "location": "w145", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 367 }, "destinations": [ { "location": "w146" } ] }, { "location": "w146", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 741 }, "destinations": [ { "location": "w147" } ] }, { "location": "w147", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "xabs" }, "right": 149 }, "destinations": [ { "location": "w148" } ] }, { "location": "w148", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 751 }, "destinations": [ { "location": "w149" } ] }, { "location": "w149", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 759 }, "destinations": [ { "location": "w150" } ] }, { "location": "w150", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 767 }, "destinations": [ { "location": "w151" } ] }, { "location": "w151", "guard": { "op": "=", "left": { "op": "*", "left": 10, "right": "xabs" }, "right": 77 }, "destinations": [ { "location": "w152" } ] }, { "location": "w152", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 771 }, "destinations": [ { "location": "w153" } ] }, { "location": "w153", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 777 }, "destinations": [ { "location": "w154" } ] }, { "location": "w154", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 779 }, "destinations": [ { "location": "w155" } ] }, { "location": "w155", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "xabs" }, "right": 157 }, "destinations": [ { "location": "w156" } ] }, { "location": "w156", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 197 }, "destinations": [ { "location": "w157" } ] }, { "location": "w157", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 789 }, "destinations": [ { "location": "w158" } ] }, { "location": "w158", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 198 }, "destinations": [ { "location": "w159" } ] }, { "location": "w159", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 399 }, "destinations": [ { "location": "w160" } ] }, { "location": "w160", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 801 }, "destinations": [ { "location": "w161" } ] }, { "location": "w161", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 202 }, "destinations": [ { "location": "w162" } ] }, { "location": "w162", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 204 }, "destinations": [ { "location": "w163" } ] }, { "location": "w163", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "xabs" }, "right": 41 }, "destinations": [ { "location": "w164" } ] }, { "location": "w164", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 411 }, "destinations": [ { "location": "w165" } ] }, { "location": "w165", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 831 }, "destinations": [ { "location": "w166" } ] }, { "location": "w166", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 837 }, "destinations": [ { "location": "w167" } ] }, { "location": "w167", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 841 }, "destinations": [ { "location": "w168" } ] }, { "location": "w168", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 421 }, "destinations": [ { "location": "w169" } ] }, { "location": "w169", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "xabs" }, "right": 17 }, "destinations": [ { "location": "w170" } ] }, { "location": "w170", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 859 }, "destinations": [ { "location": "w171" } ] }, { "location": "w171", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 217 }, "destinations": [ { "location": "w172" } ] }, { "location": "w172", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 877 }, "destinations": [ { "location": "w173" } ] }, { "location": "w173", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 879 }, "destinations": [ { "location": "w174" } ] }, { "location": "w174", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 443 }, "destinations": [ { "location": "w175" } ] }, { "location": "w175", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 893 }, "destinations": [ { "location": "w176" } ] }, { "location": "w176", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "xabs" }, "right": 179 }, "destinations": [ { "location": "w177" } ] }, { "location": "w177", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 226 }, "destinations": [ { "location": "w178" } ] }, { "location": "w178", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 907 }, "destinations": [ { "location": "w179" } ] }, { "location": "w179", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 909 }, "destinations": [ { "location": "w180" } ] }, { "location": "w180", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 913 }, "destinations": [ { "location": "w181" } ] }, { "location": "w181", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "xabs" }, "right": 46 }, "destinations": [ { "location": "w182" } ] }, { "location": "w182", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "xabs" }, "right": 37 }, "destinations": [ { "location": "w183" } ] }, { "location": "w183", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 232 }, "destinations": [ { "location": "w184" } ] }, { "location": "w184", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "xabs" }, "right": 187 }, "destinations": [ { "location": "w185" } ] }, { "location": "w185", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 941 }, "destinations": [ { "location": "w186" } ] }, { "location": "w186", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "xabs" }, "right": 471 }, "destinations": [ { "location": "w187" } ] }, { "location": "w187", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 949 }, "destinations": [ { "location": "w188" } ] }, { "location": "w188", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 953 }, "destinations": [ { "location": "w189" } ] }, { "location": "w189", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "xabs" }, "right": 48 }, "destinations": [ { "location": "w190" } ] }, { "location": "w190", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 241 }, "destinations": [ { "location": "w191" } ] }, { "location": "w191", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 242 }, "destinations": [ { "location": "w192" } ] }, { "location": "w192", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 969 }, "destinations": [ { "location": "w193" } ] }, { "location": "w193", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 973 }, "destinations": [ { "location": "w194" } ] }, { "location": "w194", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "xabs" }, "right": 49 }, "destinations": [ { "location": "w195" } ] }, { "location": "w195", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 247 }, "destinations": [ { "location": "w196" } ] }, { "location": "w196", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 989 }, "destinations": [ { "location": "w197" } ] }, { "location": "w197", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "xabs" }, "right": 248 }, "destinations": [ { "location": "w198" } ] }, { "location": "w198", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 999 }, "destinations": [ { "location": "w199" } ] }, { "location": "w199", "guard": { "op": "=", "left": { "op": "*", "left": 100, "right": "xabs" }, "right": 1007 }, "destinations": [ { "location": "w200" } ] } ] } ], "system": { "elements": [ { "automaton": "pta" }, { "automaton": "word" } ], "syncs": [ { "synchronise": [ "a", "a" ], "result": "a" }, { "synchronise": [ "b", "b" ], "result": "b" }, { "synchronise": [ "dollar", null ], "result": "dollar" }, { "synchronise": [ "start", null ], "result": "start" } ] } }