Added Conntrack-related code

1. Conntrack.PNPRO - A basic petri-net version of conntrack from Android and Linux. No RST or FIN, No sequence numbers.
2. Added python code to generate diagram of conntrack TCP state transitions.
This commit is contained in:
BB 2025-05-02 22:29:28 -06:00
parent 786bef11f5
commit d60af90a7a
3 changed files with 766 additions and 1 deletions

325
Conntrack.PNPRO Normal file
View File

@ -0,0 +1,325 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!-- This project file has been saved by the New GreatSPN Editor, v.100 --><project name="NSF TCP copy 2" version="121">
<gspn name="PetriNet">
<nodes>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" marking="1" name="client" x="9.0" y="14.0"/>
<place label-y="-2.0" magnets="FOUR_PER_SIDE" marking="1" name="idle" x="16.0" y="14.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" marking="1" name="ackonce" x="23.0" y="14.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" marking="1" name="ackonce_" x="34.0" y="14.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" marking="1" name="idle_" x="42.0" y="14.0"/>
<place label-y="-2.0" magnets="FOUR_PER_SIDE" name="client_" x="49.0" y="14.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" name="syn2" x="4.0" y="19.0"/>
<place label-y="-2.0" magnets="FIVE_PER_SIDE" name="myisn" x="4.0" y="24.0"/>
<place label-y="-2.0" magnets="FOUR_PER_SIDE" name="theirisn" x="4.0" y="30.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" name="acksent" x="4.0" y="36.0"/>
<place label-x="-2.5" label-y="0.0" magnets="FOUR_PER_SIDE" name="ackrcvd" x="4.0" y="43.0"/>
<place magnets="FIVE_PER_SIDE" name="estab" x="4.0" y="49.0"/>
<place label-x="1.0" magnets="NSEW_SQUARE_POINTS" name="estab_" x="54.0" y="49.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" name="syn2_" x="54.0" y="19.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" name="myisn_" x="54.0" y="24.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" name="theirisn_" x="54.0" y="30.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" name="acksent_" x="54.0" y="36.0"/>
<place label-x="3.5" label-y="0.0" magnets="NSEW_SQUARE_POINTS" name="ackrcvd_" x="54.0" y="43.0"/>
<transition delay="I[1.0]" label-y="2.0" magnets="FOUR_PER_SIDE" name="SYN_" type="GEN" x="39.55" y="18.0"/>
<transition delay="I[1.0]" label-x="0.5" label-y="2.5" magnets="THREE_PER_SIDE" name="SYNACK_" type="GEN" x="39.55" y="27.0"/>
<transition delay="I[1.0]" label-x="-2.0" label-y="-0.5" magnets="THREE_PER_SIDE" name="ACK_" type="GEN" x="39.55" y="36.0"/>
<transition delay="I[1.0]" label-x="0.5" label-y="2.0" magnets="FIVE_PER_SIDE" name="CONNECT_" type="GEN" x="39.55" y="46.0"/>
<transition delay="I[1.0]" label-y="2.5" magnets="FOUR_PER_SIDE" name="SYNACK" type="GEN" x="19.55" y="27.0"/>
<transition delay="I[1.0]" label-x="2.0" label-y="-0.5" magnets="FIVE_PER_SIDE" name="ACK" type="GEN" x="19.55" y="36.0"/>
<transition delay="I[1.0]" label-y="2.0" magnets="FIVE_PER_SIDE" name="CONNECT" type="GEN" x="19.55" y="46.0"/>
<transition delay="I[1.0]" label-y="2.0" magnets="FOUR_PER_SIDE" name="SYN" type="GEN" x="19.55" y="18.0"/>
<place magnets="FIVE_PER_SIDE" name="fin_wait1" x="4.0" y="60.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="finrcvd_" x="54.0" y="54.0"/>
<transition delay="I[1.0]" label-x="2.5" label-y="-1.0" magnets="FOUR_PER_SIDE" name="FIN" type="GEN" x="19.55" y="54.0"/>
<transition delay="I[1.0]" label-x="-2.0" label-y="1.0" magnets="FOUR_PER_SIDE" name="FIN_" type="GEN" x="39.55" y="54.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="finrcvd" x="4.0" y="54.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="fin_wait1_" x="54.0" y="60.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="ackfrcvd" x="4.0" y="66.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="timewait" x="4.0" y="88.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="ackfrcvd_" x="54.0" y="66.0"/>
<place magnets="FIVE_PER_SIDE" name="timewait_" x="54.0" y="88.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="closewait_" x="54.0" y="96.0"/>
<place magnets="FIVE_PER_SIDE" name="closewait" x="4.0" y="96.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="lastack_" x="54.0" y="103.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="lastack" x="4.0" y="103.0"/>
<transition delay="I[1.0]" label-x="2.5" label-y="-1.0" magnets="FOUR_PER_SIDE" name="FIN2" type="GEN" x="19.55" y="84.0"/>
<transition delay="I[1.0]" label-x="-2.0" label-y="-0.5" magnets="FOUR_PER_SIDE" name="FIN2_" type="GEN" x="39.55" y="84.0"/>
<place magnets="FIVE_PER_SIDE" name="closing" x="4.0" y="79.0"/>
<place magnets="FIVE_PER_SIDE" name="closing_" x="54.0" y="79.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="fin2rcvd" x="4.0" y="71.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="fin2rcvd_" x="54.0" y="71.0"/>
<transition delay="I[1.0]" label-x="2.0" label-y="-0.5" magnets="FOUR_PER_SIDE" name="ACKF2b" type="GEN" x="19.55" y="71.0"/>
<transition delay="I[1.0]" label-x="-3.0" label-y="-0.5" magnets="FOUR_PER_SIDE" name="ACKF2b_" type="GEN" x="39.55" y="71.0"/>
<transition delay="I[1.0]" label-x="3.0" label-y="-0.5" magnets="FOUR_PER_SIDE" name="ACKF2a" type="GEN" x="19.55" y="65.0"/>
<transition delay="I[1.0]" label-x="-3.0" label-y="-0.5" magnets="FOUR_PER_SIDE" name="ACKF2a_" type="GEN" x="39.55" y="65.0"/>
<transition delay="I[1.0]" label-x="3.0" label-y="-0.5" magnets="FOUR_PER_SIDE" name="ACKF" type="GEN" x="19.55" y="59.0"/>
<transition delay="I[1.0]" label-x="-2.5" label-y="-0.5" magnets="FOUR_PER_SIDE" name="ACKF_" type="GEN" x="39.55" y="59.0"/>
<transition delay="I[1.0]" label-x="2.5" magnets="FOUR_PER_SIDE" name="END1" type="GEN" x="25.55" y="103.0"/>
<transition delay="I[1.0]" label-x="2.5" magnets="FOUR_PER_SIDE" name="END1_" type="GEN" x="33.55" y="103.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" name="closed" x="27.0" y="7.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" name="closed_" x="30.0" y="7.0"/>
<transition delay="I[1.0]" label-x="2.5" magnets="FOUR_PER_SIDE" name="END2" type="GEN" x="24.55" y="95.0"/>
<transition delay="I[1.0]" label-x="2.5" magnets="FOUR_PER_SIDE" name="END2_" type="GEN" x="34.55" y="95.0"/>
<transition delay="I[1.0]" label-y="2.0" magnets="FOUR_PER_SIDE" name="OPEN" type="GEN" x="16.55" y="7.0"/>
<transition delay="I[1.0]" label-y="2.0" magnets="FOUR_PER_SIDE" name="OPEN_" type="GEN" x="42.55" y="7.0"/>
</nodes>
<edges>
<arc head="ACK" head-magnet="4" kind="INPUT" tail="ackonce"/>
<arc head="SYNACK_" head-magnet="9" kind="INPUT" tail="ackonce_"/>
<arc head="ACK_" head-magnet="9" kind="INPUT" tail="ackonce_"/>
<arc head="client" kind="OUTPUT" tail="SYN"/>
<arc head="SYN" head-magnet="15" kind="INPUT" tail="client" tail-magnet="2"/>
<arc head="SYNACK" head-magnet="0" kind="INPUT" tail="syn2"/>
<arc head="syn2" kind="OUTPUT" mult-k="0.7528320312500001" tail="SYN_" tail-magnet="15">
<point x="19.0" y="22.0"/>
</arc>
<arc head="myisn" kind="OUTPUT" tail="SYN" tail-magnet="8"/>
<arc head="SYNACK" kind="INPUT" tail="myisn"/>
<arc head="myisn" kind="OUTPUT" tail="SYNACK"/>
<arc head="myisn" kind="OUTPUT" tail="ACK" tail-magnet="2"/>
<arc head="CONNECT" head-magnet="3" kind="INPUT" tail="myisn" tail-magnet="5"/>
<arc head="SYNACK" head-magnet="15" kind="INPUT" tail="theirisn" tail-magnet="13"/>
<arc head="theirisn" kind="OUTPUT" tail="SYNACK" tail-magnet="8"/>
<arc head="ACK" kind="INPUT" tail="theirisn" tail-magnet="1"/>
<arc head="theirisn" head-magnet="2" kind="OUTPUT" tail="ACK" tail-magnet="18"/>
<arc head="theirisn" head-magnet="11" kind="OUTPUT" mult-k="0.7139648437500001" tail="SYN_" tail-magnet="8">
<point x="15.408825195312499" y="27.0029296875"/>
</arc>
<arc head="theirisn" head-magnet="0" kind="OUTPUT" tail="SYNACK_"/>
<arc head="ackrcvd_" kind="OUTPUT" mult-k="1.1723632812499996" tail="SYNACK">
<point x="36.5" y="39.0"/>
</arc>
<arc head="acksent" kind="OUTPUT" mult-k="1.4465820312499997" tail="SYNACK" tail-magnet="10">
<point x="18.5883681640625" y="29.79609375"/>
</arc>
<arc head="theirisn_" head-magnet="4" kind="OUTPUT" tail="SYNACK"/>
<arc head="acksent" kind="OUTPUT" tail="ACK" tail-magnet="19"/>
<arc head="ackrcvd_" head-magnet="3" kind="OUTPUT" tail="ACK"/>
<arc head="CONNECT" head-magnet="19" kind="INPUT" tail="ackrcvd" tail-magnet="3"/>
<arc head="estab" head-magnet="17" kind="OUTPUT" tail="CONNECT" tail-magnet="10"/>
<arc head="ackrcvd" head-magnet="0" kind="OUTPUT" tail="ACK_" tail-magnet="6"/>
<arc head="estab_" head-magnet="5" kind="OUTPUT" tail="CONNECT_" tail-magnet="13"/>
<arc head="ackrcvd_" head-magnet="6" kind="OUTPUT" tail="ACK_" tail-magnet="5"/>
<arc head="ACK_" head-magnet="8" kind="INPUT" tail="ackrcvd_" tail-magnet="5"/>
<arc head="acksent_" kind="OUTPUT" tail="ACK_" tail-magnet="5"/>
<arc head="acksent_" kind="OUTPUT" tail="SYNACK_" tail-magnet="8"/>
<arc head="CONNECT_" head-magnet="5" kind="INPUT" tail="theirisn_" tail-magnet="1"/>
<arc head="CONNECT_" head-magnet="1" kind="INPUT" tail="myisn_"/>
<arc head="ACK_" head-magnet="4" kind="INPUT" tail="theirisn_" tail-magnet="2"/>
<arc head="myisn_" kind="OUTPUT" tail="ACK_"/>
<arc head="ACK_" head-magnet="0" kind="INPUT" mult-k="1.23779296875" tail="myisn_" tail-magnet="4">
<point x="49.1533203125" y="29.154296875"/>
</arc>
<arc head="myisn_" head-magnet="5" kind="OUTPUT" tail="SYNACK_"/>
<arc head="theirisn_" head-magnet="5" kind="OUTPUT" tail="SYNACK_"/>
<arc head="myisn_" head-magnet="6" kind="OUTPUT" tail="SYN_" tail-magnet="11"/>
<arc head="SYNACK_" head-magnet="3" kind="INPUT" mult-k="0.52978515625" tail="syn2_" tail-magnet="1">
<point x="41.30672230460764" y="27.118563124920144"/>
</arc>
<arc head="SYN_" head-magnet="0" kind="INPUT" mult-k="1.46240234375" tail="idle_">
<point x="42.0" y="15.0"/>
</arc>
<arc head="SYNACK_" kind="INPUT" tail="idle_"/>
<arc head="SYN_" head-magnet="4" kind="INPUT" tail="client_"/>
<arc head="client_" head-magnet="2" kind="OUTPUT" tail="SYN_"/>
<arc head="SYN" head-magnet="0" kind="INPUT" tail="idle"/>
<arc head="SYN_" head-magnet="7" kind="INPUT" tail="syn2_"/>
<arc head="client_" head-magnet="8" kind="OUTPUT" mult-k="0.7870117187500001" tail="SYN">
<point x="35.5" y="9.0"/>
</arc>
<arc head="syn2_" head-magnet="3" kind="OUTPUT" mult-k="1.29873046875" tail="SYN" tail-magnet="7">
<point x="35.0" y="22.5"/>
<point x="54.28964195971005" y="20.707135384039947"/>
</arc>
<arc head="finrcvd_" kind="OUTPUT" mult-k="3.0999023437500006" tail="FIN" tail-magnet="5">
<point x="30.715747070312503" y="52.51240234375"/>
<point x="35.0" y="52.0"/>
<point x="37.5" y="52.0"/>
</arc>
<arc head="finrcvd" kind="OUTPUT" mult-k="1.6958007812499996" tail="FIN_" tail-magnet="14">
<point x="29.1588232421875" y="53.3053125"/>
<point x="22.0" y="52.0"/>
</arc>
<arc head="fin_wait1" head-magnet="16" kind="OUTPUT" mult-k="1.4465820312499997" tail="FIN" tail-magnet="15">
<point x="17.0" y="55.5"/>
</arc>
<arc head="fin_wait1_" head-magnet="6" kind="OUTPUT" tail="FIN_" tail-magnet="6"/>
<arc head="theirisn_" head-magnet="3" kind="OUTPUT" tail="ACK_" tail-magnet="2"/>
<arc head="ackrcvd" head-magnet="14" kind="OUTPUT" mult-k="1.17373046875" tail="SYNACK_" tail-magnet="11">
<point x="21.5" y="40.0"/>
</arc>
<arc head="CONNECT" head-magnet="17" kind="INPUT" tail="acksent" tail-magnet="1"/>
<arc head="CONNECT" head-magnet="15" kind="INPUT" tail="theirisn" tail-magnet="4"/>
<arc head="ACK" head-magnet="15" kind="INPUT" tail="myisn" tail-magnet="3"/>
<arc head="CONNECT_" head-magnet="8" kind="INPUT" tail="ackrcvd_" tail-magnet="2"/>
<arc head="CONNECT_" head-magnet="7" kind="INPUT" tail="acksent_" tail-magnet="3"/>
<arc head="FIN2" head-magnet="15" kind="INPUT" tail="closewait" tail-magnet="18"/>
<arc head="FIN2_" head-magnet="7" kind="INPUT" tail="closewait_" tail-magnet="5"/>
<arc head="lastack_" head-magnet="5" kind="OUTPUT" tail="FIN2_" tail-magnet="10"/>
<arc head="lastack" kind="OUTPUT" tail="FIN2" tail-magnet="9"/>
<arc head="FIN2_" head-magnet="4" kind="INPUT" tail="ackfrcvd_" tail-magnet="3"/>
<arc head="FIN2" head-magnet="12" kind="INPUT" tail="ackfrcvd" tail-magnet="1"/>
<arc head="FIN" head-magnet="12" kind="INPUT" tail="estab" tail-magnet="0"/>
<arc head="FIN_" head-magnet="4" kind="INPUT" mult-k="1.5290039062499998" tail="estab_" tail-magnet="3">
<point x="55.0" y="50.0"/>
</arc>
<arc head="closewait_" kind="OUTPUT" tail="FIN2" tail-magnet="11"/>
<arc head="closewait" head-magnet="0" kind="OUTPUT" tail="FIN2_" tail-magnet="8"/>
<arc head="ACKF2a" head-magnet="14" kind="INPUT" tail="fin_wait1" tail-magnet="2"/>
<arc head="closing" head-magnet="19" kind="OUTPUT" tail="ACKF2a" tail-magnet="15"/>
<arc head="ACKF2a_" head-magnet="5" kind="INPUT" tail="fin_wait1_" tail-magnet="3"/>
<arc head="closing_" head-magnet="13" kind="OUTPUT" tail="ACKF2a_" tail-magnet="11"/>
<arc head="ACKF2b_" head-magnet="3" kind="INPUT" tail="fin_wait1_" tail-magnet="2"/>
<arc head="ACKF2b" head-magnet="0" kind="INPUT" tail="fin_wait1" tail-magnet="4"/>
<arc head="ACKF2b" head-magnet="15" kind="INPUT" tail="fin2rcvd" tail-magnet="1"/>
<arc head="ACKF2b" head-magnet="12" kind="INPUT" tail="ackfrcvd" tail-magnet="0"/>
<arc head="timewait" head-magnet="7" kind="OUTPUT" tail="ACKF2b" tail-magnet="8"/>
<arc head="ACKF2b_" head-magnet="5" kind="INPUT" tail="ackfrcvd_" tail-magnet="2"/>
<arc head="ACKF2b_" head-magnet="6" kind="INPUT" tail="fin2rcvd_" tail-magnet="2"/>
<arc head="timewait_" kind="OUTPUT" tail="ACKF2b_" tail-magnet="10"/>
<arc head="fin2rcvd_" head-magnet="5" kind="OUTPUT" tail="FIN2" tail-magnet="3"/>
<arc head="fin2rcvd" head-magnet="0" kind="OUTPUT" tail="FIN2_" tail-magnet="12"/>
<arc head="ACKF" head-magnet="12" kind="INPUT" tail="finrcvd" tail-magnet="1"/>
<arc head="ackfrcvd_" head-magnet="4" kind="OUTPUT" tail="ACKF" tail-magnet="6"/>
<arc head="ACKF_" head-magnet="5" kind="INPUT" tail="finrcvd_" tail-magnet="3"/>
<arc head="ackfrcvd" head-magnet="7" kind="OUTPUT" tail="ACKF_" tail-magnet="14"/>
<arc head="closewait_" head-magnet="6" kind="OUTPUT" tail="ACKF_" tail-magnet="10"/>
<arc head="closewait" head-magnet="15" kind="OUTPUT" tail="ACKF" tail-magnet="8"/>
<arc head="ackfrcvd_" head-magnet="6" kind="OUTPUT" tail="ACKF_" tail-magnet="7"/>
<arc head="ackfrcvd" head-magnet="6" kind="OUTPUT" tail="ACKF" tail-magnet="14"/>
<arc head="ACKF_" head-magnet="3" kind="INPUT" tail="estab_" tail-magnet="2"/>
<arc head="END1" head-magnet="8" kind="INPUT" tail="lastack" tail-magnet="1"/>
<arc head="END1_" head-magnet="11" kind="INPUT" tail="lastack_" tail-magnet="2"/>
<arc head="END2" head-magnet="0" kind="INPUT" tail="closing" tail-magnet="3"/>
<arc head="END2" head-magnet="14" kind="INPUT" tail="timewait" tail-magnet="2"/>
<arc head="END2_" head-magnet="4" kind="INPUT" tail="closing_" tail-magnet="10"/>
<arc head="END2_" head-magnet="7" kind="INPUT" tail="timewait_" tail-magnet="6"/>
<arc head="closed" head-magnet="1" kind="OUTPUT" tail="END1" tail-magnet="2"/>
<arc head="closed" head-magnet="3" kind="OUTPUT" tail="END2" tail-magnet="1"/>
<arc head="closed_" head-magnet="3" kind="OUTPUT" tail="END1_" tail-magnet="0"/>
<arc head="closed_" head-magnet="1" kind="OUTPUT" tail="END2_" tail-magnet="0"/>
<arc head="OPEN" head-magnet="5" kind="INPUT" tail="closed" tail-magnet="4"/>
<arc head="OPEN_" head-magnet="13" kind="INPUT" tail="closed_" tail-magnet="0"/>
<arc head="idle" head-magnet="11" kind="OUTPUT" tail="OPEN" tail-magnet="8"/>
<arc head="ackonce" head-magnet="5" kind="OUTPUT" tail="OPEN" tail-magnet="10"/>
<arc head="ackonce_" head-magnet="7" kind="OUTPUT" tail="OPEN_" tail-magnet="8"/>
<arc head="idle_" kind="OUTPUT" tail="OPEN_" tail-magnet="9"/>
<arc head="closing" head-magnet="1" kind="OUTPUT" tail="ACKF2b" tail-magnet="8"/>
<arc head="closing_" head-magnet="11" kind="OUTPUT" tail="ACKF2b_" tail-magnet="7"/>
<arc head="ACKF" head-magnet="0" kind="INPUT" tail="estab" tail-magnet="1"/>
<arc head="END2" head-magnet="8" kind="INPUT" tail="closewait" tail-magnet="2"/>
<arc head="END2_" head-magnet="10" kind="INPUT" tail="closewait_" tail-magnet="3"/>
</edges>
</gspn>
<gspn name="Conntrack" show-color-cmd="false" show-fluid-cmd="false" zoom="75">
<nodes>
<place marking="1" name="sNO" x="2.0" y="23.0"/>
<transition name="syn_no" nservers-x="0.5" type="EXP" x="9.55" y="2.0"/>
<transition name="synack_no_o" nservers-x="0.5" type="EXP" x="10.55" y="21.0"/>
<transition name="ack_no_o" nservers-x="0.5" type="EXP" x="11.55" y="32.0"/>
<transition label-y="-2.0" name="syn_no_r" nservers-x="0.5" type="EXP" x="10.55" y="44.0"/>
<place name="SYN_SENT" x="17.0" y="2.0"/>
<transition name="syn_ss_o" nservers-x="0.5" type="EXP" x="26.55" y="2.0"/>
<place name="ESTB" x="32.0" y="38.0"/>
<place name="sIV_DROP" x="75.0" y="48.0"/>
<transition name="ack_es_o" nservers-x="0.5" type="EXP" x="45.55" y="49.0"/>
<transition name="syn_ss_r" nservers-x="0.5" type="EXP" x="26.55" y="6.0"/>
<place name="SYN_SENT2" x="34.0" y="9.0"/>
<transition name="synack_ss_o" nservers-x="0.5" type="EXP" x="26.55" y="10.0"/>
<transition name="synack_ss_r" nservers-x="0.5" type="EXP" x="26.55" y="14.0"/>
<transition name="ack_ss_o" nservers-x="0.5" type="EXP" x="26.55" y="18.0"/>
<transition name="ack_ss_r" nservers-x="0.5" type="EXP" x="26.55" y="22.0"/>
<transition name="syn_s2_o" nservers-x="0.5" type="EXP" x="43.55" y="2.0"/>
<transition name="syn_s2_r" nservers-x="0.5" type="EXP" x="43.55" y="6.0"/>
<transition name="synack_s2_o" nservers-x="0.5" type="EXP" x="43.55" y="10.0"/>
<transition name="synack_s2_r" nservers-x="0.5" type="EXP" x="43.55" y="14.0"/>
<transition name="ack_s2_o" nservers-x="0.5" type="EXP" x="43.55" y="18.0"/>
<transition name="ack_s2_r" nservers-x="0.5" type="EXP" x="43.55" y="22.0"/>
<place name="SYN_RCVD" x="51.0" y="12.0"/>
<place name="sIG" x="35.0" y="26.0"/>
<transition name="syn_sr_o" nservers-x="0.5" type="EXP" x="60.55" y="2.0"/>
<transition name="syn_sr_r" nservers-x="0.5" type="EXP" x="60.55" y="6.0"/>
<transition name="synack_sr_o" nservers-x="0.5" type="EXP" x="60.55" y="10.0"/>
<transition name="synack_sr_r" nservers-x="0.5" type="EXP" x="60.55" y="14.0"/>
<transition name="ack_sr_o" nservers-x="0.5" type="EXP" x="60.55" y="18.0"/>
<transition name="ack_sr_r" nservers-x="0.5" type="EXP" x="60.55" y="22.0"/>
<transition name="syn_es_o" nservers-x="0.5" type="EXP" x="45.55" y="32.0"/>
<transition name="syn_es_r" nservers-x="0.5" type="EXP" x="45.55" y="36.0"/>
<transition name="ack_es_r" nservers-x="0.5" type="EXP" x="45.55" y="53.0"/>
<transition name="synack_es_o" nservers-x="0.5" type="EXP" x="45.55" y="40.0"/>
<transition name="synack_es_r" nservers-x="0.5" type="EXP" x="45.55" y="44.0"/>
<transition label-y="-2.5" name="IG_sNO" nservers-x="0.5" rotation="-0.0" type="EXP" x="20.55" y="29.0"/>
<transition name="IV_sNO" nservers-x="0.5" rotation="-0.0" type="EXP" x="9.55" y="65.0"/>
</nodes>
<edges>
<arc head="syn_no" kind="INPUT" tail="sNO"/>
<arc head="synack_no_o" kind="INPUT" tail="sNO"/>
<arc head="ack_no_o" kind="INPUT" tail="sNO"/>
<arc head="syn_no_r" kind="INPUT" tail="sNO"/>
<arc head="syn_ss_o" kind="INPUT" tail="SYN_SENT"/>
<arc head="SYN_SENT" kind="OUTPUT" tail="syn_ss_o"/>
<arc head="SYN_SENT" kind="OUTPUT" tail="syn_no"/>
<arc head="ESTB" kind="OUTPUT" tail="ack_no_o"/>
<arc head="sIV_DROP" kind="OUTPUT" tail="synack_no_o"/>
<arc head="sIV_DROP" kind="OUTPUT" tail="syn_no_r"/>
<arc head="ack_es_o" kind="INPUT" tail="ESTB"/>
<arc head="ESTB" kind="OUTPUT" tail="ack_es_o"/>
<arc head="syn_ss_r" kind="INPUT" tail="SYN_SENT"/>
<arc head="SYN_SENT2" kind="OUTPUT" tail="syn_ss_r"/>
<arc head="synack_ss_o" kind="INPUT" tail="SYN_SENT"/>
<arc head="synack_ss_r" kind="INPUT" tail="SYN_SENT"/>
<arc head="ack_ss_o" kind="INPUT" tail="SYN_SENT"/>
<arc head="ack_ss_r" kind="INPUT" tail="SYN_SENT"/>
<arc head="syn_s2_o" kind="INPUT" tail="SYN_SENT2"/>
<arc head="syn_s2_r" kind="INPUT" tail="SYN_SENT2"/>
<arc head="synack_s2_o" kind="INPUT" tail="SYN_SENT2"/>
<arc head="synack_s2_r" kind="INPUT" tail="SYN_SENT2"/>
<arc head="ack_s2_o" kind="INPUT" tail="SYN_SENT2"/>
<arc head="ack_s2_r" kind="INPUT" tail="SYN_SENT2"/>
<arc head="SYN_SENT2" kind="OUTPUT" tail="syn_s2_o"/>
<arc head="SYN_SENT2" kind="OUTPUT" tail="syn_s2_r"/>
<arc head="SYN_RCVD" kind="OUTPUT" tail="synack_s2_o"/>
<arc head="SYN_RCVD" kind="OUTPUT" tail="synack_s2_r"/>
<arc head="sIV_DROP" kind="OUTPUT" tail="ack_s2_o"/>
<arc head="sIG" kind="OUTPUT" tail="ack_s2_r"/>
<arc head="sIV_DROP" kind="OUTPUT" tail="synack_ss_o"/>
<arc head="SYN_RCVD" kind="OUTPUT" tail="synack_ss_r"/>
<arc head="sIV_DROP" kind="OUTPUT" tail="ack_ss_o"/>
<arc head="sIG" kind="OUTPUT" tail="ack_ss_r"/>
<arc head="syn_sr_o" kind="INPUT" tail="SYN_RCVD"/>
<arc head="syn_sr_r" kind="INPUT" tail="SYN_RCVD"/>
<arc head="synack_sr_o" kind="INPUT" tail="SYN_RCVD"/>
<arc head="synack_sr_r" kind="INPUT" tail="SYN_RCVD"/>
<arc head="ack_sr_o" kind="INPUT" tail="SYN_RCVD"/>
<arc head="ack_sr_r" kind="INPUT" tail="SYN_RCVD"/>
<arc head="sIG" kind="OUTPUT" tail="syn_sr_o"/>
<arc head="SYN_RCVD" kind="OUTPUT" tail="synack_sr_o"/>
<arc head="ESTB" kind="OUTPUT" tail="ack_sr_o"/>
<arc head="sIV_DROP" kind="OUTPUT" tail="syn_sr_r"/>
<arc head="sIG" kind="OUTPUT" tail="synack_sr_r"/>
<arc head="SYN_RCVD" kind="OUTPUT" tail="ack_sr_r"/>
<arc head="syn_es_o" kind="INPUT" tail="ESTB"/>
<arc head="sIG" kind="OUTPUT" tail="syn_es_o"/>
<arc head="synack_es_o" kind="INPUT" tail="ESTB"/>
<arc head="sIV_DROP" kind="OUTPUT" tail="synack_es_o"/>
<arc head="syn_es_r" kind="INPUT" tail="ESTB"/>
<arc head="sIV_DROP" kind="OUTPUT" tail="syn_es_r"/>
<arc head="sIG" kind="OUTPUT" tail="synack_es_r"/>
<arc head="synack_es_r" kind="INPUT" tail="ESTB"/>
<arc head="ack_es_r" kind="INPUT" tail="ESTB"/>
<arc head="ESTB" kind="OUTPUT" tail="ack_es_r"/>
<arc head="IG_sNO" kind="INPUT" tail="sIG"/>
<arc head="sNO" kind="OUTPUT" tail="IG_sNO"/>
<arc head="IV_sNO" kind="INPUT" tail="sIV_DROP"/>
<arc head="sNO" kind="OUTPUT" tail="IV_sNO"/>
</edges>
</gspn>
<measures gspn-name="PetriNet" name="Measures" simplified-UI="false">
<assignments/>
<greatspn/>
<formulas>
<formula comment="Basic statistics of the toolchain execution." language="STAT"/>
<formula comment="All the basic Petri net measures" language="ALL"/>
</formulas>
</measures>
</project>

