/*************************************************** * File automatically generated for file 'NAV01.hym' * Reachability analysis * 3 states and 3 transitions * Program terminated after 0.404 second ***************************************************/ /* DESCRIPTION OF THE STATES STATE 0: nav: Q_hub ==> 2*x0 = 5 & 2*y0 = 3 & vx0 = 0 & vy0 = 0 & 2*x = 5 & 2*y = 3 & vx = 0 & vy = 0 STATE 1: nav: Q_2_1 ==> y >= 1 & vx >= 0 & 2*y >= 3 + 2*vy & 0 >= 12*vx + vy & 3 >= 2*y & 20*vx + 240*vy + 549 >= 286*y & 10*vy + 23 >= 12*y & vy + 1 >= 0 & vy0 = 0 & 286*x + 240*vx + 20*vy = 715 & 2*y0 = 3 & vx0 = 0 & 2*x0 = 5 STATE 2: nav: Q_safe ==> vx >= 0 & 735 >= 286*x + 240*vx & 286*x + 240*vx >= 725 & 2*x >= 5 & 2*x0 = 5 & 2*y0 = 3 & vx0 = 0 & vy0 = 0 & y = 1 & 286*x + 240*vx + 20*vy = 715 */ digraph G { s0 -> s1; s1 -> s2 [label="south"]; s2 -> s2; s0[fillcolor=red, style=filled, shape=Mrecord, label="s0|{Q_hub}"]; s1[fillcolor=green, style=filled, shape=Mrecord, label="s1|{Q_2_1}"]; s2[fillcolor=blue, style=filled, shape=Mrecord, label="s2|{Q_safe}"]; }