<hyxml type="Model">
  <automaton name="default_automaton">
    <variable name="xp" scope="LOCAL_DATA" type="Real" />
    <variable name="yp" scope="LOCAL_DATA" type="Real" />
    <variable name="xd" scope="LOCAL_DATA" type="Real" />
    <variable name="yd" scope="LOCAL_DATA" type="Real" />
    <variable name="t" scope="LOCAL_DATA" type="Real" />
    <variable name="loc" scope="LOCAL_DATA" type="Real" />
    <mode id="0" initial="True" name="ProxA">
      <dai equation="xp_dot= xd" />
      <dai equation="yp_dot= yd" />
      <dai equation="xd_dot= -2.89995083970656*xd - 0.0576765518445905*xp + 0.00877200894463775*yd + 0.000200959896519766*yp - (1.43496e+18*xp + 6.050365344e+25)*pow(pow(yp, 2) + pow(xp + 42164000, 2), -1.5) + 807.153595726846" />
      <dai equation="yd_dot= -0.00875351105536225*xd - 0.000174031357370456*xp - 2.90300269286856*yd - 1.43496e+18*yp*pow(pow(yp, 2) + pow(xp + 42164000, 2), -1.5) - 0.0664932019993982*yp" />
      <dai equation="t_dot= 1" />
      <dai equation="loc_dot= 0" />
      <invariant equation="yp&lt;-100 || xp+yp&lt;-141.1 || xp&lt;-100 || yp-xp&gt;141.1 || yp&gt;100 || xp+yp&gt;141.1 || xp&gt;100 || yp-xp&lt;-141.1" />
    </mode>
    <mode id="1" initial="False" name="ProxB">
      <dai equation="xp_dot= xd" />
      <dai equation="yp_dot= yd" />
      <dai equation="xd_dot= -19.2299795908647*xd - 0.576076729033652*xp + 0.00876275931760007*yd + 0.000262486079431672*yp - (1.43496e+18*xp + 6.050365344e+25)*pow(pow(yp, 2) + pow(xp + 42164000, 2), -1.5) + 807.153595726846" />
      <dai equation="yd_dot= -0.00876276068239993*xd - 0.000262486080737868*xp - 19.2299765959399*yd - 1.43496e+18*yp*pow(pow(yp, 2) + pow(xp + 42164000, 2), -1.5) - 0.575980743701182*yp" />
      <dai equation="t_dot= 1" />
      <dai equation="loc_dot= 0" />
      <invariant equation="yp&gt;=-100" />
      <invariant equation="xp+yp&gt;=-141.1" />
      <invariant equation="xp&gt;=-100" />
      <invariant equation="yp-xp&lt;=141.1" />
      <invariant equation="yp&lt;=100" />
      <invariant equation="xp+yp&lt;=141.1" />
      <invariant equation="xp&lt;=100" />
      <invariant equation="yp-xp&gt;=-141.1" />
    </mode>
    <transition destination="1" id="0" source="0">
      <guard equation="yp&gt;=-100&amp;&amp;xp+yp&gt;=-141.1&amp;&amp;xp&gt;=-100&amp;&amp;yp-xp&lt;=141.1&amp;&amp;yp&lt;=100&amp;&amp;xp+yp&lt;=141.1&amp;&amp;xp&lt;=100&amp;&amp;yp-xp&gt;=-141.1" />
      <action equation="loc = 3" />
    </transition>
  </automaton>
  <composition automata="default_automaton" />
  <property initialSet="ProxA:t==0&amp;&amp;loc==2&amp;&amp;xp&lt;=-875&amp;&amp;xp&gt;=-925&amp;&amp;yp&lt;=-375&amp;&amp;yp&gt;=-425&amp;&amp;xd&gt;=0&amp;&amp;xd&lt;=0&amp;&amp;yd&gt;=0&amp;&amp;yd&lt;=0" name="LOS1" type="Safety" unsafeSet="loc==3&amp;&amp;xp&lt;-100">
    <parameters kvalue="2000.0" timehorizon="270.0" timestep="0.1" />
  </property>
  <property initialSet="ProxA:t==0&amp;&amp;loc==2&amp;&amp;xp&lt;=-875&amp;&amp;xp&gt;=-925&amp;&amp;yp&lt;=-375&amp;&amp;yp&gt;=-425&amp;&amp;xd&gt;=0&amp;&amp;xd&lt;=0&amp;&amp;yd&gt;=0&amp;&amp;yd&lt;=0" name="VEL1" type="Safety" unsafeSet="loc==3&amp;&amp;xd&gt;3">
    <parameters kvalue="2000.0" timehorizon="270.0" timestep="0.1" />
  </property>
  <property initialSet="ProxA:t==0&amp;&amp;loc==2&amp;&amp;xp&lt;=-875&amp;&amp;xp&gt;=-925&amp;&amp;yp&lt;=-375&amp;&amp;yp&gt;=-425&amp;&amp;xd&gt;=0&amp;&amp;xd&lt;=0&amp;&amp;yd&gt;=0&amp;&amp;yd&lt;=0" name="VEL2" type="Safety" unsafeSet="loc==3&amp;&amp;xd&lt;-3">
    <parameters kvalue="2000.0" timehorizon="270.0" timestep="0.1" />
  </property>
  <property initialSet="ProxA:t==0&amp;&amp;loc==2&amp;&amp;xp&lt;=-875&amp;&amp;xp&gt;=-925&amp;&amp;yp&lt;=-375&amp;&amp;yp&gt;=-425&amp;&amp;xd&gt;=0&amp;&amp;xd&lt;=0&amp;&amp;yd&gt;=0&amp;&amp;yd&lt;=0" name="VEL3" type="Safety" unsafeSet="loc==3&amp;&amp;yd&gt;3">
    <parameters kvalue="2000.0" timehorizon="270.0" timestep="0.1" />
  </property>
  <property initialSet="ProxA:t==0&amp;&amp;loc==2&amp;&amp;xp&lt;=-875&amp;&amp;xp&gt;=-925&amp;&amp;yp&lt;=-375&amp;&amp;yp&gt;=-425&amp;&amp;xd&gt;=0&amp;&amp;xd&lt;=0&amp;&amp;yd&gt;=0&amp;&amp;yd&lt;=0" name="VEL4" type="Safety" unsafeSet="loc==3&amp;&amp;yd&lt;-3">
    <parameters kvalue="2000.0" timehorizon="270.0" timestep="0.1" />
  </property>
  <property initialSet="ProxA:t==0&amp;&amp;loc==2&amp;&amp;xp&lt;=-875&amp;&amp;xp&gt;=-925&amp;&amp;yp&lt;=-375&amp;&amp;yp&gt;=-425&amp;&amp;xd&gt;=0&amp;&amp;xd&lt;=0&amp;&amp;yd&gt;=0&amp;&amp;yd&lt;=0" name="VEL5" type="Safety" unsafeSet="loc==3&amp;&amp;yd+xd&gt;4.243">
    <parameters kvalue="2000.0" timehorizon="270.0" timestep="0.1" />
  </property>
  <property initialSet="ProxA:t==0&amp;&amp;loc==2&amp;&amp;xp&lt;=-875&amp;&amp;xp&gt;=-925&amp;&amp;yp&lt;=-375&amp;&amp;yp&gt;=-425&amp;&amp;xd&gt;=0&amp;&amp;xd&lt;=0&amp;&amp;yd&gt;=0&amp;&amp;yd&lt;=0" name="VEL6" type="Safety" unsafeSet="loc==3&amp;&amp;yd-xd&lt;-4.243">
    <parameters kvalue="2000.0" timehorizon="270.0" timestep="0.1" />
  </property>
  <property initialSet="ProxA:t==0&amp;&amp;loc==2&amp;&amp;xp&lt;=-875&amp;&amp;xp&gt;=-925&amp;&amp;yp&lt;=-375&amp;&amp;yp&gt;=-425&amp;&amp;xd&gt;=0&amp;&amp;xd&lt;=0&amp;&amp;yd&gt;=0&amp;&amp;yd&lt;=0" name="VEL7" type="Safety" unsafeSet="loc==3&amp;&amp;yd-xd&gt;4.243">
    <parameters kvalue="2000.0" timehorizon="270.0" timestep="0.1" />
  </property>
  <property initialSet="ProxA:t==0&amp;&amp;loc==2&amp;&amp;xp&lt;=-875&amp;&amp;xp&gt;=-925&amp;&amp;yp&lt;=-375&amp;&amp;yp&gt;=-425&amp;&amp;xd&gt;=0&amp;&amp;xd&lt;=0&amp;&amp;yd&gt;=0&amp;&amp;yd&lt;=0" name="VEL8" type="Safety" unsafeSet="loc==3&amp;&amp;yd+xd&lt;-4.243">
    <parameters kvalue="2000.0" timehorizon="270.0" timestep="0.1" />
  </property>
</hyxml>