View File

@ -61,7 +61,7 @@
<transition delay="I[1.0]" label-x="2.5" magnets="FOUR_PER_SIDE" name="END2" type="GEN" x="24.55" y="95.0"/> <transition delay="I[1.0]" label-x="2.5" magnets="FOUR_PER_SIDE" name="END2" type="GEN" x="24.55" y="95.0"/>
<transition delay="I[1.0]" label-x="2.5" magnets="FOUR_PER_SIDE" name="END2_" type="GEN" x="34.55" y="95.0"/> <transition delay="I[1.0]" label-x="2.5" magnets="FOUR_PER_SIDE" name="END2_" type="GEN" x="34.55" y="95.0"/>
<transition delay="I[1.0]" label-y="2.0" magnets="FOUR_PER_SIDE" name="OPEN" type="GEN" x="16.55" y="7.0"/> <transition delay="I[1.0]" label-y="2.0" magnets="FOUR_PER_SIDE" name="OPEN" type="GEN" x="16.55" y="7.0"/>
<transition delay="I[1.0]" label-y="2.0" magnets="FOUR_PER_SIDE" name="OPEN_" type="GEN" x="43.55" y="7.0"/> <transition delay="I[1.0]" label-y="2.0" magnets="FOUR_PER_SIDE" name="OPEN_" type="GEN" x="42.55" y="7.0"/>
</nodes> </nodes>
<edges> <edges>
<arc head="ACK" head-magnet="4" kind="INPUT" tail="ackonce"/> <arc head="ACK" head-magnet="4" kind="INPUT" tail="ackonce"/>
@ -211,6 +211,219 @@
<arc head="END2_" head-magnet="10" kind="INPUT" tail="closewait_" tail-magnet="3"/> <arc head="END2_" head-magnet="10" kind="INPUT" tail="closewait_" tail-magnet="3"/>
</edges> </edges>
</gspn> </gspn>
<gspn name="copy of PetriNet" zoom="75">
<nodes>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" marking="1" name="client" x="9.0" y="14.0"/>
<place label-y="-2.0" magnets="FOUR_PER_SIDE" marking="1" name="idle" x="16.0" y="14.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" marking="1" name="ackonce" x="23.0" y="14.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" marking="1" name="ackonce_" x="63.0" y="17.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" marking="1" name="idle_" x="69.0" y="13.0"/>
<place label-y="-2.0" magnets="FOUR_PER_SIDE" name="client_" x="85.0" y="9.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" name="syn2" x="4.0" y="19.0"/>
<place label-y="-2.0" magnets="FIVE_PER_SIDE" name="myisn" x="4.0" y="24.0"/>
<place label-y="-2.0" magnets="FOUR_PER_SIDE" name="theirisn" x="4.0" y="30.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" name="acksent" x="4.0" y="36.0"/>
<place label-x="-2.5" label-y="0.0" magnets="FOUR_PER_SIDE" name="ackrcvd" x="4.0" y="43.0"/>
<place magnets="FIVE_PER_SIDE" name="estab" x="4.0" y="49.0"/>
<place label-x="1.0" magnets="NSEW_SQUARE_POINTS" name="estab_" x="85.0" y="48.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" name="syn2_" x="85.0" y="22.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" name="myisn_" x="81.0" y="27.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" name="theirisn_" x="85.0" y="29.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" name="acksent_" x="85.0" y="35.0"/>
<place label-x="3.5" label-y="0.0" magnets="NSEW_SQUARE_POINTS" name="ackrcvd_" x="85.0" y="42.0"/>
<transition delay="I[1.0]" label-y="2.0" magnets="FOUR_PER_SIDE" name="SYN_" type="GEN" x="73.55" y="18.0"/>
<transition delay="I[1.0]" label-x="0.5" label-y="2.5" magnets="THREE_PER_SIDE" name="SYNACK_" type="GEN" x="73.55" y="29.0"/>
<transition delay="I[1.0]" label-x="-2.0" label-y="-0.5" magnets="THREE_PER_SIDE" name="ACK_" type="GEN" x="72.55" y="37.0"/>
<transition delay="I[1.0]" label-x="0.5" label-y="2.0" magnets="FIVE_PER_SIDE" name="CONNECT_" type="GEN" x="73.55" y="47.0"/>
<transition delay="I[1.0]" label-y="2.5" magnets="FOUR_PER_SIDE" name="SYNACK" type="GEN" x="19.55" y="27.0"/>
<transition delay="I[1.0]" label-x="2.0" label-y="-0.5" magnets="FIVE_PER_SIDE" name="ACK" type="GEN" x="19.55" y="36.0"/>
<transition delay="I[1.0]" label-y="2.0" magnets="FIVE_PER_SIDE" name="CONNECT" type="GEN" x="19.55" y="46.0"/>
<transition delay="I[1.0]" label-y="2.0" magnets="FOUR_PER_SIDE" name="SYN" type="GEN" x="19.55" y="18.0"/>
<place magnets="FIVE_PER_SIDE" name="fin_wait1" x="4.0" y="60.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="finrcvd_" x="85.0" y="54.0"/>
<transition delay="I[1.0]" label-x="2.5" label-y="-1.0" magnets="FOUR_PER_SIDE" name="FIN" type="GEN" x="19.55" y="54.0"/>
<transition delay="I[1.0]" label-x="-2.0" label-y="1.0" magnets="FOUR_PER_SIDE" name="FIN_" type="GEN" x="73.55" y="55.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="finrcvd" x="4.0" y="54.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="fin_wait1_" x="85.0" y="60.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="ackfrcvd" x="4.0" y="66.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="timewait" x="4.0" y="88.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="ackfrcvd_" x="85.0" y="66.0"/>
<place magnets="FIVE_PER_SIDE" name="timewait_" x="85.0" y="90.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="closewait_" x="85.0" y="96.0"/>
<place magnets="FIVE_PER_SIDE" name="closewait" x="4.0" y="96.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="lastack_" x="85.0" y="103.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="lastack" x="4.0" y="103.0"/>
<transition delay="I[1.0]" label-x="2.5" label-y="-1.0" magnets="FOUR_PER_SIDE" name="FIN2" type="GEN" x="19.55" y="84.0"/>
<transition delay="I[1.0]" label-x="-2.0" label-y="-0.5" magnets="FOUR_PER_SIDE" name="FIN2_" type="GEN" x="73.55" y="83.0"/>
<place magnets="FIVE_PER_SIDE" name="closing" x="4.0" y="79.0"/>
<place magnets="FIVE_PER_SIDE" name="closing_" x="85.0" y="83.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="fin2rcvd" x="4.0" y="71.0"/>
<place magnets="NSEW_SQUARE_POINTS" name="fin2rcvd_" x="85.0" y="73.0"/>
<transition delay="I[1.0]" label-x="2.0" label-y="-0.5" magnets="FOUR_PER_SIDE" name="ACKF2b" type="GEN" x="19.55" y="71.0"/>
<transition delay="I[1.0]" label-x="-3.0" label-y="-0.5" magnets="FOUR_PER_SIDE" name="ACKF2b_" type="GEN" x="73.55" y="72.0"/>
<transition delay="I[1.0]" label-x="3.0" label-y="-0.5" magnets="FOUR_PER_SIDE" name="ACKF2a" type="GEN" x="19.55" y="65.0"/>
<transition delay="I[1.0]" label-x="-3.0" label-y="-0.5" magnets="FOUR_PER_SIDE" name="ACKF2a_" type="GEN" x="73.55" y="66.0"/>
<transition delay="I[1.0]" label-x="3.0" label-y="-0.5" magnets="FOUR_PER_SIDE" name="ACKF" type="GEN" x="19.55" y="59.0"/>
<transition delay="I[1.0]" label-x="-2.5" label-y="-0.5" magnets="FOUR_PER_SIDE" name="ACKF_" type="GEN" x="73.55" y="60.0"/>
<transition delay="I[1.0]" label-x="2.5" magnets="FOUR_PER_SIDE" name="END1" type="GEN" x="25.55" y="103.0"/>
<transition delay="I[1.0]" label-x="2.5" magnets="FOUR_PER_SIDE" name="END1_" type="GEN" x="58.55" y="103.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" name="closed" x="27.0" y="7.0"/>
<place label-y="-2.0" magnets="NSEW_SQUARE_POINTS" name="closed_" x="59.0" y="7.0"/>
<transition delay="I[1.0]" label-x="2.5" magnets="FOUR_PER_SIDE" name="END2" type="GEN" x="24.55" y="95.0"/>
<transition delay="I[1.0]" label-x="2.5" magnets="FOUR_PER_SIDE" name="END2_" type="GEN" x="60.55" y="95.0"/>
<transition delay="I[1.0]" label-y="2.0" magnets="FOUR_PER_SIDE" name="OPEN" type="GEN" x="16.55" y="7.0"/>
<transition delay="I[1.0]" label-y="2.0" magnets="FOUR_PER_SIDE" name="LISTEN" type="GEN" x="69.55" y="7.0"/>
<place name="SYN_SENT_fw" x="34.0" y="14.0"/>
<place name="DIR_orig" x="34.0" y="18.0"/>
<place name="DIR_reply" x="37.0" y="26.0"/>
<transition delay="I[1.0]" name="D0" type="GEN" x="45.55" y="16.0"/>
</nodes>
<edges>
<arc head="ACK" head-magnet="4" kind="INPUT" tail="ackonce"/>
<arc head="SYNACK_" head-magnet="9" kind="INPUT" tail="ackonce_"/>
<arc head="ACK_" head-magnet="9" kind="INPUT" tail="ackonce_"/>
<arc head="client" kind="OUTPUT" tail="SYN"/>
<arc head="SYN" head-magnet="15" kind="INPUT" tail="client" tail-magnet="2"/>
<arc head="SYNACK" head-magnet="0" kind="INPUT" tail="syn2"/>
<arc head="syn2" kind="OUTPUT" mult-k="0.7528320312500001" tail="SYN_" tail-magnet="15">
<point x="19.0" y="22.0"/>
</arc>
<arc head="myisn" kind="OUTPUT" tail="SYN" tail-magnet="8"/>
<arc head="SYNACK" kind="INPUT" tail="myisn"/>
<arc head="myisn" kind="OUTPUT" tail="SYNACK"/>
<arc head="myisn" kind="OUTPUT" tail="ACK" tail-magnet="2"/>
<arc head="CONNECT" head-magnet="3" kind="INPUT" tail="myisn" tail-magnet="5"/>
<arc head="SYNACK" head-magnet="15" kind="INPUT" tail="theirisn" tail-magnet="13"/>
<arc head="theirisn" kind="OUTPUT" tail="SYNACK" tail-magnet="8"/>
<arc head="ACK" kind="INPUT" tail="theirisn" tail-magnet="1"/>
<arc head="theirisn" head-magnet="2" kind="OUTPUT" tail="ACK" tail-magnet="18"/>
<arc head="theirisn" head-magnet="11" kind="OUTPUT" mult-k="0.7139648437500001" tail="SYN_" tail-magnet="8">
<point x="15.408825195312499" y="27.0029296875"/>
</arc>
<arc head="theirisn" head-magnet="0" kind="OUTPUT" tail="SYNACK_"/>
<arc head="ackrcvd_" kind="OUTPUT" mult-k="1.1723632812499996" tail="SYNACK">
<point x="29.5" y="30.0"/>
</arc>
<arc head="acksent" kind="OUTPUT" mult-k="1.4465820312499997" tail="SYNACK" tail-magnet="10">
<point x="18.5883681640625" y="29.79609375"/>
</arc>
<arc head="theirisn_" head-magnet="4" kind="OUTPUT" tail="SYNACK"/>
<arc head="acksent" kind="OUTPUT" tail="ACK" tail-magnet="19"/>
<arc head="ackrcvd_" head-magnet="3" kind="OUTPUT" tail="ACK"/>
<arc head="CONNECT" head-magnet="19" kind="INPUT" tail="ackrcvd" tail-magnet="3"/>
<arc head="estab" head-magnet="17" kind="OUTPUT" tail="CONNECT" tail-magnet="10"/>
<arc head="ackrcvd" head-magnet="0" kind="OUTPUT" tail="ACK_" tail-magnet="6"/>
<arc head="estab_" head-magnet="5" kind="OUTPUT" tail="CONNECT_" tail-magnet="13"/>
<arc head="ackrcvd_" head-magnet="6" kind="OUTPUT" tail="ACK_" tail-magnet="5"/>
<arc head="ACK_" head-magnet="8" kind="INPUT" tail="ackrcvd_" tail-magnet="5"/>
<arc head="acksent_" kind="OUTPUT" tail="ACK_" tail-magnet="5"/>
<arc head="acksent_" kind="OUTPUT" tail="SYNACK_" tail-magnet="8"/>
<arc head="CONNECT_" head-magnet="5" kind="INPUT" tail="theirisn_" tail-magnet="1"/>
<arc head="CONNECT_" head-magnet="1" kind="INPUT" tail="myisn_"/>
<arc head="ACK_" head-magnet="4" kind="INPUT" tail="theirisn_" tail-magnet="2"/>
<arc head="myisn_" kind="OUTPUT" tail="ACK_"/>
<arc head="ACK_" head-magnet="0" kind="INPUT" mult-k="1.1194335937499997" tail="myisn_" tail-magnet="4">
<point x="76.5" y="33.0"/>
</arc>
<arc head="myisn_" head-magnet="5" kind="OUTPUT" tail="SYNACK_"/>
<arc head="theirisn_" head-magnet="5" kind="OUTPUT" tail="SYNACK_"/>
<arc head="myisn_" head-magnet="6" kind="OUTPUT" tail="SYN_" tail-magnet="11"/>
<arc head="SYNACK_" head-magnet="3" kind="INPUT" mult-k="0.9420898437499999" tail="syn2_" tail-magnet="1">
<point x="82.5" y="25.0"/>
</arc>
<arc head="SYN_" head-magnet="0" kind="INPUT" mult-k="1.46240234375" tail="idle_">
<point x="72.5" y="16.5"/>
</arc>
<arc head="SYNACK_" kind="INPUT" tail="idle_"/>
<arc head="SYN_" head-magnet="4" kind="INPUT" tail="client_"/>
<arc head="client_" head-magnet="2" kind="OUTPUT" tail="SYN_"/>
<arc head="SYN" head-magnet="0" kind="INPUT" tail="idle"/>
<arc head="SYN_" head-magnet="7" kind="INPUT" tail="syn2_"/>
<arc head="finrcvd_" kind="OUTPUT" mult-k="3.0999023437500006" tail="FIN" tail-magnet="5">
<point x="31.715747070312503" y="55.01240234375"/>
<point x="36.0" y="54.5"/>
<point x="38.5" y="54.5"/>
</arc>
<arc head="finrcvd" kind="OUTPUT" mult-k="1.6958007812499996" tail="FIN_" tail-magnet="14">
<point x="29.1588232421875" y="53.3053125"/>
<point x="22.0" y="52.0"/>
</arc>
<arc head="fin_wait1" head-magnet="16" kind="OUTPUT" mult-k="1.4465820312499997" tail="FIN" tail-magnet="15">
<point x="17.0" y="55.5"/>
</arc>
<arc head="fin_wait1_" head-magnet="6" kind="OUTPUT" tail="FIN_" tail-magnet="6"/>
<arc head="theirisn_" head-magnet="3" kind="OUTPUT" tail="ACK_" tail-magnet="2"/>
<arc head="ackrcvd" head-magnet="14" kind="OUTPUT" mult-k="1.17373046875" tail="SYNACK_" tail-magnet="11">
<point x="21.5" y="40.0"/>
</arc>
<arc head="CONNECT" head-magnet="17" kind="INPUT" tail="acksent" tail-magnet="1"/>
<arc head="CONNECT" head-magnet="15" kind="INPUT" tail="theirisn" tail-magnet="4"/>
<arc head="ACK" head-magnet="15" kind="INPUT" tail="myisn" tail-magnet="3"/>
<arc head="CONNECT_" head-magnet="8" kind="INPUT" tail="ackrcvd_" tail-magnet="2"/>
<arc head="CONNECT_" head-magnet="7" kind="INPUT" tail="acksent_" tail-magnet="3"/>
<arc head="FIN2" head-magnet="15" kind="INPUT" tail="closewait" tail-magnet="18"/>
<arc head="FIN2_" head-magnet="7" kind="INPUT" tail="closewait_" tail-magnet="5"/>
<arc head="lastack_" head-magnet="5" kind="OUTPUT" tail="FIN2_" tail-magnet="10"/>
<arc head="lastack" kind="OUTPUT" tail="FIN2" tail-magnet="9"/>
<arc head="FIN2_" head-magnet="4" kind="INPUT" tail="ackfrcvd_" tail-magnet="3"/>
<arc head="FIN2" head-magnet="12" kind="INPUT" tail="ackfrcvd" tail-magnet="1"/>
<arc head="FIN" head-magnet="12" kind="INPUT" tail="estab" tail-magnet="0"/>
<arc head="FIN_" head-magnet="4" kind="INPUT" mult-k="1.0200195312499996" tail="estab_" tail-magnet="3">
<point x="79.0" y="53.0"/>
</arc>
<arc head="closewait_" kind="OUTPUT" tail="FIN2" tail-magnet="11"/>
<arc head="closewait" head-magnet="0" kind="OUTPUT" tail="FIN2_" tail-magnet="8"/>
<arc head="ACKF2a" head-magnet="14" kind="INPUT" tail="fin_wait1" tail-magnet="2"/>
<arc head="closing" head-magnet="19" kind="OUTPUT" tail="ACKF2a" tail-magnet="15"/>
<arc head="ACKF2a_" head-magnet="5" kind="INPUT" tail="fin_wait1_" tail-magnet="3"/>
<arc head="closing_" head-magnet="13" kind="OUTPUT" tail="ACKF2a_" tail-magnet="11"/>
<arc head="ACKF2b_" head-magnet="3" kind="INPUT" tail="fin_wait1_" tail-magnet="2"/>
<arc head="ACKF2b" head-magnet="0" kind="INPUT" tail="fin_wait1" tail-magnet="4"/>
<arc head="ACKF2b" head-magnet="15" kind="INPUT" tail="fin2rcvd" tail-magnet="1"/>
<arc head="ACKF2b" head-magnet="12" kind="INPUT" tail="ackfrcvd" tail-magnet="0"/>
<arc head="timewait" head-magnet="7" kind="OUTPUT" tail="ACKF2b" tail-magnet="8"/>
<arc head="ACKF2b_" head-magnet="5" kind="INPUT" tail="ackfrcvd_" tail-magnet="2"/>
<arc head="ACKF2b_" head-magnet="6" kind="INPUT" tail="fin2rcvd_" tail-magnet="2"/>
<arc head="timewait_" kind="OUTPUT" tail="ACKF2b_" tail-magnet="10"/>
<arc head="fin2rcvd_" head-magnet="5" kind="OUTPUT" tail="FIN2" tail-magnet="3"/>
<arc head="fin2rcvd" head-magnet="0" kind="OUTPUT" tail="FIN2_" tail-magnet="12"/>
<arc head="ACKF" head-magnet="12" kind="INPUT" tail="finrcvd" tail-magnet="1"/>
<arc head="ackfrcvd_" head-magnet="4" kind="OUTPUT" tail="ACKF" tail-magnet="6"/>
<arc head="ACKF_" head-magnet="5" kind="INPUT" tail="finrcvd_" tail-magnet="3"/>
<arc head="ackfrcvd" head-magnet="7" kind="OUTPUT" tail="ACKF_" tail-magnet="14"/>
<arc head="closewait_" head-magnet="6" kind="OUTPUT" tail="ACKF_" tail-magnet="10"/>
<arc head="closewait" head-magnet="15" kind="OUTPUT" tail="ACKF" tail-magnet="8"/>
<arc head="ackfrcvd_" head-magnet="6" kind="OUTPUT" tail="ACKF_" tail-magnet="7"/>
<arc head="ackfrcvd" head-magnet="6" kind="OUTPUT" tail="ACKF" tail-magnet="14"/>
<arc head="ACKF_" head-magnet="3" kind="INPUT" tail="estab_" tail-magnet="2"/>
<arc head="END1" head-magnet="8" kind="INPUT" tail="lastack" tail-magnet="1"/>
<arc head="END1_" head-magnet="11" kind="INPUT" tail="lastack_" tail-magnet="2"/>
<arc head="END2" head-magnet="0" kind="INPUT" tail="closing" tail-magnet="3"/>
<arc head="END2" head-magnet="14" kind="INPUT" tail="timewait" tail-magnet="2"/>
<arc head="END2_" head-magnet="4" kind="INPUT" tail="closing_" tail-magnet="10"/>
<arc head="END2_" head-magnet="7" kind="INPUT" tail="timewait_" tail-magnet="6"/>
<arc head="closed" head-magnet="1" kind="OUTPUT" tail="END1" tail-magnet="2"/>
<arc head="closed" head-magnet="3" kind="OUTPUT" tail="END2" tail-magnet="1"/>
<arc head="closed_" head-magnet="3" kind="OUTPUT" tail="END1_" tail-magnet="0"/>
<arc head="closed_" head-magnet="1" kind="OUTPUT" tail="END2_" tail-magnet="0"/>
<arc head="OPEN" head-magnet="5" kind="INPUT" tail="closed" tail-magnet="4"/>
<arc head="LISTEN" head-magnet="13" kind="INPUT" tail="closed_" tail-magnet="0"/>
<arc head="idle" head-magnet="11" kind="OUTPUT" tail="OPEN" tail-magnet="8"/>
<arc head="ackonce" head-magnet="5" kind="OUTPUT" tail="OPEN" tail-magnet="10"/>
<arc head="ackonce_" head-magnet="7" kind="OUTPUT" tail="LISTEN" tail-magnet="8"/>
<arc head="idle_" kind="OUTPUT" tail="LISTEN" tail-magnet="9"/>
<arc head="closing" head-magnet="1" kind="OUTPUT" tail="ACKF2b" tail-magnet="8"/>
<arc head="closing_" head-magnet="11" kind="OUTPUT" tail="ACKF2b_" tail-magnet="7"/>
<arc head="ACKF" head-magnet="0" kind="INPUT" tail="estab" tail-magnet="1"/>
<arc head="END2" head-magnet="8" kind="INPUT" tail="closewait" tail-magnet="2"/>
<arc head="END2_" head-magnet="10" kind="INPUT" tail="closewait_" tail-magnet="3"/>
<arc head="SYN_SENT_fw" kind="OUTPUT" tail="SYN" tail-magnet="6"/>
<arc head="DIR_orig" kind="OUTPUT" tail="SYN" tail-magnet="6"/>
<arc head="D0" kind="INPUT" tail="SYN_SENT_fw"/>
<arc head="client_" head-magnet="6" kind="OUTPUT" tail="D0"/>
<arc head="syn2_" head-magnet="4" kind="OUTPUT" tail="D0"/>
</edges>
</gspn>
<measures gspn-name="PetriNet" name="Measures" simplified-UI="false"> <measures gspn-name="PetriNet" name="Measures" simplified-UI="false">
<assignments/> <assignments/>
<greatspn/> <greatspn/>
@ -219,4 +432,25 @@
<formula comment="All the basic Petri net measures" language="ALL"/> <formula comment="All the basic Petri net measures" language="ALL"/>
</formulas> </formulas>
</measures> </measures>
<gspn name="Android" show-color-cmd="false" show-fluid-cmd="false">
<nodes>
<place label-y="-2.0" name="sNO_o" x="12.0" y="11.0"/>
<transition delay="I[1.0]" name="syn_o" type="GEN" x="27.55" y="11.0"/>
<place label-y="-2.0" name="sSS_o" x="35.0" y="6.0"/>
<place marking="1" name="Orig" x="12.0" y="2.0"/>
<transition delay="I[1.0]" name="orig" type="GEN" x="27.55" y="2.0"/>
<transition delay="I[1.0]" name="original" type="GEN" x="4.55" y="6.0"/>
<place name="SYN_orig" x="19.0" y="6.0"/>
</nodes>
<edges>
<arc head="syn_o" kind="INPUT" tail="sNO_o"/>
<arc head="sSS_o" kind="OUTPUT" tail="syn_o"/>
<arc head="orig" kind="INPUT" tail="sSS_o"/>
<arc head="Orig" kind="OUTPUT" tail="orig"/>
<arc head="original" kind="INPUT" tail="Orig"/>
<arc head="sNO_o" kind="OUTPUT" tail="original"/>
<arc head="syn_o" kind="INPUT" tail="SYN_orig"/>
<arc head="SYN_orig" kind="OUTPUT" tail="original"/>
</edges>
</gspn>
</project> </project>

