reti ABCD
This commit is contained in:
Francesco Mecca
parent
1c6d6334d2
commit
fd33263a6d
15 changed files with 265 additions and 13 deletions
BIN
anno3/vpc/Balbo.pdf
Normal file
BIN
anno3/vpc/Balbo.pdf
Normal file
Binary file not shown.
BIN
anno3/vpc/consegne/2.b/19-20EsercizioWN.pdf
Normal file
BIN
anno3/vpc/consegne/2.b/19-20EsercizioWN.pdf
Normal file
Binary file not shown.
126
anno3/vpc/consegne/2.b/ReteE.PNPRO
Normal file
126
anno3/vpc/consegne/2.b/ReteE.PNPRO
Normal file
|
|
@ -0,0 +1,126 @@
|
||||||
|
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||||
|
<!-- This project file has been saved by the New GreatSPN Editor, v.100 --><project name="ReteE" version="121">
|
||||||
|
<gspn name="CPN" show-fluid-cmd="false" show-timed-cmd="false" view-rates="false" zoom="75">
|
||||||
|
<nodes>
|
||||||
|
<place label-y="-2.0" marking="R1" name="S0" x="59.0" y="14.0"/>
|
||||||
|
<place label-y="-2.0" marking="R2" name="R0" x="80.0" y="14.0"/>
|
||||||
|
<place domain="Master" name="S1_a" x="53.0" y="20.0"/>
|
||||||
|
<place domain="Master" name="S1_b" x="65.0" y="21.0"/>
|
||||||
|
<place domain="Master" label-x="3.0" label-y="0.0" name="R_1" x="80.0" y="23.0"/>
|
||||||
|
<place domain="Master" label-x="3.5" label-y="0.0" name="R_2" x="80.0" y="31.0"/>
|
||||||
|
<place name="R3" x="80.0" y="39.0"/>
|
||||||
|
<place domain="Master" label-x="-4.5" label-y="-1.5" name="S2_b" x="65.0" y="31.0"/>
|
||||||
|
<place name="S3" x="59.0" y="38.0"/>
|
||||||
|
<place domain="Master" label-x="4.5" label-y="0.0" name="S2_a" x="53.0" y="31.0"/>
|
||||||
|
<transition label-x="-3.0" label-y="0.0" name="T3" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="59.55" y="18.0"/>
|
||||||
|
<transition label-x="2.0" label-y="0.0" name="T4" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="53.55" y="26.0"/>
|
||||||
|
<transition label-x="-2.0" label-y="0.0" name="T5" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="65.55" y="26.0"/>
|
||||||
|
<transition label-y="-2.0" name="T6" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="59.55" y="35.0"/>
|
||||||
|
<transition label-x="2.0" label-y="0.0" name="T9" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="80.55" y="18.0"/>
|
||||||
|
<transition label-x="2.5" label-y="0.0" name="T8" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="80.55" y="27.0"/>
|
||||||
|
<transition label-x="2.0" label-y="0.0" name="T7" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="80.55" y="35.0"/>
|
||||||
|
<transition name="Reset_s" nservers-x="0.5" type="EXP" x="64.55" y="14.0"/>
|
||||||
|
<transition label-y="-2.0" name="Reset_r" nservers-x="0.5" type="EXP" x="85.55" y="14.0"/>
|
||||||
|
<transition label-x="1.0" label-y="-2.0" name="T1" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="29.55" y="18.0"/>
|
||||||
|
<place domain="Master" label-x="-0.5" label-y="2.0" marking="N<All>" name="Richiesta" x="29.0" y="13.0"/>
|
||||||
|
<place domain="Master" label-y="2.0" name="Attesa" x="29.0" y="24.0"/>
|
||||||
|
<place domain="Master" label-y="2.0" name="Elabora" x="29.0" y="34.0"/>
|
||||||
|
<transition name="T2" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="29.55" y="29.0"/>
|
||||||
|
<transition name="T0" nservers-x="0.5" type="EXP" x="23.55" y="34.0"/>
|
||||||
|
<place domain="Master" label-y="-2.0" name="Buffer_input" x="49.0" y="18.0"/>
|
||||||
|
<place domain="Master" name="Buffer_output" x="44.0" y="35.0"/>
|
||||||
|
<color-class definition="m{1..k}" name="Master" x="35.3125" y="8.0"/>
|
||||||
|
<color-var domain="Master" name="m" x="35.9375" y="10.0"/>
|
||||||
|
<template last-binding="1" name="N" type="INTEGER" x="36.0" y="6.0"/>
|
||||||
|
<template last-binding="2" name="R1" type="INTEGER" x="38.0" y="6.0"/>
|
||||||
|
<template last-binding="2" name="R2" type="INTEGER" x="40.0" y="6.0"/>
|
||||||
|
<template last-binding="3" name="k" type="INTEGER" x="79.0" y="35.0"/>
|
||||||
|
</nodes>
|
||||||
|
<edges>
|
||||||
|
<arc head="T3" kind="INPUT" tail="S0"/>
|
||||||
|
<arc head="S1_a" kind="OUTPUT" mult="<m>" tail="T3"/>
|
||||||
|
<arc head="S2_a" kind="OUTPUT" mult="<m>" tail="T4"/>
|
||||||
|
<arc head="T4" kind="INPUT" mult="<m>" tail="S1_a"/>
|
||||||
|
<arc head="T6" kind="INPUT" mult="<m>" tail="S2_a">
|
||||||
|
<point x="60.0" y="35.5"/>
|
||||||
|
</arc>
|
||||||
|
<arc head="S1_b" kind="OUTPUT" mult="<m>" tail="T3"/>
|
||||||
|
<arc head="S2_b" kind="OUTPUT" mult="<m>" tail="T5"/>
|
||||||
|
<arc head="T5" kind="INPUT" mult="<m>" tail="S1_b"/>
|
||||||
|
<arc head="T6" kind="INPUT" mult="<m>" tail="S2_b"/>
|
||||||
|
<arc head="S3" kind="OUTPUT" tail="T6"/>
|
||||||
|
<arc head="T9" kind="INPUT" tail="R0"/>
|
||||||
|
<arc head="R_1" kind="OUTPUT" mult="<m>" tail="T9"/>
|
||||||
|
<arc head="T8" kind="INPUT" mult="<m>" tail="R_1"/>
|
||||||
|
<arc head="R_2" kind="OUTPUT" mult="<m>" tail="T8"/>
|
||||||
|
<arc head="T7" kind="INPUT" mult="<m>" tail="R_2"/>
|
||||||
|
<arc head="R3" kind="OUTPUT" tail="T7"/>
|
||||||
|
<arc head="Reset_s" kind="INPUT" tail="S3">
|
||||||
|
<point x="71.0" y="38.5"/>
|
||||||
|
<point x="71.0" y="15.0"/>
|
||||||
|
</arc>
|
||||||
|
<arc head="S0" kind="OUTPUT" tail="Reset_s"/>
|
||||||
|
<arc head="Reset_r" kind="INPUT" tail="R3">
|
||||||
|
<point x="89.0" y="40.0"/>
|
||||||
|
<point x="89.0" y="15.0"/>
|
||||||
|
</arc>
|
||||||
|
<arc head="R0" kind="OUTPUT" tail="Reset_r"/>
|
||||||
|
<arc head="T1" kind="INPUT" mult="<m>" mult-x="0.5" tail="Richiesta"/>
|
||||||
|
<arc head="Attesa" kind="OUTPUT" mult="<m>" mult-k="1.2018554687500003" tail="T1">
|
||||||
|
<point x="30.0" y="22.0"/>
|
||||||
|
</arc>
|
||||||
|
<arc head="T2" kind="INPUT" mult="<m>" tail="Attesa"/>
|
||||||
|
<arc head="Elabora" kind="OUTPUT" mult="<m>" tail="T2"/>
|
||||||
|
<arc head="Buffer_input" kind="OUTPUT" mult="<m>" tail="T1"/>
|
||||||
|
<arc head="Buffer_output" kind="OUTPUT" mult="<m>" mult-k="0.8393554687500001" tail="T6">
|
||||||
|
<point x="52.0" y="36.0"/>
|
||||||
|
<point x="52.0" y="36.0"/>
|
||||||
|
<point x="52.5" y="36.0"/>
|
||||||
|
</arc>
|
||||||
|
<arc head="T3" kind="INPUT" mult="<m>" tail="Buffer_input"/>
|
||||||
|
<arc head="T0" kind="INPUT" mult="<m>" tail="Elabora"/>
|
||||||
|
<arc head="Richiesta" kind="OUTPUT" mult="<m>" tail="T0">
|
||||||
|
<point x="24.0" y="14.0"/>
|
||||||
|
</arc>
|
||||||
|
<arc head="T2" kind="INPUT" mult="<m>" tail="Buffer_output">
|
||||||
|
<point x="45.0" y="30.0"/>
|
||||||
|
</arc>
|
||||||
|
<arc head="T9" kind="INPUT" mult="<m>" mult-k="1.2639648437500002" tail="Buffer_input">
|
||||||
|
<point x="50.0" y="11.0"/>
|
||||||
|
<point x="76.5" y="11.0"/>
|
||||||
|
<point x="76.5" y="19.0"/>
|
||||||
|
</arc>
|
||||||
|
<arc head="Buffer_output" kind="OUTPUT" mult="<m>" mult-k="2.28427734375" mult-x="-0.5402589824786475" mult-y="3.6422181113892265" tail="T7">
|
||||||
|
<point x="76.5" y="36.0"/>
|
||||||
|
<point x="76.5" y="43.0"/>
|
||||||
|
<point x="45.0" y="42.5"/>
|
||||||
|
</arc>
|
||||||
|
</edges>
|
||||||
|
</gspn>
|
||||||
|
<measures gspn-name="CPN" name="RG of CPN" rapid-type="BUILD_RG" simplified-UI="true">
|
||||||
|
<assignments>
|
||||||
|
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="N"/>
|
||||||
|
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="R1"/>
|
||||||
|
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="R2"/>
|
||||||
|
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="k"/>
|
||||||
|
</assignments>
|
||||||
|
<greatspn/>
|
||||||
|
<formulas>
|
||||||
|
<formula language="STAT"/>
|
||||||
|
<formula language="RG"/>
|
||||||
|
</formulas>
|
||||||
|
</measures>
|
||||||
|
<measures gspn-name="CPN" name="SRG of CPN" rapid-type="BUILD_SYMRG" simplified-UI="true">
|
||||||
|
<assignments>
|
||||||
|
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="N"/>
|
||||||
|
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="R1"/>
|
||||||
|
<assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="R2"/>
|
||||||
|
<assignment bind-model="SINGLE_VALUE" single-val="6" type="INTEGER" varname="k"/>
|
||||||
|
</assignments>
|
||||||
|
<greatspn mode="SWN_SYM"/>
|
||||||
|
<formulas>
|
||||||
|
<formula language="STAT"/>
|
||||||
|
<formula language="RG"/>
|
||||||
|
</formulas>
|
||||||
|
</measures>
|
||||||
|
</project>
|
||||||
BIN
anno3/vpc/consegne/2.b/reteE.jpg
Normal file
BIN
anno3/vpc/consegne/2.b/reteE.jpg
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 52 KiB |
|
|
@ -48,6 +48,30 @@ stesso padre nei seguenti modi:
|
||||||
- usando reti WN
|
- usando reti WN
|
||||||
|
|
||||||
|
|
||||||
|
** TODO Riduzione
|
||||||
|
** TODO P e T invarianti
|
||||||
|
Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi
|
||||||
|
|
||||||
|
[[./semiflowsAT.jpg]]
|
||||||
|
[[./semiflowsAP.jpg]]
|
||||||
|
|
||||||
|
Gli P-invarianti sono i seguenti:
|
||||||
|
| S0 + S1_a + S2_a + S3
|
||||||
|
| S0 + S1_b + S2_b + S3
|
||||||
|
| M0 + M1 + M2 + M3
|
||||||
|
| S1_a + S2_a + Buffer_output + Buffer_input + M0 + M1 + M3
|
||||||
|
| S1_b + S2_b + Buffer_output + Buffer_input + M0 + M1 + M3
|
||||||
|
Il T-invariante e` il seguento:
|
||||||
|
\[
|
||||||
|
Inizio_servizio + azione_locale_sa + azione_locale_sb + \\
|
||||||
|
Fine_servizio + Reset_s + azione_locale_m + Richiesta_servizio + \\
|
||||||
|
Attesa_elaborazione + Reset_m + Reset_s
|
||||||
|
\]
|
||||||
|
|
||||||
|
Dato che la reteA e` interamente coperta dagli P-semiflussi, possiamo
|
||||||
|
affermare che la rete sia bounded.
|
||||||
|
[ ] Deadlock
|
||||||
|
[ ] Liveness
|
||||||
|
|
||||||
* Rete B
|
* Rete B
|
||||||
M master identici, uno slave di tipo 1 e uno slave di tipo 1 scelti
|
M master identici, uno slave di tipo 1 e uno slave di tipo 1 scelti
|
||||||
|
|
@ -98,6 +122,36 @@ Lo slave di tipo 1 processa una sola richiesta alla volta.
|
||||||
Il master in attesa del risultato (M2) potrebbe ricevere il risultato
|
Il master in attesa del risultato (M2) potrebbe ricevere il risultato
|
||||||
di un lavoro richiesto da un altro master.
|
di un lavoro richiesto da un altro master.
|
||||||
|
|
||||||
|
** TODO P e T invarianti
|
||||||
|
Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi
|
||||||
|
|
||||||
|
[[./semiflowsBT.jpg]]
|
||||||
|
[[./semiflowsBP.jpg]]
|
||||||
|
|
||||||
|
Gli P-invarianti sono i seguenti:
|
||||||
|
| S0 + S1_a + S2_a + S3
|
||||||
|
| S0 + S1_b + S2_b + S3
|
||||||
|
| R0 + R1 + R2 + R3
|
||||||
|
| M0 + M1 + M2 + M3
|
||||||
|
| S1_a + S2_a + R1 + R2 + M0 + M1 + M3 + Freechoice + P0 + P1 + Risultato
|
||||||
|
| S1_b + S2_b + R1 + R2 + M0 + M1 + M3 + Freechoice + P0 + P1 + Risultbto
|
||||||
|
Gli T-invarianti sono i seguenti:
|
||||||
|
\[
|
||||||
|
Inizio_servizio_R + azione_locale_R + \\
|
||||||
|
Fine_servizio_R + Reset_R + azione_locale_m + Richiesta_servizio + \\
|
||||||
|
Attesa_elaborazione + Reset_M + Scelta_2
|
||||||
|
\]
|
||||||
|
\[
|
||||||
|
Inizio_servizio_S + azione_locale_sa + azione_locale_sb + \\
|
||||||
|
Fine_servizio_S + Reset_s + azione_locale_m + Richiesta_servizio + \\
|
||||||
|
Attesa_elaborazione + Reset_m + Scelta_1
|
||||||
|
\]
|
||||||
|
|
||||||
|
Dato che la reteB e` interamente coperta dagli P-semiflussi, possiamo
|
||||||
|
affermare che la rete sia bounded.
|
||||||
|
[ ] Deadlock
|
||||||
|
[ ] Liveness
|
||||||
|
|
||||||
* Rete C
|
* Rete C
|
||||||
Due master identici, uno slave di tipo 1 e uno slave di tipo 1 scelti
|
Due master identici, uno slave di tipo 1 e uno slave di tipo 1 scelti
|
||||||
liberamente dai master.
|
liberamente dai master.
|
||||||
|
|
@ -117,10 +171,27 @@ R3 e dalle transizioni Inizio_Servizio_R, Azione_Locale_R, Fine_Servizio e Reset
|
||||||
La richiesta del servizio
|
La richiesta del servizio
|
||||||
verso lo slave scelto e` gestita attraverso due buffer, posti
|
verso lo slave scelto e` gestita attraverso due buffer, posti
|
||||||
FreeChoice e Risultato.
|
FreeChoice e Risultato.
|
||||||
|
** TODO P e T invarianti
|
||||||
|
[ ] Immagini
|
||||||
|
Tramite GreatSPN possiamo calcolare gli T- e P- semiflussi
|
||||||
|
|
||||||
|
[[./semiflowsBT.jpg]]
|
||||||
|
[[./semiflowsBP.jpg]]
|
||||||
|
|
||||||
|
Gli P-invarianti sono i seguenti:
|
||||||
|
Gli T-invarianti sono i seguenti:
|
||||||
|
|
||||||
|
Dato che la reteB e` interamente coperta dagli P-semiflussi, possiamo
|
||||||
|
affermare che la rete sia bounded.
|
||||||
|
[ ] Deadlock
|
||||||
|
[ ] Liveness
|
||||||
|
|
||||||
* Rete D
|
* Rete D
|
||||||
Due master identici, uno slave di tipo 1 e uno slave di tipo 1 scelti
|
Due master identici, uno slave di tipo 1 e uno slave di tipo 1 scelti
|
||||||
associati ciascuno ad un master diverso.
|
associati ciascuno ad un master diverso.
|
||||||
|
|
||||||
#+CAPTION: Modello della reteC
|
#+CAPTION: Modello della reteD
|
||||||
[[./reteD.jpg]]
|
[[./reteD.jpg]]
|
||||||
|
|
||||||
|
** TODO P e T invarianti
|
||||||
|
** TODO Decision Diagram
|
||||||
|
|
|
||||||
BIN
anno3/vpc/consegne/2/riduzioneA.jpg
Normal file
BIN
anno3/vpc/consegne/2/riduzioneA.jpg
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 86 KiB |
BIN
anno3/vpc/consegne/2/semiflowsAP.jpg
Normal file
BIN
anno3/vpc/consegne/2/semiflowsAP.jpg
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 94 KiB |
BIN
anno3/vpc/consegne/2/semiflowsAT.jpg
Normal file
BIN
anno3/vpc/consegne/2/semiflowsAT.jpg
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 93 KiB |
BIN
anno3/vpc/consegne/2/semiflowsBP.jpg
Normal file
BIN
anno3/vpc/consegne/2/semiflowsBP.jpg
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 102 KiB |
BIN
anno3/vpc/consegne/2/semiflowsBT.jpg
Normal file
BIN
anno3/vpc/consegne/2/semiflowsBT.jpg
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 97 KiB |
|
|
@ -37,7 +37,7 @@ Fine_Servizio 1.0 0 0 2 0 2.6666666666666665 4.5 1.609375 4.55729166666666
|
||||||
1 6 0 0
|
1 6 0 0
|
||||||
1 7 0 0
|
1 7 0 0
|
||||||
0
|
0
|
||||||
Reset 1.0 0 0 1 1 1.1666666666666667 5.166666666666667 1.046875 4.973958333333333 1.25 5.234375 0
|
Reset_s 1.0 0 0 1 1 1.1666666666666667 5.166666666666667 0.9739583333333334 4.973958333333333 1.25 5.234375 0
|
||||||
1 6 0 0
|
1 6 0 0
|
||||||
1
|
1
|
||||||
1 1 2 0
|
1 1 2 0
|
||||||
|
|
|
||||||
File diff suppressed because one or more lines are too long
14
anno3/vpc/gspn/EsE.PNPRO
Normal file
14
anno3/vpc/gspn/EsE.PNPRO
Normal file
|
|
@ -0,0 +1,14 @@
|
||||||
|
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||||
|
<!-- This project file has been saved by the New GreatSPN Editor, v.100 --><project name="EsE" version="121">
|
||||||
|
<gspn name="CPN" show-fluid-cmd="false" show-timed-cmd="false" view-rates="false">
|
||||||
|
<nodes/>
|
||||||
|
<edges/>
|
||||||
|
</gspn>
|
||||||
|
<measures gspn-name="CPN" name="Measures" simplified-UI="false">
|
||||||
|
<assignments/>
|
||||||
|
<greatspn/>
|
||||||
|
<formulas>
|
||||||
|
<formula comment="Basic statistics of the toolchain execution." language="STAT"/>
|
||||||
|
</formulas>
|
||||||
|
</measures>
|
||||||
|
</project>
|
||||||
14
anno3/vpc/gspn/es
Normal file
14
anno3/vpc/gspn/es
Normal file
|
|
@ -0,0 +1,14 @@
|
||||||
|
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||||
|
<!-- This project file has been saved by the New GreatSPN Editor, v.100 --><project name="reteE" version="121">
|
||||||
|
<gspn name="PT" show-color-cmd="false" show-fluid-cmd="false" show-timed-cmd="false" view-rates="false">
|
||||||
|
<nodes/>
|
||||||
|
<edges/>
|
||||||
|
</gspn>
|
||||||
|
<measures gspn-name="PT" name="Measures" simplified-UI="false">
|
||||||
|
<assignments/>
|
||||||
|
<greatspn/>
|
||||||
|
<formulas>
|
||||||
|
<formula comment="Basic statistics of the toolchain execution." language="STAT"/>
|
||||||
|
</formulas>
|
||||||
|
</measures>
|
||||||
|
</project>
|
||||||
14
anno3/vpc/gspn/esE.PNPRO
Normal file
14
anno3/vpc/gspn/esE.PNPRO
Normal file
|
|
@ -0,0 +1,14 @@
|
||||||
|
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||||||
|
<!-- This project file has been saved by the New GreatSPN Editor, v.100 --><project name="reteE" version="121">
|
||||||
|
<gspn name="PT" show-color-cmd="false" show-fluid-cmd="false" show-timed-cmd="false" view-rates="false">
|
||||||
|
<nodes/>
|
||||||
|
<edges/>
|
||||||
|
</gspn>
|
||||||
|
<measures gspn-name="PT" name="Measures" simplified-UI="false">
|
||||||
|
<assignments/>
|
||||||
|
<greatspn/>
|
||||||
|
<formulas>
|
||||||
|
<formula comment="Basic statistics of the toolchain execution." language="STAT"/>
|
||||||
|
</formulas>
|
||||||
|
</measures>
|
||||||
|
</project>
|
||||||
Loading…
Reference in a new issue