Merge pull request #1 from bmixonba/main

Added Conntrack-related code
This commit is contained in:
bmixonba 2025-05-02 22:32:53 -06:00 committed by GitHub
commit bc9e2d495a
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
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="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="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>
<edges>
<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"/>
</edges>
</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">
<assignments/>
<greatspn/>
@ -219,4 +432,25 @@
<formula comment="All the basic Petri net measures" language="ALL"/>
</formulas>
</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>

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()