206
src/android_net.py Normal file
View File

@ -0,0 +1,206 @@
import networkx as nx
import matplotlib.pyplot as plt
def build_and_save_graph_labeled(edges, edge_labels=None, output_file='graph.png'):
"""
Builds a network graph with optional edge labels and saves it as a PNG image.
Args:
edges (list of tuple): List of tuples representing edges (e.g., [('A', 'B'), ('B', 'C')]).
edge_labels (dict, optional): Dictionary of edge labels {(u, v): label}.
output_file (str): Path to the output PNG file.
"""
# plt.figure(figsize=(30, 30))
G = nx.DiGraph()
# pos = nx.kamada_kawai_layout(G)
G.add_edges_from(edges)
# pos = nx.spring_layout(G)
pos = nx.kamada_kawai_layout(G)
plt.figure(figsize=(15, 15))
nx.draw(G, pos, with_labels=True, node_color='skyblue',
edge_color='gray',
node_size=2000, font_size=12, font_weight='bold')
if edge_labels:
nx.draw_networkx_edge_labels(G, pos,
edge_labels=edge_labels, font_color='red')
plt.savefig(output_file)
plt.close()
print(f"Graph with edge labels saved to {output_file}")
def build_and_save_graph(edges, output_file='graph.png'):
"""
Builds a network graph from a list of edges and saves it as a PNG image.
Args:
edges (list of tuple): List of tuples representing edges (e.g., [('A', 'B'), ('B', 'C')]).
output_file (str): Path to the output PNG file.
"""
# Create a graph
G = nx.DiGraph()
# Add edges to the graph
G.add_edges_from(edges)
# Create a layout for the graph
pos = nx.spring_layout(G)
# Draw the graph
plt.figure(figsize=(8, 6))
nx.draw(G, pos, with_labels=True, node_color='skyblue', edge_color='gray',
node_size=2000, font_size=12, font_weight='bold')
# Save to PNG
plt.savefig(output_file)
plt.close()
print(f"Graph saved to {output_file}")
def make_edges():
"""
SYN:
* sNO -> sSS Initialize a new connection
* sSS -> sSS Retransmitted SYN
* sS2 -> sS2 Late retransmitted SYN
* sSR -> sIG
* sES -> sIG Error: SYNs in window outside the SYN_SENT state
* are errors. Receiver will reply with RST
* and close the connection.
* Or we are not in sync and hold a dead connection.
* sFW -> sIG
* sCW -> sIG
* sLA -> sIG
* sTW -> sSS Reopened connection (RFC 1122).
* sCL -> sSS
SYN/ACK
* sNO -> sIV Too late and no reason to do anything
* sSS -> sIV Client can't send SYN and then SYN/ACK
* sS2 -> sSR SYN/ACK sent to SYN2 in simultaneous open
* sSR -> sSR Late retransmitted SYN/ACK in simultaneous open
* sES -> sIV Invalid SYN/ACK packets sent by the client
* sFW -> sIV
* sCW -> sIV
* sLA -> sIV
* sTW -> sIV
* sCL -> sIV
FIN
ACK
* sNO -> sES Assumed.
* sSS -> sIV ACK is invalid: we haven't seen a SYN/ACK yet.
* sS2 -> sIV
* sSR -> sES Established state is reached.
* sES -> sES :-)
* sFW -> sCW Normal close request answered by ACK.
* sCW -> sCW
* sLA -> sTW Last ACK detected (RFC5961 challenged)
* sTW -> sTW Retransmitted last ACK. Remain in the same state.
* sCL -> sCL
RST
* sNO, sSS, sSR, sES, sFW, sCW, sLA, sTW, sCL, sS2 */
{ sIV, sCL, sCL, sCL, sCL, sCL, sCL, sCL, sCL, sCL },
REPLY Direction:
SYN:
* sNO -> sIV Never reached.
* sSS -> sS2 Simultaneous open
* sS2 -> sS2 Retransmitted simultaneous SYN
* sSR -> sIV Invalid SYN packets sent by the server
* sES -> sIV
* sFW -> sIV
* sCW -> sIV
* sLA -> sIV
* sTW -> sSS Reopened connection, but server may have switched role
* sCL -> sIV
SYN/ACK
* sSS -> sSR Standard open.
* sS2 -> sSR Simultaneous open
* sSR -> sIG Retransmitted SYN/ACK, ignore it.
* sES -> sIG Late retransmitted SYN/ACK?
* sFW -> sIG Might be SYN/ACK answering ignored SYN
* sCW -> sIG
* sLA -> sIG
* sTW -> sIG
* sCL -> sIG
ACK
* sSS -> sIG Might be a half-open connection.
* sS2 -> sIG
* sSR -> sSR Might answer late resent SYN.
* sES -> sES :-)
* sFW -> sCW Normal close request answered by ACK.
* sCW -> sCW
* sLA -> sTW Last ACK detected (RFC5961 challenged)
* sTW -> sTW Retransmitted last ACK.
* sCL -> sCL
"""
orig_syn_edges = [('sNO','sSS'), ('sSS','sSS'),
('sS2','sS2'),('sSR','sIG'),
('sES','sIG'),('sFW','sIG'),
('sCW','sIG'),('sLA','sIG'),
('sTW','sSS'),('sCL','sSS')]
orig_syn_edges_labels = { e : 'syn_o' for e in orig_syn_edges}
orig_synack_edges = [('sNO','sIV'),('sSS','sIV'),
('sS2','sSR'),('sSR','sSR'),
('sES','sIV'),('sFW','sIV'),
('sCW','sIV'),('sLA','sIV'),
('sTW','sIV'),('sCL','sIV')]
orig_synack_edges_labels = { e : 'syn/ack_o'
for e in orig_synack_edges}
orig_ack_edges =[('sNO','sES'),('sSS','sIV'),
('sS2','sIV'),('sSR','sES'),
('sES','sES'),('sFW','sCW'),
('sCW','sCW'),('sLA','sTW'),
('sTW','sTW'),('sCL','sCL')]
orig_ack_edges_labels = { e : 'ack_o' for e in orig_ack_edges}
reply_syn_edges = [('sNO','sIV'),('sSS','sS2'),
('sS2','sS2'),('sSR','sIV'),
('sES','sIV'),('sFW','sIV'),
('sCW','sIV'),('sLA','sIV'),
('sTW','sSS'),('sCL','sIV')]
reply_syn_edges_labels = { e : 'syn_r'
for e in reply_syn_edges}
reply_synack_edges = [('sSS','sSR'),('sS2','sSR'),
('sSR','sIG'),('sES','sIG'),
('sFW','sIG'),('sCW','sIG'),
('sLA','sIG'),('sTW','sIG'),
('sCL','sIG')]
reply_synack_edges_labels = { e : 'syn/ack_r'
for e in reply_synack_edges}
reply_ack_edges = [('sSS','sIG'),('sS2','sIG'),('sSR','sSR'),
('sES','sES'),('sFW','sCW'),
('sCW','sCW'),('sLA','sTW'),
('sTW','sTW'),('sCL','sCL')]
reply_ack_edges_labels = { e : 'ack_r'
for e in reply_ack_edges}
edges = orig_syn_edges+orig_synack_edges+orig_ack_edges +\
reply_syn_edges+reply_synack_edges+reply_ack_edges
labels = {**orig_syn_edges_labels,**orig_synack_edges_labels,\
**orig_ack_edges_labels,**reply_syn_edges_labels,\
**reply_synack_edges_labels,**reply_ack_edges_labels}
return edges, labels
def main():
edges, labels = make_edges()
build_and_save_graph_labeled(
edges, edge_labels=labels, output_file='my_network.png')
if __name__ == '__main__':
main()