plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/xSAP/examples/tfpg/battery_sensor_fdir/battery_sensor_fdir.txml

<?xml version='1.0' encoding='UTF-8'?>
<tfpg name="DependencyGraph_tightened" infty_semantics="closed">
  <nodesList>
    <node name="G1_Off" isMonitored="false">
      <type>FM</type>
    </node>
    <node name="S2_Off" isMonitored="false">
      <type>FM</type>
    </node>
    <node name="S1_Off" isMonitored="false">
      <type>FM</type>
    </node>
    <node name="G2_Off" isMonitored="false">
      <type>FM</type>
    </node>
    <node name="S1_WO" isMonitored="false">
      <type>OR</type>
    </node>
    <node name="G1_DEAD" isMonitored="false">
      <type>OR</type>
    </node>
    <node name="G2_DEAD" isMonitored="false">
      <type>OR</type>
    </node>
    <node name="S2_WO" isMonitored="false">
      <type>OR</type>
    </node>
    <node name="B2_LOW" isMonitored="true">
      <type>OR</type>
    </node>
    <node name="B1_LOW" isMonitored="true">
      <type>OR</type>
    </node>
    <node name="System_Dead" isMonitored="true">
      <type>AND</type>
    </node>
    <node name="B1_DEAD" isMonitored="false">
      <type>AND</type>
    </node>
    <node name="B2_DEAD" isMonitored="false">
      <type>AND</type>
    </node>
  </nodesList>
  <modesList>
    <mode>Primary</mode>
    <mode>Secondary1</mode>
    <mode>Secondary2</mode>
  </modesList>
  <edgesList>
    <edge name="EDGE1">
      <srcNode>S1_Off</srcNode>
      <tMin>1.0</tMin>
      <tMax>2.0</tMax>
      <modesList>
        <mode>Primary</mode>
        <mode>Secondary1</mode>
        <mode>Secondary2</mode>
      </modesList>
      <destNode>S1_WO</destNode>
    </edge>
    <edge name="EDGE2">
      <srcNode>B1_DEAD</srcNode>
      <tMin>1.0</tMin>
      <tMax>2.0</tMax>
      <modesList>
        <mode>Secondary1</mode>
      </modesList>
      <destNode>S1_WO</destNode>
    </edge>
    <edge name="EDGE3">
      <srcNode>B2_DEAD</srcNode>
      <tMin>1.0</tMin>
      <tMax>2.0</tMax>
      <modesList>
        <mode>Primary</mode>
        <mode>Secondary2</mode>
      </modesList>
      <destNode>S1_WO</destNode>
    </edge>
    <edge name="EDGE4">
      <srcNode>S1_WO</srcNode>
      <tMin>0.0</tMin>
      <tMax>0.0</tMax>
      <modesList>
        <mode>Primary</mode>
        <mode>Secondary1</mode>
        <mode>Secondary2</mode>
      </modesList>
      <destNode>System_Dead</destNode>
    </edge>
    <edge name="EDGE5">
      <srcNode>S2_WO</srcNode>
      <tMin>0.0</tMin>
      <tMax>0.0</tMax>
      <modesList>
        <mode>Primary</mode>
        <mode>Secondary1</mode>
        <mode>Secondary2</mode>
      </modesList>
      <destNode>System_Dead</destNode>
    </edge>
    <edge name="EDGE6">
      <srcNode>G1_Off</srcNode>
      <tMin>0.0</tMin>
      <tMax>0.0</tMax>
      <modesList>
        <mode>Primary</mode>
        <mode>Secondary1</mode>
      </modesList>
      <destNode>G1_DEAD</destNode>
    </edge>
    <edge name="EDGE7">
      <srcNode>G2_Off</srcNode>
      <tMin>0.0</tMin>
      <tMax>0.0</tMax>
      <modesList>
        <mode>Primary</mode>
        <mode>Secondary2</mode>
      </modesList>
      <destNode>G2_DEAD</destNode>
    </edge>
    <edge name="EDGE8">
      <srcNode>S2_Off</srcNode>
      <tMin>1.0</tMin>
      <tMax>2.0</tMax>
      <modesList>
        <mode>Primary</mode>
        <mode>Secondary1</mode>
        <mode>Secondary2</mode>
      </modesList>
      <destNode>S2_WO</destNode>
    </edge>
    <edge name="EDGE9">
      <srcNode>B1_DEAD</srcNode>
      <tMin>1.0</tMin>
      <tMax>2.0</tMax>
      <modesList>
        <mode>Primary</mode>
        <mode>Secondary1</mode>
      </modesList>
      <destNode>S2_WO</destNode>
    </edge>
    <edge name="EDGE10">
      <srcNode>B2_DEAD</srcNode>
      <tMin>1.0</tMin>
      <tMax>2.0</tMax>
      <modesList>
        <mode>Secondary2</mode>
      </modesList>
      <destNode>S2_WO</destNode>
    </edge>
    <edge name="EDGE11">
      <srcNode>G2_DEAD</srcNode>
      <tMin>2.0</tMin>
      <tMax>6.0</tMax>
      <modesList>
        <mode>Primary</mode>
        <mode>Secondary2</mode>
      </modesList>
      <destNode>B2_LOW</destNode>
    </edge>
    <edge name="EDGE12">
      <srcNode>B2_LOW</srcNode>
      <tMin>2.0</tMin>
      <tMax>2.0</tMax>
      <modesList>
        <mode>Primary</mode>
        <mode>Secondary1</mode>
      </modesList>
      <destNode>B1_DEAD</destNode>
    </edge>
    <edge name="EDGE13">
      <srcNode>B1_LOW</srcNode>
      <tMin>1.0</tMin>
      <tMax>3.0</tMax>
      <modesList>
        <mode>Primary</mode>
        <mode>Secondary1</mode>
      </modesList>
      <destNode>B1_DEAD</destNode>
    </edge>
    <edge name="EDGE14">
      <srcNode>G1_DEAD</srcNode>
      <tMin>2.0</tMin>
      <tMax>6.0</tMax>
      <modesList>
        <mode>Primary</mode>
        <mode>Secondary1</mode>
      </modesList>
      <destNode>B1_LOW</destNode>
    </edge>
    <edge name="EDGE15">
      <srcNode>B2_LOW</srcNode>
      <tMin>1.0</tMin>
      <tMax>3.0</tMax>
      <modesList>
        <mode>Primary</mode>
        <mode>Secondary2</mode>
      </modesList>
      <destNode>B2_DEAD</destNode>
    </edge>
    <edge name="EDGE16">
      <srcNode>B1_LOW</srcNode>
      <tMin>2.0</tMin>
      <tMax>2.0</tMax>
      <modesList>
        <mode>Primary</mode>
        <mode>Secondary2</mode>
      </modesList>
      <destNode>B2_DEAD</destNode>
    </edge>
  </edgesList>
</tfpg>