diff --git a/anno3/vpc/c05.pdf b/anno3/vpc/c05.pdf new file mode 100644 index 0000000..9b4911f Binary files /dev/null and b/anno3/vpc/c05.pdf differ diff --git a/anno3/vpc/consegne/3/.#3.2.b.smv b/anno3/vpc/consegne/3/.#3.2.b.smv new file mode 120000 index 0000000..6d16a97 --- /dev/null +++ b/anno3/vpc/consegne/3/.#3.2.b.smv @@ -0,0 +1 @@ +user@thinkgentoo.14302:1588838104 \ No newline at end of file diff --git a/anno3/vpc/consegne/3/3.2-Measures.solution/PT.bnd b/anno3/vpc/consegne/3/3.2-Measures.solution/PT.bnd new file mode 100644 index 0000000..20ae457 --- /dev/null +++ b/anno3/vpc/consegne/3/3.2-Measures.solution/PT.bnd @@ -0,0 +1,10 @@ +0 1 +0 1 +0 1 +0 1 +0 1 +0 1 +0 1 +0 1 +0 1 +0 1 diff --git a/anno3/vpc/consegne/3/3.2-Measures.solution/PT.ctl b/anno3/vpc/consegne/3/3.2-Measures.solution/PT.ctl new file mode 100644 index 0000000..885ff45 --- /dev/null +++ b/anno3/vpc/consegne/3/3.2-Measures.solution/PT.ctl @@ -0,0 +1,2 @@ +% MEASURE0 +AG ( (#Wait_P==1 || #Wait_Q == 1) -> AF (#Critical_P == 1 || #Critical_Q == 1)) diff --git a/anno3/vpc/consegne/3/3.2-Measures.solution/PT.def b/anno3/vpc/consegne/3/3.2-Measures.solution/PT.def new file mode 100644 index 0000000..f9eee66 --- /dev/null +++ b/anno3/vpc/consegne/3/3.2-Measures.solution/PT.def @@ -0,0 +1,3 @@ +|256 +% +| diff --git a/anno3/vpc/consegne/3/3.2-Measures.solution/PT.ilpbnd b/anno3/vpc/consegne/3/3.2-Measures.solution/PT.ilpbnd new file mode 100644 index 0000000..aa47d0d --- /dev/null +++ b/anno3/vpc/consegne/3/3.2-Measures.solution/PT.ilpbnd @@ -0,0 +1,2 @@ +0 +0 diff --git a/anno3/vpc/consegne/3/3.2-Measures.solution/PT.net b/anno3/vpc/consegne/3/3.2-Measures.solution/PT.net new file mode 100644 index 0000000..06bb17f --- /dev/null +++ b/anno3/vpc/consegne/3/3.2-Measures.solution/PT.net @@ -0,0 +1,96 @@ +|0| +| +f 0 10 0 10 0 0 0 +Begin_P 1 2.0 1.3333333333333333 2.008125 0.945625 0 +Wait_P 0 2.0 2.8333333333333335 2.122708333333333 2.6122916666666667 0 +Critical_P 0 2.0 4.5 2.1175 4.195625 0 +Done_P 0 2.0 5.833333333333333 2.27375 5.612291666666667 0 +Turn_P 1 3.5 3.0 3.3674999999999997 2.6122916666666667 0 +Turn_Q 0 6.0 4.666666666666667 6.028958333333333 4.945625 0 +Begin_Q 1 8.0 6.666666666666667 7.252916666666667 6.362291666666667 0 +Wait_Q 0 8.0 4.666666666666667 7.278958333333333 4.445625 0 +Critical_Q 0 8.0 3.1666666666666665 7.02375 2.8622916666666662 0 +Done_Q 0 8.0 1.8333333333333333 7.268541666666667 1.695625 0 +T0 1.0 0 0 1 0 2.0 2.1666666666666665 1.9791666666666667 1.9739583333333333 2.0833333333333335 2.234375 0 + 1 1 0 0 + 1 + 1 2 0 0 + 0 +T1 1.0 0 0 2 0 2.0 3.6666666666666665 1.9791666666666667 3.4739583333333335 2.0833333333333335 3.734375 0 + 1 2 0 0 + 1 5 1 0 +2.6666666666666665 3.0 + 2 + 1 3 0 0 + 1 5 1 0 +2.75 3.0833333333333335 + 0 +T3 1.0 0 0 2 0 2.0 7.0 1.9791666666666667 6.807291666666667 2.0833333333333335 7.067708333333333 0 + 1 4 0 0 + 1 5 1 0 +3.5 6.333333333333333 + 2 + 1 1 2 0 +1.0833333333333333 7.0 +1.0833333333333333 1.3333333333333333 + 1 6 1 0 +5.0 6.916666666666667 + 0 +T2 1.0 0 0 2 0 2.0 5.166666666666667 1.9791666666666667 4.973958333333333 2.0833333333333335 5.234375 0 + 1 3 0 0 + 1 5 1 0 +2.9166666666666665 4.666666666666667 + 2 + 1 4 0 0 + 1 5 1 0 +3.0833333333333335 4.833333333333333 + 0 +T4 1.0 0 0 1 0 8.0 5.333333333333333 7.979166666666667 5.140625 8.083333333333334 5.401041666666667 0 + 1 7 0 0 + 1 + 1 8 0 0 + 0 +T5 1.0 0 0 2 0 8.0 4.0 7.979166666666667 3.8072916666666665 8.083333333333334 4.067708333333333 0 + 1 8 0 0 + 1 6 1 0 +7.25 4.833333333333333 + 2 + 1 9 0 0 + 1 6 1 0 +7.25 4.583333333333333 + 0 +T7 1.0 0 0 2 0 8.0 0.8333333333333334 7.979166666666667 0.640625 8.083333333333334 0.9010416666666666 0 + 1 10 0 0 + 1 6 1 0 +6.416666666666667 2.25 + 2 + 1 7 2 0 +8.75 0.8333333333333334 +8.75 6.666666666666667 + 1 5 1 0 +5.583333333333333 1.1666666666666667 + 0 +T6 1.0 0 0 2 0 8.0 2.5 7.979166666666667 2.3072916666666665 8.083333333333334 2.5677083333333335 0 + 1 9 0 0 + 1 6 1 0 +6.916666666666667 3.1666666666666665 + 2 + 1 10 0 0 + 1 6 1 0 +6.75 3.0833333333333335 + 0 +T8 1.0 0 0 1 1 3.1666666666666665 1.3333333333333333 3.1458333333333335 1.140625 3.25 1.4010416666666667 0 + 1 1 1 0 +2.5833333333333335 1.0833333333333333 + 1 + 1 1 1 0 +2.5833333333333335 1.5833333333333333 + 0 +T9 1.0 0 0 1 1 8.0 7.833333333333333 7.979166666666667 7.640625 8.083333333333334 7.901041666666667 0 + 1 7 1 0 +8.5 7.25 + 1 + 1 7 2 0 +7.583333333333333 7.416666666666667 +7.583333333333333 7.333333333333333 + 0 diff --git a/anno3/vpc/consegne/3/3.2-Measures.solution/PT.pba b/anno3/vpc/consegne/3/3.2-Measures.solution/PT.pba new file mode 100644 index 0000000..77bd7fd --- /dev/null +++ b/anno3/vpc/consegne/3/3.2-Measures.solution/PT.pba @@ -0,0 +1,5 @@ +3 +4 1 1 1 2 1 3 1 4 +2 1 5 1 6 +4 1 7 1 8 1 9 1 10 +0 diff --git a/anno3/vpc/consegne/3/3.2-Measures.solution/PT.pin b/anno3/vpc/consegne/3/3.2-Measures.solution/PT.pin new file mode 100644 index 0000000..3ed7919 --- /dev/null +++ b/anno3/vpc/consegne/3/3.2-Measures.solution/PT.pin @@ -0,0 +1,5 @@ +3 +4 1 7 1 8 1 9 1 10 +2 1 5 1 6 +4 1 1 1 2 1 3 1 4 +0 diff --git a/anno3/vpc/consegne/3/3.2.PNPRO b/anno3/vpc/consegne/3/3.2.PNPRO new file mode 100644 index 0000000..88adb5c --- /dev/null +++ b/anno3/vpc/consegne/3/3.2.PNPRO @@ -0,0 +1,135 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + rO0ABXNyABRqYXZhLnV0aWwuTGlua2VkTGlzdAwpU11KYIgiAwAAeHB3BAAAANt0AJMbWzBtRVhFQzogL3Vzci9sb2NhbC9HcmVhdFNQTi9iaW4vRFNQTi1Ub29sIC1sb2FkICIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuMi1NZWFzdXJlcy5zb2x1dGlvbi9QVCIgLXBiYXNpcyAtZGV0ZWN0LWV4cCAtcHNmbCAtYm5kIAp0AHAbWzFtG1s0bUxPQURJTkcgUEVUUkkgTkVUIC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy4yLU1lYXN1cmVzLnNvbHV0aW9uL1BUIChuZXQvZGVmKS4uLhtbMjJtG1syNG0KdAAPTUFSS0lORyBQQVI6IDAKdAAQUExBQ0VTOiAgICAgIDEwCnQAD1JBVEUgUEFSOiAgICAwCnQAEFRSQU5TSVRJT05TOiAxMAp0AA9NRUFTVVJFUzogICAgMAp0AChMT0FESU5HIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAABCnQAAQp0AB5DT01QVVRJTkcgUExBQ0UgRkxPVyBCQVNJUy4uLgp0ABJNPTEwLCBOPTEwLCBOMD0xMAp0ADhDb21wdXRhdGlvbiBvZiBGbG93IGJhc2lzOiBzdGVwIDEvMTAsIHxLfD04LCBwcm9kdWN0cz0xCnQAUxtbMUEgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAKdABSG1sxQUNvbXB1dGF0aW9uIG9mIEZsb3cgYmFzaXM6IGNvbXBsZXRlZCBpbiA3IHN0ZXBzLCB8S3w9My4gICAgICAgICAgICAgICAgICAgICAgCnQAKUZPVU5EIDMgVkVDVE9SUyBJTiBUSEUgUExBQ0UgRkxPVyBCQVNJUy4KdAABCnQAAQp0ACdBbGwgcGxhY2VzIGFyZSBjb3ZlcmVkIGJ5IHNvbWUgUC1mbG93Lgp0AAEKdAAmVE9UQUwgVElNRTogW1VzZXIgMC4wMDBzLCBTeXMgMC4wMDBzXQp0ACdBVk9JRCBFWFBPTkVOVElBTCBHUk9XVEggT0YgU0VNSUZMT1dTLgp0AB1DT01QVVRJTkcgUExBQ0UgU0VNSUZMT1dTLi4uCnQAEk09MTAsIE49MTAsIE4wPTEwCnQAKkdlbmVyYXRpb24gb2YgU2VtaWZsb3dzOiBzdGVwIDEvMTAsIHxLfD04CnQAUxtbMUEgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAKdABQG1sxQUdlbmVyYXRpb24gb2YgU2VtaWZsb3dzOiBjb21wbGV0ZWQgaW4gNyBzdGVwcywgfEt8PTMuICAgICAgICAgICAgICAgICAgICAgIAp0ABlGT1VORCAzIFBMQUNFIFNFTUlGTE9XUy4KdAABCnQAAQp0ACtBbGwgcGxhY2VzIGFyZSBjb3ZlcmVkIGJ5IHNvbWUgUC1zZW1pZmxvdy4KdAABCnQAJlRPVEFMIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAAsQ09NUFVUSU5HIFBMQUNFIEJPVU5EUyBGUk9NIFAtU0VNSUZMT1dTIC4uLgp0ACcbWzBYG1szMm0gUFJPQ0VTUyBFWElURUQgTk9STUFMTFkuG1swbQp0AKQbWzBtRVhFQzogcGVybCAtZSAnYWxhcm0gNSA7IGV4ZWMgIi91c3IvbG9jYWwvR3JlYXRTUE4vYmluL0RTUE4tVG9vbCAtbG9hZCBcIi9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy4yLU1lYXN1cmVzLnNvbHV0aW9uL1BUXCIgLWxvYWQtYm5kIC1pbHAtYm5kIiAnCnQAcBtbMW0bWzRtTE9BRElORyBQRVRSSSBORVQgL2hvbWUvdXNlci9VTklUTy9hbm5vMy92cGMvY29uc2VnbmUvMy8zLjItTWVhc3VyZXMuc29sdXRpb24vUFQgKG5ldC9kZWYpLi4uG1syMm0bWzI0bQp0AA9NQVJLSU5HIFBBUjogMAp0ABBQTEFDRVM6ICAgICAgMTAKdAAPUkFURSBQQVI6ICAgIDAKdAAQVFJBTlNJVElPTlM6IDEwCnQAD01FQVNVUkVTOiAgICAwCnQAKExPQURJTkcgVElNRTogW1VzZXIgMC4wMDBzLCBTeXMgMC4wMDBzXQp0AAEKdAABCnQAFUxPQURJTkcgQk5EIEZJTEUgLi4uCnQAJUNPTVBVVElORyBQTEFDRSBCT1VORFMgVVNJTkcgSUxQIC4uLgp0ABhBbGwgcGxhY2VzIGFyZSBib3VuZGVkLgpxAH4AJHQAeBtbMG1FWEVDOiAvdXNyL2xvY2FsL0dyZWF0U1BOL2Jpbi9SR01FREQzICIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuMi1NZWFzdXJlcy5zb2x1dGlvbi9QVCIgLU1FVEEgIC1jIC1DCnQAIFJhbmRvbSBzZWVkczogMTU4ODg1NzE0OCAzODgwMzYKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0ABFHcmVhdFNQTi9NZWRkbHkuCnQAOCAgQ29weXJpZ2h0IChDKSAxOTg3LTIwMTgsIFVuaXZlcnNpdHkgb2YgVG9yaW5vLCBJdGFseS4KdAAxICBTZW5kIGZpbGVzIG5ldG5hbWUubmV0LCAuZGVmIHRvIGUtbWFpbCBhZGRyZXNzCnQAKyAgYmVjY3V0aUBkaS51bml0by5pdCBpZiB5b3UgZmluZCBhbnkgYnVnLgp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAH0Jhc2VkIG9uIE1FRERMWSB2ZXJzaW9uIDAuMTYuMAp0AEYgIENvcHlyaWdodCAoQykgMjAwOSwgSW93YSBTdGF0ZSBVbml2ZXJzaXR5IFJlc2VhcmNoIEZvdW5kYXRpb24sIEluYy4KdAApICB3ZWJzaXRlOiBodHRwOi8vbWVkZGx5LnNvdXJjZWZvcmdlLm5ldAp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAKVVzaW5nIHBlci1ldmVudCBzYXR1cmF0aW9uIChzYXQtcHJlZ2VuKS4KdAAbVXNpbmcgZmFzdCBOU0YgZ2VuZXJhdGlvbi4KdAASUHJvY2VzcyBJRDogMjkzODAKdABLTU9ERUwgTkFNRTogL2hvbWUvdXNlci9VTklUTy9hbm5vMy92cGMvY29uc2VnbmUvMy8zLjItTWVhc3VyZXMuc29sdXRpb24vUFQKdAAdICAxMCBwbGFjZXMsIDEwIHRyYW5zaXRpb25zLgp0ACdVc2VkIE1lbW9yeSBmb3IgZW5jb2RpbmcgbmV0OiAzODQwNjhLQgp0AFVPcGVuaW5nIGZpbGU6IC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy4yLU1lYXN1cmVzLnNvbHV0aW9uL1BULmJuZCBPSy4KdABYT3BlbmluZyBmaWxlOiAvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuMi1NZWFzdXJlcy5zb2x1dGlvbi9QVC5pbHBibmQgT0suCnQAEElOUFVUIEFSQ1M6ICAxMAp0ABBPVVRQVVQgQVJDUzogMTAKdAAPSU5ISUIgQVJDUzogIDAKdAAPVEVTVCBBUkNTOiAgIDYKdAAQUExBQ0VTOiAgICAgIDEwCnQAEFRSQU5TSVRJT05TOiAxMAp0AA9JTlZBUklBTlRTOiAgMwp0AA9QLVNFTUlGTE9XUzogMwp0ABZNQVggSU5WQVJJQU5UIENBUkQ6IDEKdAABCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0gVkFSSUFCTEUgT1JERVIgPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAA8VmFyaWFibGUgb3JkZXIgbWV0aG9kOiBNZXRhLWhldXJpc3RpYyB1c2luZyB3ZWlnaHRlZCBzY29yZS4KdABRICBNRVRIT0QgICAgICAgICAgICAgIFNDT1JFICAgICAgICBTV0lSICAgICAgIFNPVVBTIERJU0NPVU5UICBXRUlHSFQgICAgICAgVElNRSAKdABVICBTTE8gICAgICAgICAgICAgICAgICA1Ni4xICAgICAgICAgIDUwICAgICAgICAgIDM3ICAgICAgICAxICAgMS4xMjIgICAwLjAwMDU0NSBzZWMuCnQAVSAgU0xPK0ZvcmNlICAgICAgICAgICAyMy43NiAgICAgICAgICAyNyAgICAgICAgICAyNyAgICAgICAgMSAgICAwLjg4ICAgMC4wMDAxMTggc2VjLgp0AFUgIFNMTy0xNiAgICAgICAgICAgICAgIDM5LjkgICAgICAgICAgNTAgICAgICAgICAgMzcgICAgICAgIDEgICAwLjc5OCAgICA5LjllLTA1IHNlYy4KdABVICBTTE8tMTYrRm9yY2UgICAgICAgMjQuNTk3ICAgICAgICAgIDI3ICAgICAgICAgIDI3ICAgICAgICAxICAgMC45MTEgICAgMy42ZS0wNSBzZWMuCnQAVSAgVE9WMiAgICAgICAgICAgICAgIDM5LjA4NyAgICAgICAgICA0MyAgICAgICAgICAzMiAgICAgICAgMSAgIDAuOTA5ICAgIDQuNGUtMDUgc2VjLgp0AFUgIFRPVjIrRm9yY2UgICAgICAgICAzMS4yNjYgICAgICAgICAgMjcgICAgICAgICAgMjcgICAgICAgIDEgICAxLjE1OCAgICAgIDJlLTA1IHNlYy4KdABVICBOT0FDSzIgICAgICAgICAgICAgODEuNDMyICAgICAgICAgIDcyICAgICAgICAgIDM3ICAgICAgICAxICAgMS4xMzEgICAgMS43ZS0wNSBzZWMuCnQAVSAgTk9BQ0syK0ZvcmNlICAgICAgICAyNi40NiAgICAgICAgICAyNyAgICAgICAgICAyNyAgICAgICAgMSAgICAwLjk4ICAgIDEuOGUtMDUgc2VjLgp0AFUgIEFDTSAgICAgICAgICAgICAgICAzNi4zOTYgICAgICAgICAgMzYgICAgICAgICAgMjkgICAgICAgIDEgICAxLjAxMSAgICAzLjNlLTA1IHNlYy4KdABVICBBQ00rRm9yY2UgICAgICAgICAgMzQuNTA2ICAgICAgICAgIDI3ICAgICAgICAgIDI3ICAgICAgICAxICAgMS4yNzggICAgMS43ZS0wNSBzZWMuCnQAVSAgQ00yICAgICAgICAgICAgICAgICAgNDAuOCAgICAgICAgICAzMiAgICAgICAgICAyOCAgICAgICAgMSAgIDEuMjc1ICAgIDEuN2UtMDUgc2VjLgp0AFUgIENNMitGb3JjZSAgICAgICAgICAyOS42NzMgICAgICAgICAgMjcgICAgICAgICAgMjcgICAgICAgIDEgICAxLjA5OSAgICAyLjVlLTA1IHNlYy4KdABVICBQICAgICAgICAgICAgICAgICAgMjkuMzcyICAgICAgICAgIDI4ICAgICAgICAgIDI4ICAgICAgICAxICAgMS4wNDkgICAgMS42ZS0wNSBzZWMuCnQAVSAgR1AgICAgICAgICAgICAgICAgIDM2LjA1MyAgICAgICAgICAzMSAgICAgICAgICAzMSAgICAgICAgMSAgIDEuMTYzICAgIDcuM2UtMDUgc2VjLgp0AFUgIEdQK0ZvcmNlICAgICAgICAgICAgIDMxLjUgICAgICAgICAgMjggICAgICAgICAgMjggICAgICAgIDEgICAxLjEyNSAgICAyLjZlLTA1IHNlYy4KdAA9TWV0YS1oZXVyaXN0aWM6IHNlbGVjdGluZyBtZXRob2QgU0xPK0ZvcmNlIHdpdGggc2NvcmU6IDIzLjc2CnQAKVRpbWUgdG8gY29tcHV0ZSB2YXJpYWJsZSBvcmRlcjogMC4wMDI3MTcKdAABCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT0gU1RBUlQgRklSSU5HIFJVTEVTIEVOQ09ESU5HID09PT09PT09PT09PT09PT09PT09PT09PT0KdAAsRW5jb2RlZCAxMCB0cmFuc2l0aW9uIGluIDEgcHJpb3JpdHkgZ3JvdXBzLgp0ACFUaW1lIHRvIGJ1aWxkIGFsbCBOU0ZzOiAwLjAwMDM1OQp0AAEKdABQPT09PT09PT09PT09PT09PT09PT09PT09PSBSRUFDSEFCSUxJVFkgU0VUIEdFTkVSQVRJT04gPT09PT09PT09PT09PT09PT09PT09PT09PQp0ABVTcGxpdDogU3BsaXRTdWJ0cmFjdAp0ABxSUyBnZW5lcmF0aW9uIHRpbWU6IDkuMmUtMDUKdAAdQ29tcHV0aW5nIHZhcmlhYmxlIGJvdW5kcy4uLgp0AAEKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0gTUVNT1JZID09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0ACkgVG90YWwgTWVtb3J5IFVzZWQ6ICAgICAgIDM4NDA2OCBLQnl0ZXMuCnQAAQp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09IENUTCBFVkFMVUFUSU9OID09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAAQp0AItQcm9jZXNzaW5nOiAobm90IEUgRiAobm90ICgobm90ICgoV2FpdF9QID0gMSkgb3IgKENyaXRpY2FsX1EgPSAxKSkpIG9yIChub3QgRSBHIChub3QgKChDcml0aWNhbF9QID0gMSkgb3IgKENyaXRpY2FsX1EgPSAxKSkpKSkpKSAgLT4gIGJvb2wKdAANRXZhbDogV2FpdF9QCnQAFCAgICAgIDAuMDAwMDE2IHNlYy4KdAATRXZhbDogKFdhaXRfUCA9IDEpCnQAHiAgICAgIDAuMDAwMDI3IHNlYy4gIGNhcmQgPSA2CnQAEUV2YWw6IENyaXRpY2FsX1EKdAAUICAgICAgMC4wMDAwMDIgc2VjLgp0ABdFdmFsOiAoQ3JpdGljYWxfUSA9IDEpCnQAHiAgICAgIDAuMDAwMDA2IHNlYy4gIGNhcmQgPSAyCnQAKUV2YWw6ICgoV2FpdF9QID0gMSkgb3IgKENyaXRpY2FsX1EgPSAxKSkKdAAeICAgICAgMC4wMDAwMTAgc2VjLiAgY2FyZCA9IDcKdAAvRXZhbDogKG5vdCAoKFdhaXRfUCA9IDEpIG9yIChDcml0aWNhbF9RID0gMSkpKQp0AB4gICAgICAwLjAwMDAxMyBzZWMuICBjYXJkID0gOQp0ABFFdmFsOiBDcml0aWNhbF9QCnQAFCAgICAgIDAuMDAwMDAyIHNlYy4KdAAXRXZhbDogKENyaXRpY2FsX1AgPSAxKQp0AB4gICAgICAwLjAwMDAxNiBzZWMuICBjYXJkID0gMgp0ABFFdmFsOiBDcml0aWNhbF9RCnQAFCAgICAgIDAuMDAwMDAyIHNlYy4KdAAXRXZhbDogKENyaXRpY2FsX1EgPSAxKQp0AB4gICAgICAwLjAwMDAwMyBzZWMuICBjYXJkID0gMgp0AC1FdmFsOiAoKENyaXRpY2FsX1AgPSAxKSBvciAoQ3JpdGljYWxfUSA9IDEpKQp0AB4gICAgICAwLjAwMDAwNCBzZWMuICBjYXJkID0gNAp0ADNFdmFsOiAobm90ICgoQ3JpdGljYWxfUCA9IDEpIG9yIChDcml0aWNhbF9RID0gMSkpKQp0AB8gICAgICAwLjAwMDAwNyBzZWMuICBjYXJkID0gMTIKdAA3RXZhbDogRSBHIChub3QgKChDcml0aWNhbF9QID0gMSkgb3IgKENyaXRpY2FsX1EgPSAxKSkpCnQAIEVHOiBzdGVwPTEsICBTQVQgc2l6ZT0xMC4wMDAwMDAKdAAgRUc6IHN0ZXA9MiwgIFNBVCBzaXplPTEwLjAwMDAwMAp0ABpSMiA9IDEzMyBpbiAyIGl0ZXJhdGlvbnMuCnQAHyAgICAgIDAuMDAwMTE5IHNlYy4gIGNhcmQgPSAxMAp0AD1FdmFsOiAobm90IEUgRyAobm90ICgoQ3JpdGljYWxfUCA9IDEpIG9yIChDcml0aWNhbF9RID0gMSkpKSkKdAAeICAgICAgMC4wMDAwMTIgc2VjLiAgY2FyZCA9IDYKdABrRXZhbDogKChub3QgKChXYWl0X1AgPSAxKSBvciAoQ3JpdGljYWxfUSA9IDEpKSkgb3IgKG5vdCBFIEcgKG5vdCAoKENyaXRpY2FsX1AgPSAxKSBvciAoQ3JpdGljYWxfUSA9IDEpKSkpKQp0AB8gICAgICAwLjAwMDA2NSBzZWMuICBjYXJkID0gMTMKdABxRXZhbDogKG5vdCAoKG5vdCAoKFdhaXRfUCA9IDEpIG9yIChDcml0aWNhbF9RID0gMSkpKSBvciAobm90IEUgRyAobm90ICgoQ3JpdGljYWxfUCA9IDEpIG9yIChDcml0aWNhbF9RID0gMSkpKSkpKQp0AB4gICAgICAwLjAwMDAxMSBzZWMuICBjYXJkID0gMwp0AHVFdmFsOiBFIEYgKG5vdCAoKG5vdCAoKFdhaXRfUCA9IDEpIG9yIChDcml0aWNhbF9RID0gMSkpKSBvciAobm90IEUgRyAobm90ICgoQ3JpdGljYWxfUCA9IDEpIG9yIChDcml0aWNhbF9RID0gMSkpKSkpKQp0AC4gICAgICA3IHN0ZXBzOiAgICAgICAwLjAwMDE2MSBzZWMuICBjYXJkID0gMzIKdAB7RXZhbDogKG5vdCBFIEYgKG5vdCAoKG5vdCAoKFdhaXRfUCA9IDEpIG9yIChDcml0aWNhbF9RID0gMSkpKSBvciAobm90IEUgRyAobm90ICgoQ3JpdGljYWxfUCA9IDEpIG9yIChDcml0aWNhbF9RID0gMSkpKSkpKSkKdAAeICAgICAgMC4wMDAwMTQgc2VjLiAgY2FyZCA9IDAKdABcLS0tIEFHICggKCNXYWl0X1A9PTEgfHwgI0NyaXRpY2FsX1EgPT0gMSkgLT4gQUYgKCNDcml0aWNhbF9QID09IDEgfHwgI0NyaXRpY2FsX1EgPT0gMSkpIC0tLQp0ABlGb3JtdWxhIG5hbWU6IE1FQVNVUkUwICAKdAAWCUV2YWx1YXRpb246IGZhbHNlICAgCnQAJwlTYXQtc2V0IGdlbmVyYXRpb24gdGltZTogMC4wMDA1OTQgc2VjCnQAHwlFdmFsdWF0aW9uIHRpbWU6IDAuMDAwNTk1IHNlYwp0AAEKdAAcR2VuZXJhdGVkIGNvdW50ZXItZXhhbXBsZTogCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PSBUcmFjZSA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAA0SW5pdGlhbCBzdGF0ZSBpczogQmVnaW5fUCgxKSwgVHVybl9QKDEpLCBCZWdpbl9RKDEpCnQAikluaXRpYWwgc3RhdGUgc2F0aXNmaWVzOiBFIEYgKG5vdCAoKG5vdCAoKFdhaXRfUCA9IDEpIG9yIChDcml0aWNhbF9RID0gMSkpKSBvciAobm90IEUgRyAobm90ICgoQ3JpdGljYWxfUCA9IDEpIG9yIChDcml0aWNhbF9RID0gMSkpKSkpKS4gCnQAAQp0ACUxOiBCZWdpbl9QKDEpLCBUdXJuX1AoMSksIEJlZ2luX1EoMSkKdAB9ICBTdGF0ZSAxLiBzYXRpc2ZpZXM6ICgobm90ICgoV2FpdF9QID0gMSkgb3IgKENyaXRpY2FsX1EgPSAxKSkpIG9yIChub3QgRSBHIChub3QgKChDcml0aWNhbF9QID0gMSkgb3IgKENyaXRpY2FsX1EgPSAxKSkpKSkuIAp0AAEKdAApICAxLjE6IEJlZ2luX1AoMSksIFR1cm5fUCgxKSwgQmVnaW5fUSgxKQp0AEYgICAgU3RhdGUgMS4xLiBkb2VzIG5vdCBzYXRpc2Z5OiAoKFdhaXRfUCA9IDEpIG9yIChDcml0aWNhbF9RID0gMSkpLiAKdAABCnQALSAgICAxLjEuMTogQmVnaW5fUCgxKSwgVHVybl9QKDEpLCBCZWdpbl9RKDEpCnQANiAgICAgIFN0YXRlIDEuMS4xLkwuIGRvZXMgbm90IHNhdGlzZnk6IChXYWl0X1AgPSAxKS4gCnQAAQp0ADogICAgICBTdGF0ZSAxLjEuMS5SLiBkb2VzIG5vdCBzYXRpc2Z5OiAoQ3JpdGljYWxfUSA9IDEpLiAKdAABCnQAJDI6IFdhaXRfUCgxKSwgVHVybl9QKDEpLCBCZWdpbl9RKDEpCnQAhCAgU3RhdGUgMi4gZG9lcyBub3Qgc2F0aXNmeTogKChub3QgKChXYWl0X1AgPSAxKSBvciAoQ3JpdGljYWxfUSA9IDEpKSkgb3IgKG5vdCBFIEcgKG5vdCAoKENyaXRpY2FsX1AgPSAxKSBvciAoQ3JpdGljYWxfUSA9IDEpKSkpKS4gCnQAAQp0ACggIDIuMTogV2FpdF9QKDEpLCBUdXJuX1AoMSksIEJlZ2luX1EoMSkKdABBICAgIFN0YXRlIDIuMS5MLiBzYXRpc2ZpZXM6ICgoV2FpdF9QID0gMSkgb3IgKENyaXRpY2FsX1EgPSAxKSkuIAp0AAEKdAAuICAgIDIuMS5MLjE6IFdhaXRfUCgxKSwgVHVybl9QKDEpLCBCZWdpbl9RKDEpCnQALyAgICAgIFN0YXRlIDIuMS5MLjEuIHNhdGlzZmllczogKFdhaXRfUCA9IDEpLiAKdAABCnQAXSAgICBTdGF0ZSAyLjEuUi4gc2F0aXNmaWVzOiBFIEcgKG5vdCAoKENyaXRpY2FsX1AgPSAxKSBvciAoQ3JpdGljYWxfUSA9IDEpKSkuIFN0YXJ0IG9mIGxvb3AuCnQAAQp0AC4gICAgMi4xLlIuMTogV2FpdF9QKDEpLCBUdXJuX1AoMSksIEJlZ2luX1EoMSkKdABQICAgICAgU3RhdGUgMi4xLlIuMS4gZG9lcyBub3Qgc2F0aXNmeTogKChDcml0aWNhbF9QID0gMSkgb3IgKENyaXRpY2FsX1EgPSAxKSkuIAp0AAEKdAAyICAgICAgMi4xLlIuMS4xOiBXYWl0X1AoMSksIFR1cm5fUCgxKSwgQmVnaW5fUSgxKQp0AEAgICAgICAgIFN0YXRlIDIuMS5SLjEuMS5MLiBkb2VzIG5vdCBzYXRpc2Z5OiAoQ3JpdGljYWxfUCA9IDEpLiAKdAABCnQAQCAgICAgICAgU3RhdGUgMi4xLlIuMS4xLlIuIGRvZXMgbm90IHNhdGlzZnk6IChDcml0aWNhbF9RID0gMSkuIAp0AAEKdAApICAgIDIuMS5SLjI6IGxvb3AgYmFjayB0byBzdGF0ZSAyLjEuUi4xLgp0AAEKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09IENUTCBNRU1PUlkgPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0AB0gUlMgbm9kZXM6ICAgICAgICAgICAgICAgIDIxCnQAQCBGb3Jlc3QoUlMpIG5vZGVzOiAgICAgICAgMjMyIGFjdGl2ZXMsIDIzMiBwZWFrLCAwIGNvbXBhY3Rpb25zLgp0ADsgRm9yZXN0KFJTKSBzaXplOiAgICAgICAgIDU4NTYgQnl0ZXMgbm93LCA1ODU2IEJ5dGVzIHBlYWsuCnQAHSBQb3RlbnRpYWwgUkcgbm9kZXM6ICAgICAgNjgKdABAIEZvcmVzdChSRykgbm9kZXM6ICAgICAgICAyMzIgYWN0aXZlcywgMjUzIHBlYWssIDAgY29tcGFjdGlvbnMuCnQAOyBGb3Jlc3QoUkcpIHNpemU6ICAgICAgICAgNjYwNCBCeXRlcyBub3csIDcyMzEgQnl0ZXMgcGVhay4KdAA8IEZvcmVzdChSRytyZWFsKSBub2RlczogICAzIGFjdGl2ZXMsIDMgcGVhaywgMCBjb21wYWN0aW9ucy4KdAA3IEZvcmVzdChSRytyZWFsKSBzaXplOiAgICA4MSBCeXRlcyBub3csIDgxIEJ5dGVzIHBlYWsuCnQAAQp0AARPay4KdAABCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PSBUSU1FID09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAAlIFZhcmlhYmxlIG9yZGVyIFRpbWU6IDAuMDA0ICAgICBzZWMuCnQAJSBOU0YgZ2VuLiBUaW1lOiAgICAgICAwLjAwMCAgICAgc2VjLgp0ACUgUlMgR2VuZXJhdGlvbiBUaW1lOiAgMC4wMDAgICAgIHNlYy4KdAAlIFRvdGFsIFJTIFRpbWU6ICAgICAgIDAuMDAwICAgICBzZWMuCnQAJSBTdGF0aXN0aWNzIFRpbWU6ICAgICAwLjAwMCAgICAgc2VjLgp0ACUgQ1RMIFRpbWU6ICAgICAgICAgICAgMC4wMDEgICAgIHNlYy4KdAAlIFRvdGFsIFRpbWU6ICAgICAgICAgIDAuMDA2ICAgICBzZWMuCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KcQB+ACR4c3EAfgAAdwQAAADbc3IAEWphdmEubGFuZy5Cb29sZWFuzSBygNWc+u4CAAFaAAV2YWx1ZXhwAXEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN1xAH4A3XEAfgDdcQB+AN14 + + diff --git a/anno3/vpc/consegne/3/3.2.b.smv b/anno3/vpc/consegne/3/3.2.b.smv index 94148ac..25d10b1 100644 --- a/anno3/vpc/consegne/3/3.2.b.smv +++ b/anno3/vpc/consegne/3/3.2.b.smv @@ -22,6 +22,8 @@ CTLSPEC -- no individual starvation AG (p.state = wait -> AF p.state = critical) CTLSPEC AG (q.state = wait -> AF q.state = critical) +CTLSPEC + AG (q.state = wait -> EF q.state = critical) MODULE proc(turn, id) -- Model a process taking turn VAR @@ -32,7 +34,7 @@ ASSIGN case state = begin: {begin, wait}; state = wait & turn = id: critical; - state = critical: critical; + state = critical: done; state = done: begin; TRUE: state; esac; \ No newline at end of file diff --git a/anno3/vpc/consegne/3/3.2.jpg b/anno3/vpc/consegne/3/3.2.jpg new file mode 100644 index 0000000..f9ef1ec Binary files /dev/null and b/anno3/vpc/consegne/3/3.2.jpg differ diff --git a/anno3/vpc/consegne/3/3.5-Measures.solution/PT.bnd b/anno3/vpc/consegne/3/3.5-Measures.solution/PT.bnd new file mode 100644 index 0000000..0e49a24 --- /dev/null +++ b/anno3/vpc/consegne/3/3.5-Measures.solution/PT.bnd @@ -0,0 +1,6 @@ +0 1 +0 1 +0 1 +0 1 +0 -1 +0 -1 diff --git a/anno3/vpc/consegne/3/3.5-Measures.solution/PT.ctl b/anno3/vpc/consegne/3/3.5-Measures.solution/PT.ctl new file mode 100644 index 0000000..f9fa1ea --- /dev/null +++ b/anno3/vpc/consegne/3/3.5-Measures.solution/PT.ctl @@ -0,0 +1,8 @@ +% MEASURE1 +AG(!(#Done_P == 1) || !(#Done_Q == 1)) +% MEASURE2 +AG ((#Await_P==1 || #Await_Q == 1) -> AF (#Done_P == 1 || #Done_Q == 1)) +% MEASURE3 +AG ((#Await_P==1 ) -> AF (#Done_P == 1)) +% MEASURE4 +AG ((#Await_Q==1 ) -> AF (#Done_Q == 1)) diff --git a/anno3/vpc/consegne/3/3.5-Measures.solution/PT.def b/anno3/vpc/consegne/3/3.5-Measures.solution/PT.def new file mode 100644 index 0000000..f9eee66 --- /dev/null +++ b/anno3/vpc/consegne/3/3.5-Measures.solution/PT.def @@ -0,0 +1,3 @@ +|256 +% +| diff --git a/anno3/vpc/consegne/3/3.5-Measures.solution/PT.ilpbnd b/anno3/vpc/consegne/3/3.5-Measures.solution/PT.ilpbnd new file mode 100644 index 0000000..1496d21 --- /dev/null +++ b/anno3/vpc/consegne/3/3.5-Measures.solution/PT.ilpbnd @@ -0,0 +1,4 @@ +2 +4 1 +5 1 +0 diff --git a/anno3/vpc/consegne/3/3.5-Measures.solution/PT.net b/anno3/vpc/consegne/3/3.5-Measures.solution/PT.net new file mode 100644 index 0000000..b509ea0 --- /dev/null +++ b/anno3/vpc/consegne/3/3.5-Measures.solution/PT.net @@ -0,0 +1,66 @@ +|0| +| +f 0 6 0 6 0 0 0 +Await_P 1 1.8333333333333333 1.0 2.164375 0.8622916666666667 0 +Done_P 0 1.8333333333333333 2.6666666666666665 1.6070833333333334 2.278958333333333 0 +Turn_P 1 3.0 1.3333333333333333 3.1174999999999997 1.6122916666666667 0 +Turn_Q 0 3.3333333333333335 2.8333333333333335 3.4456249999999997 3.1122916666666662 0 +Await_Q 1 4.833333333333333 3.3333333333333335 5.075833333333333 3.3622916666666662 0 +Done_Q 0 4.833333333333333 1.6666666666666667 5.185208333333333 1.6122916666666667 0 +T0 1.0 0 0 2 1 1.8333333333333333 1.8333333333333333 1.8125 1.640625 1.9166666666666667 1.9010416666666667 0 + 1 1 1 0 +1.25 1.4166666666666667 + 1 3 0 0 + 2 + 1 2 1 0 +1.3333333333333333 2.25 + 1 3 1 0 +2.5833333333333335 1.8333333333333333 + 0 +T1 1.0 0 0 2 1 1.8333333333333333 3.3333333333333335 1.8125 3.140625 1.9166666666666667 3.4010416666666665 0 + 1 2 1 0 +1.4166666666666667 3.0833333333333335 + 1 3 2 0 +2.25 3.0833333333333335 +2.25 2.4166666666666665 + 2 + 1 1 2 0 +1.0833333333333333 3.3333333333333335 +1.0833333333333333 1.0 + 1 4 1 0 +3.0 3.3333333333333335 + 0 +T2 1.0 0 0 1 1 1.8333333333333333 0.3333333333333333 1.8125 0.140625 1.9166666666666667 0.4010416666666667 0 + 1 1 1 0 +1.4166666666666667 0.5 + 1 + 1 1 1 0 +2.1666666666666665 0.5 + 0 +T3 1.0 0 0 1 1 4.833333333333333 4.166666666666667 4.8125 3.9739583333333335 4.916666666666667 4.234375 0 + 1 5 1 0 +4.416666666666667 3.9166666666666665 + 1 + 1 5 1 0 +5.166666666666667 3.9166666666666665 + 0 +T4 1.0 0 0 2 1 4.833333333333333 2.5 4.8125 2.3072916666666665 4.916666666666667 2.5677083333333335 0 + 1 5 1 0 +5.333333333333333 2.9166666666666665 + 1 4 0 0 + 2 + 1 6 1 0 +5.333333333333333 2.0 + 1 4 1 0 +4.0 2.5 + 0 +T5 1.0 0 0 2 1 4.833333333333333 1.0 4.8125 0.8072916666666666 4.916666666666667 1.0677083333333333 0 + 1 6 1 0 +5.333333333333333 1.25 + 1 4 3 0 +4.416666666666667 1.5 +4.5 2.25 +3.4166666666666665 2.5 + 1 + 1 3 0 0 + 0 diff --git a/anno3/vpc/consegne/3/3.5-Measures.solution/PT.pba b/anno3/vpc/consegne/3/3.5-Measures.solution/PT.pba new file mode 100644 index 0000000..0fd18e8 --- /dev/null +++ b/anno3/vpc/consegne/3/3.5-Measures.solution/PT.pba @@ -0,0 +1,4 @@ +2 +2 1 1 1 2 +2 1 3 1 4 +0 diff --git a/anno3/vpc/consegne/3/3.5-Measures.solution/PT.pin b/anno3/vpc/consegne/3/3.5-Measures.solution/PT.pin new file mode 100644 index 0000000..6a34dbf --- /dev/null +++ b/anno3/vpc/consegne/3/3.5-Measures.solution/PT.pin @@ -0,0 +1,4 @@ +2 +2 1 3 1 4 +2 1 1 1 2 +0 diff --git a/anno3/vpc/consegne/3/3.5.PNPRO b/anno3/vpc/consegne/3/3.5.PNPRO new file mode 100644 index 0000000..0c85227 --- /dev/null +++ b/anno3/vpc/consegne/3/3.5.PNPRO @@ -0,0 +1,125 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + rO0ABXNyABRqYXZhLnV0aWwuTGlua2VkTGlzdAwpU11KYIgiAwAAeHB3BAAAATJ0AJMbWzBtRVhFQzogL3Vzci9sb2NhbC9HcmVhdFNQTi9iaW4vRFNQTi1Ub29sIC1sb2FkICIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuNS1NZWFzdXJlcy5zb2x1dGlvbi9QVCIgLXBiYXNpcyAtZGV0ZWN0LWV4cCAtcHNmbCAtYm5kIAp0AHAbWzFtG1s0bUxPQURJTkcgUEVUUkkgTkVUIC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy41LU1lYXN1cmVzLnNvbHV0aW9uL1BUIChuZXQvZGVmKS4uLhtbMjJtG1syNG0KdAAPTUFSS0lORyBQQVI6IDAKdAAPUExBQ0VTOiAgICAgIDYKdAAPUkFURSBQQVI6ICAgIDAKdAAPVFJBTlNJVElPTlM6IDYKdAAPTUVBU1VSRVM6ICAgIDAKdAAoTE9BRElORyBUSU1FOiBbVXNlciAwLjAwMHMsIFN5cyAwLjAwMHNdCnQAAQp0AAEKdAAeQ09NUFVUSU5HIFBMQUNFIEZMT1cgQkFTSVMuLi4KdAAPTT02LCBOPTYsIE4wPTYKdAA3Q29tcHV0YXRpb24gb2YgRmxvdyBiYXNpczogc3RlcCAxLzYsIHxLfD00LCBwcm9kdWN0cz0xCnQAUxtbMUEgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAKdABSG1sxQUNvbXB1dGF0aW9uIG9mIEZsb3cgYmFzaXM6IGNvbXBsZXRlZCBpbiA0IHN0ZXBzLCB8S3w9Mi4gICAgICAgICAgICAgICAgICAgICAgCnQAKUZPVU5EIDIgVkVDVE9SUyBJTiBUSEUgUExBQ0UgRkxPVyBCQVNJUy4KdAABCnQAAQp0AC5UaGVyZSBhcmUgMiBwbGFjZXMgbm90IGNvdmVyZWQgYnkgYW55IFAtZmxvdzoKdAABCnQAJlRPVEFMIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAAnQVZPSUQgRVhQT05FTlRJQUwgR1JPV1RIIE9GIFNFTUlGTE9XUy4KdAAdQ09NUFVUSU5HIFBMQUNFIFNFTUlGTE9XUy4uLgp0AA9NPTYsIE49NiwgTjA9Ngp0AClHZW5lcmF0aW9uIG9mIFNlbWlmbG93czogc3RlcCAxLzYsIHxLfD00CnQAUxtbMUEgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAKdABQG1sxQUdlbmVyYXRpb24gb2YgU2VtaWZsb3dzOiBjb21wbGV0ZWQgaW4gNCBzdGVwcywgfEt8PTIuICAgICAgICAgICAgICAgICAgICAgIAp0ABlGT1VORCAyIFBMQUNFIFNFTUlGTE9XUy4KdAABCnQAAQp0ADJUaGVyZSBhcmUgMiBwbGFjZXMgbm90IGNvdmVyZWQgYnkgYW55IFAtc2VtaWZsb3c6CnQAAQp0ACZUT1RBTCBUSU1FOiBbVXNlciAwLjAwMHMsIFN5cyAwLjAwMHNdCnQALENPTVBVVElORyBQTEFDRSBCT1VORFMgRlJPTSBQLVNFTUlGTE9XUyAuLi4KdAAnG1swWBtbMzJtIFBST0NFU1MgRVhJVEVEIE5PUk1BTExZLhtbMG0KdACkG1swbUVYRUM6IHBlcmwgLWUgJ2FsYXJtIDUgOyBleGVjICIvdXNyL2xvY2FsL0dyZWF0U1BOL2Jpbi9EU1BOLVRvb2wgLWxvYWQgXCIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuNS1NZWFzdXJlcy5zb2x1dGlvbi9QVFwiIC1sb2FkLWJuZCAtaWxwLWJuZCIgJwp0AHAbWzFtG1s0bUxPQURJTkcgUEVUUkkgTkVUIC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy41LU1lYXN1cmVzLnNvbHV0aW9uL1BUIChuZXQvZGVmKS4uLhtbMjJtG1syNG0KdAAPTUFSS0lORyBQQVI6IDAKdAAPUExBQ0VTOiAgICAgIDYKdAAPUkFURSBQQVI6ICAgIDAKdAAPVFJBTlNJVElPTlM6IDYKdAAPTUVBU1VSRVM6ICAgIDAKdAAoTE9BRElORyBUSU1FOiBbVXNlciAwLjAwMHMsIFN5cyAwLjAwMHNdCnQAAQp0AAEKdAAVTE9BRElORyBCTkQgRklMRSAuLi4KdAAlQ09NUFVUSU5HIFBMQUNFIEJPVU5EUyBVU0lORyBJTFAgLi4uCnQAGEFsbCBwbGFjZXMgYXJlIGJvdW5kZWQuCnEAfgAkdAB/G1swbUVYRUM6IC91c3IvbG9jYWwvR3JlYXRTUE4vYmluL1JHTUVERDMgIi9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy41LU1lYXN1cmVzLnNvbHV0aW9uL1BUIiAtTUVUQSAgLWd1aS1zdGF0IC1DCnQAIFJhbmRvbSBzZWVkczogMTU4ODg2MTM4NyAxMjU3NTgKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0ABFHcmVhdFNQTi9NZWRkbHkuCnQAOCAgQ29weXJpZ2h0IChDKSAxOTg3LTIwMTgsIFVuaXZlcnNpdHkgb2YgVG9yaW5vLCBJdGFseS4KdAAxICBTZW5kIGZpbGVzIG5ldG5hbWUubmV0LCAuZGVmIHRvIGUtbWFpbCBhZGRyZXNzCnQAKyAgYmVjY3V0aUBkaS51bml0by5pdCBpZiB5b3UgZmluZCBhbnkgYnVnLgp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAH0Jhc2VkIG9uIE1FRERMWSB2ZXJzaW9uIDAuMTYuMAp0AEYgIENvcHlyaWdodCAoQykgMjAwOSwgSW93YSBTdGF0ZSBVbml2ZXJzaXR5IFJlc2VhcmNoIEZvdW5kYXRpb24sIEluYy4KdAApICB3ZWJzaXRlOiBodHRwOi8vbWVkZGx5LnNvdXJjZWZvcmdlLm5ldAp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAKVVzaW5nIHBlci1ldmVudCBzYXR1cmF0aW9uIChzYXQtcHJlZ2VuKS4KdAAbVXNpbmcgZmFzdCBOU0YgZ2VuZXJhdGlvbi4KdAARUHJvY2VzcyBJRDogMTMxMgp0AEtNT0RFTCBOQU1FOiAvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuNS1NZWFzdXJlcy5zb2x1dGlvbi9QVAp0ABsgIDYgcGxhY2VzLCA2IHRyYW5zaXRpb25zLgp0ACdVc2VkIE1lbW9yeSBmb3IgZW5jb2RpbmcgbmV0OiAzOTI1MjRLQgp0AFVPcGVuaW5nIGZpbGU6IC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy41LU1lYXN1cmVzLnNvbHV0aW9uL1BULmJuZCBPSy4KdABYT3BlbmluZyBmaWxlOiAvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuNS1NZWFzdXJlcy5zb2x1dGlvbi9QVC5pbHBibmQgT0suCnQAD0lOUFVUIEFSQ1M6ICA2CnQAD09VVFBVVCBBUkNTOiA1CnQAD0lOSElCIEFSQ1M6ICAwCnQAD1RFU1QgQVJDUzogICA0CnQAD1BMQUNFUzogICAgICA2CnQAD1RSQU5TSVRJT05TOiA2CnQAD0lOVkFSSUFOVFM6ICAyCnQAD1AtU0VNSUZMT1dTOiAyCnQAFk1BWCBJTlZBUklBTlQgQ0FSRDogMQp0AAEKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PSBWQVJJQUJMRSBPUkRFUiA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0ADxWYXJpYWJsZSBvcmRlciBtZXRob2Q6IE1ldGEtaGV1cmlzdGljIHVzaW5nIHdlaWdodGVkIHNjb3JlLgp0ABhOdW1iZXIgb2YgY29tcG9uZW50czogMwp0AFEgIE1FVEhPRCAgICAgICAgICAgICAgU0NPUkUgICAgICAgIFNXSVIgICAgICAgU09VUFMgRElTQ09VTlQgIFdFSUdIVCAgICAgICBUSU1FIAp0AFUgIFNMTyAgICAgICAgICAgICAgICAxNS43MDggICAgICAgICAgMTQgICAgICAgICAgMTQgICAgICAgIDEgICAxLjEyMiAgIDAuMDAwMjUxIHNlYy4KdABVICBTTE8rRm9yY2UgICAgICAgICAgIDEwLjU2ICAgICAgICAgIDEyICAgICAgICAgIDEyICAgICAgICAxICAgIDAuODggICAgNy45ZS0wNSBzZWMuCnQAVSAgU0xPLTE2ICAgICAgICAgICAgIDExLjE3MiAgICAgICAgICAxNCAgICAgICAgICAxNCAgICAgICAgMSAgIDAuNzk4ICAgIDUuNmUtMDUgc2VjLgp0AFUgIFNMTy0xNitGb3JjZSAgICAgICAxMC45MzIgICAgICAgICAgMTIgICAgICAgICAgMTIgICAgICAgIDEgICAwLjkxMSAgICAgIDVlLTA1IHNlYy4KdABVICBUT1YyICAgICAgICAgICAgICAgMTAuOTA4ICAgICAgICAgIDEyICAgICAgICAgIDEyICAgICAgICAxICAgMC45MDkgICAgNS4yZS0wNSBzZWMuCnQAVSAgVE9WMitGb3JjZSAgICAgICAgIDEzLjg5NiAgICAgICAgICAxMiAgICAgICAgICAxMiAgICAgICAgMSAgIDEuMTU4ICAgIDMuOWUtMDUgc2VjLgp0AFUgIE5PQUNLMiAgICAgICAgICAgICAyMS40ODkgICAgICAgICAgMTkgICAgICAgICAgMTYgICAgICAgIDEgICAxLjEzMSAgICAyLjZlLTA1IHNlYy4KdABVICBOT0FDSzIrRm9yY2UgICAgICAgIDExLjc2ICAgICAgICAgIDEyICAgICAgICAgIDEyICAgICAgICAxICAgIDAuOTggICAgMi42ZS0wNSBzZWMuCnQAVSAgQUNNICAgICAgICAgICAgICAgIDEyLjEzMiAgICAgICAgICAxMiAgICAgICAgICAxMiAgICAgICAgMSAgIDEuMDExICAgIDUuNmUtMDUgc2VjLgp0AFUgIEFDTStGb3JjZSAgICAgICAgICAxNS4zMzYgICAgICAgICAgMTIgICAgICAgICAgMTIgICAgICAgIDEgICAxLjI3OCAgICAgIDRlLTA1IHNlYy4KdABVICBDTTIgICAgICAgICAgICAgICAgICAxNS4zICAgICAgICAgIDEyICAgICAgICAgIDEyICAgICAgICAxICAgMS4yNzUgICAgMS43ZS0wNSBzZWMuCnQAVSAgQ00yK0ZvcmNlICAgICAgICAgIDEzLjE4OCAgICAgICAgICAxMiAgICAgICAgICAxMiAgICAgICAgMSAgIDEuMDk5ICAgIDQuMWUtMDUgc2VjLgp0AFUgIFAgICAgICAgICAgICAgICAgICAxNC42ODYgICAgICAgICAgMTQgICAgICAgICAgMTQgICAgICAgIDEgICAxLjA0OSAgICAyLjRlLTA1IHNlYy4KdABVICBHUCAgICAgICAgICAgICAgICAgMTYuMjgyICAgICAgICAgIDE0ICAgICAgICAgIDE0ICAgICAgICAxICAgMS4xNjMgICAwLjAwMDEwMSBzZWMuCnQAVSAgR1ArRm9yY2UgICAgICAgICAgIDE0LjYyNSAgICAgICAgICAxMyAgICAgICAgICAxMyAgICAgICAgMSAgIDEuMTI1ICAgIDQuNWUtMDUgc2VjLgp0AFUgIFRTICAgICAgICAgICAgICAgICAgOC4yMDggICAgICAgICAgMTIgICAgICAgICAgMTIgICAgICAgIDEgICAwLjY4NCAgICAyLjdlLTA1IHNlYy4KdABVICBUUytGb3JjZSAgICAgICAgICAgIDkuNDY4ICAgICAgICAgIDEyICAgICAgICAgIDEyICAgICAgICAxICAgMC43ODkgICAgMi4xZS0wNSBzZWMuCnQANk1ldGEtaGV1cmlzdGljOiBzZWxlY3RpbmcgbWV0aG9kIFRTIHdpdGggc2NvcmU6IDguMjA4CnQAKVRpbWUgdG8gY29tcHV0ZSB2YXJpYWJsZSBvcmRlcjogMC4wMDE5NjEKdAABCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT0gU1RBUlQgRklSSU5HIFJVTEVTIEVOQ09ESU5HID09PT09PT09PT09PT09PT09PT09PT09PT0KdAArRW5jb2RlZCA2IHRyYW5zaXRpb24gaW4gMSBwcmlvcml0eSBncm91cHMuCnQAIVRpbWUgdG8gYnVpbGQgYWxsIE5TRnM6IDAuMDAwNDk2CnQAAQp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09IFJFQUNIQUJJTElUWSBTRVQgR0VORVJBVElPTiA9PT09PT09PT09PT09PT09PT09PT09PT09CnQAFVNwbGl0OiBTcGxpdFN1YnRyYWN0CnQAHVJTIGdlbmVyYXRpb24gdGltZTogMC4wMDAyNDcKdAAdQ29tcHV0aW5nIHZhcmlhYmxlIGJvdW5kcy4uLgp0AAEKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0gTUVNT1JZID09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0ACkgVG90YWwgTWVtb3J5IFVzZWQ6ICAgICAgIDM5MjUyNCBLQnl0ZXMuCnQAAQp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09IENUTCBFVkFMVUFUSU9OID09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAAQp0AFFQcm9jZXNzaW5nOiAobm90IEUgRiAobm90ICgobm90IChEb25lX1AgPSAxKSkgb3IgKG5vdCAoRG9uZV9RID0gMSkpKSkpICAtPiAgYm9vbAp0AA1FdmFsOiBEb25lX1AKdAAUICAgICAgMC4wMDAwOTIgc2VjLgp0ABNFdmFsOiAoRG9uZV9QID0gMSkKdAAeICAgICAgMC4wMDAxMDkgc2VjLiAgY2FyZCA9IDIKdAAZRXZhbDogKG5vdCAoRG9uZV9QID0gMSkpCnQAHiAgICAgIDAuMDAwMDYxIHNlYy4gIGNhcmQgPSA1CnQADUV2YWw6IERvbmVfUQp0ABQgICAgICAwLjAwMDAyNiBzZWMuCnQAE0V2YWw6IChEb25lX1EgPSAxKQp0AB4gICAgICAwLjAwMDAzNiBzZWMuICBjYXJkID0gMQp0ABlFdmFsOiAobm90IChEb25lX1EgPSAxKSkKdAAeICAgICAgMC4wMDAwMjkgc2VjLiAgY2FyZCA9IDYKdAAxRXZhbDogKChub3QgKERvbmVfUCA9IDEpKSBvciAobm90IChEb25lX1EgPSAxKSkpCnQAIyAgICAgIDAuMDAwMDI3IHNlYy4gIGNhcmQgPSA3IChSUykKdAA3RXZhbDogKG5vdCAoKG5vdCAoRG9uZV9QID0gMSkpIG9yIChub3QgKERvbmVfUSA9IDEpKSkpCnQAGyAgICAgIFtOT1QgVFJVRV0gIGNhcmQgPSAwCnQAO0V2YWw6IEUgRiAobm90ICgobm90IChEb25lX1AgPSAxKSkgb3IgKG5vdCAoRG9uZV9RID0gMSkpKSkKdAAcICAgICAgW0UgRiBGQUxTRV0gIGNhcmQgPSAwCnQAQUV2YWw6IChub3QgRSBGIChub3QgKChub3QgKERvbmVfUCA9IDEpKSBvciAobm90IChEb25lX1EgPSAxKSkpKSkKdAAhICAgICAgW05PVCBGQUxTRV0gIGNhcmQgPSA3IChSUykKdAAvLS0tIEFHKCEoI0RvbmVfUCA9PSAxKSB8fCAhKCNEb25lX1EgPT0gMSkpIC0tLQp0ABlGb3JtdWxhIG5hbWU6IE1FQVNVUkUxICAKdAAWCUV2YWx1YXRpb246IHRydWUgICAgCnQAJwlTYXQtc2V0IGdlbmVyYXRpb24gdGltZTogMC4wMDA2OTUgc2VjCnQAHwlFdmFsdWF0aW9uIHRpbWU6IDAuMDAwNzA0IHNlYwp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0gQ1RMIE1FTU9SWSA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAHSBSUyBub2RlczogICAgICAgICAgICAgICAgMTEKdAA+IEZvcmVzdChSUykgbm9kZXM6ICAgICAgICAyNyBhY3RpdmVzLCAyNyBwZWFrLCAwIGNvbXBhY3Rpb25zLgp0ADkgRm9yZXN0KFJTKSBzaXplOiAgICAgICAgIDY4OSBCeXRlcyBub3csIDY4OSBCeXRlcyBwZWFrLgp0AB0gUG90ZW50aWFsIFJHIG5vZGVzOiAgICAgIDM5CnQAQCBGb3Jlc3QoUkcpIG5vZGVzOiAgICAgICAgMTI2IGFjdGl2ZXMsIDEyNiBwZWFrLCAwIGNvbXBhY3Rpb25zLgp0ADsgRm9yZXN0KFJHKSBzaXplOiAgICAgICAgIDM1MzggQnl0ZXMgbm93LCAzNTM4IEJ5dGVzIHBlYWsuCnQAPCBGb3Jlc3QoUkcrcmVhbCkgbm9kZXM6ICAgMiBhY3RpdmVzLCAyIHBlYWssIDAgY29tcGFjdGlvbnMuCnQANyBGb3Jlc3QoUkcrcmVhbCkgc2l6ZTogICAgNTQgQnl0ZXMgbm93LCA1NCBCeXRlcyBwZWFrLgp0AAEKdAABCnQAgVByb2Nlc3Npbmc6IChub3QgRSBGIChub3QgKChub3QgKChBd2FpdF9QID0gMSkgb3IgKEF3YWl0X1EgPSAxKSkpIG9yIChub3QgRSBHIChub3QgKChEb25lX1AgPSAxKSBvciAoRG9uZV9RID0gMSkpKSkpKSkgIC0+ICBib29sCnQADkV2YWw6IEF3YWl0X1AKdAAUICAgICAgMC4wMDAwMDggc2VjLgp0ABRFdmFsOiAoQXdhaXRfUCA9IDEpCnQAHiAgICAgIDAuMDAwMDE5IHNlYy4gIGNhcmQgPSA1CnQADkV2YWw6IEF3YWl0X1EKdAAUICAgICAgMC4wMDAwMDUgc2VjLgp0ABRFdmFsOiAoQXdhaXRfUSA9IDEpCnQAHiAgICAgIDAuMDAwMDA4IHNlYy4gIGNhcmQgPSAzCnQAJ0V2YWw6ICgoQXdhaXRfUCA9IDEpIG9yIChBd2FpdF9RID0gMSkpCnQAHiAgICAgIDAuMDAwMDA5IHNlYy4gIGNhcmQgPSA2CnQALUV2YWw6IChub3QgKChBd2FpdF9QID0gMSkgb3IgKEF3YWl0X1EgPSAxKSkpCnQAHiAgICAgIDAuMDAwMDExIHNlYy4gIGNhcmQgPSAxCnQADUV2YWw6IERvbmVfUAp0ABQgICAgICAwLjAwMDAwNCBzZWMuCnQAE0V2YWw6IChEb25lX1AgPSAxKQp0AB4gICAgICAwLjAwMDAwNiBzZWMuICBjYXJkID0gMgp0AA1FdmFsOiBEb25lX1EKdAAUICAgICAgMC4wMDAwMDQgc2VjLgp0ABNFdmFsOiAoRG9uZV9RID0gMSkKdAAeICAgICAgMC4wMDAwMDYgc2VjLiAgY2FyZCA9IDEKdAAlRXZhbDogKChEb25lX1AgPSAxKSBvciAoRG9uZV9RID0gMSkpCnQAHiAgICAgIDAuMDAwMDA5IHNlYy4gIGNhcmQgPSAzCnQAK0V2YWw6IChub3QgKChEb25lX1AgPSAxKSBvciAoRG9uZV9RID0gMSkpKQp0AB4gICAgICAwLjAwMDAwOCBzZWMuICBjYXJkID0gNAp0AC9FdmFsOiBFIEcgKG5vdCAoKERvbmVfUCA9IDEpIG9yIChEb25lX1EgPSAxKSkpCnQAH0VHOiBzdGVwPTEsICBTQVQgc2l6ZT00LjAwMDAwMAp0ABlSMiA9IDIzIGluIDEgaXRlcmF0aW9ucy4KdAAeICAgICAgMC4wMDAwODUgc2VjLiAgY2FyZCA9IDQKdAA1RXZhbDogKG5vdCBFIEcgKG5vdCAoKERvbmVfUCA9IDEpIG9yIChEb25lX1EgPSAxKSkpKQp0AB4gICAgICAwLjAwMDAwOSBzZWMuICBjYXJkID0gMwp0AGFFdmFsOiAoKG5vdCAoKEF3YWl0X1AgPSAxKSBvciAoQXdhaXRfUSA9IDEpKSkgb3IgKG5vdCBFIEcgKG5vdCAoKERvbmVfUCA9IDEpIG9yIChEb25lX1EgPSAxKSkpKSkKdAAeICAgICAgMC4wMDAwMTMgc2VjLiAgY2FyZCA9IDMKdABnRXZhbDogKG5vdCAoKG5vdCAoKEF3YWl0X1AgPSAxKSBvciAoQXdhaXRfUSA9IDEpKSkgb3IgKG5vdCBFIEcgKG5vdCAoKERvbmVfUCA9IDEpIG9yIChEb25lX1EgPSAxKSkpKSkpCnQAHiAgICAgIDAuMDAwMDEyIHNlYy4gIGNhcmQgPSA0CnQAa0V2YWw6IEUgRiAobm90ICgobm90ICgoQXdhaXRfUCA9IDEpIG9yIChBd2FpdF9RID0gMSkpKSBvciAobm90IEUgRyAobm90ICgoRG9uZV9QID0gMSkgb3IgKERvbmVfUSA9IDEpKSkpKSkKdAAuICAgICAgMyBzdGVwczogICAgICAgMC4wMDAwNTUgc2VjLiAgY2FyZCA9IDE1CnQAcUV2YWw6IChub3QgRSBGIChub3QgKChub3QgKChBd2FpdF9QID0gMSkgb3IgKEF3YWl0X1EgPSAxKSkpIG9yIChub3QgRSBHIChub3QgKChEb25lX1AgPSAxKSBvciAoRG9uZV9RID0gMSkpKSkpKSkKdAAeICAgICAgMC4wMDAwMTggc2VjLiAgY2FyZCA9IDAKdABRLS0tIEFHICgoI0F3YWl0X1A9PTEgfHwgI0F3YWl0X1EgPT0gMSkgLT4gQUYgKCNEb25lX1AgPT0gMSB8fCAjRG9uZV9RID09IDEpKSAtLS0KdAAZRm9ybXVsYSBuYW1lOiBNRUFTVVJFMiAgCnQAFglFdmFsdWF0aW9uOiBmYWxzZSAgIAp0ACcJU2F0LXNldCBnZW5lcmF0aW9uIHRpbWU6IDAuMDAwNDQxIHNlYwp0AB8JRXZhbHVhdGlvbiB0aW1lOiAwLjAwMDQ0MyBzZWMKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09IENUTCBNRU1PUlkgPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0AB0gUlMgbm9kZXM6ICAgICAgICAgICAgICAgIDExCnQAPiBGb3Jlc3QoUlMpIG5vZGVzOiAgICAgICAgNDYgYWN0aXZlcywgNDYgcGVhaywgMCBjb21wYWN0aW9ucy4KdAA7IEZvcmVzdChSUykgc2l6ZTogICAgICAgICAxMTg2IEJ5dGVzIG5vdywgMTE4NiBCeXRlcyBwZWFrLgp0AB0gUG90ZW50aWFsIFJHIG5vZGVzOiAgICAgIDM5CnQAQCBGb3Jlc3QoUkcpIG5vZGVzOiAgICAgICAgMTI2IGFjdGl2ZXMsIDEyNiBwZWFrLCAwIGNvbXBhY3Rpb25zLgp0ADsgRm9yZXN0KFJHKSBzaXplOiAgICAgICAgIDM1MzggQnl0ZXMgbm93LCAzNTM4IEJ5dGVzIHBlYWsuCnQAPCBGb3Jlc3QoUkcrcmVhbCkgbm9kZXM6ICAgNCBhY3RpdmVzLCA0IHBlYWssIDAgY29tcGFjdGlvbnMuCnQAOSBGb3Jlc3QoUkcrcmVhbCkgc2l6ZTogICAgMTA4IEJ5dGVzIG5vdywgMTA4IEJ5dGVzIHBlYWsuCnQAAQp0AAEKdABcUHJvY2Vzc2luZzogKG5vdCBFIEYgKG5vdCAoKG5vdCAoQXdhaXRfUCA9IDEpKSBvciAobm90IEUgRyAobm90IChEb25lX1AgPSAxKSkpKSkpICAtPiAgYm9vbAp0AA5FdmFsOiBBd2FpdF9QCnQAFCAgICAgIDAuMDAwMDA1IHNlYy4KdAAURXZhbDogKEF3YWl0X1AgPSAxKQp0AB4gICAgICAwLjAwMDAwNyBzZWMuICBjYXJkID0gNQp0ABpFdmFsOiAobm90IChBd2FpdF9QID0gMSkpCnQAHiAgICAgIDAuMDAwMDA3IHNlYy4gIGNhcmQgPSAyCnQADUV2YWw6IERvbmVfUAp0ABQgICAgICAwLjAwMDAwNSBzZWMuCnQAE0V2YWw6IChEb25lX1AgPSAxKQp0AB4gICAgICAwLjAwMDAwNiBzZWMuICBjYXJkID0gMgp0ABlFdmFsOiAobm90IChEb25lX1AgPSAxKSkKdAAeICAgICAgMC4wMDAwMDQgc2VjLiAgY2FyZCA9IDUKdAAdRXZhbDogRSBHIChub3QgKERvbmVfUCA9IDEpKQp0AB9FRzogc3RlcD0xLCAgU0FUIHNpemU9NS4wMDAwMDAKdAAZUjIgPSAyNCBpbiAxIGl0ZXJhdGlvbnMuCnQAHiAgICAgIDAuMDAwMDQ2IHNlYy4gIGNhcmQgPSA1CnQAI0V2YWw6IChub3QgRSBHIChub3QgKERvbmVfUCA9IDEpKSkKdAAeICAgICAgMC4wMDAwMDYgc2VjLiAgY2FyZCA9IDIKdAA8RXZhbDogKChub3QgKEF3YWl0X1AgPSAxKSkgb3IgKG5vdCBFIEcgKG5vdCAoRG9uZV9QID0gMSkpKSkKdAAeICAgICAgMC4wMDAwMDcgc2VjLiAgY2FyZCA9IDIKdABCRXZhbDogKG5vdCAoKG5vdCAoQXdhaXRfUCA9IDEpKSBvciAobm90IEUgRyAobm90IChEb25lX1AgPSAxKSkpKSkKdAAeICAgICAgMC4wMDAwMTAgc2VjLiAgY2FyZCA9IDUKdABGRXZhbDogRSBGIChub3QgKChub3QgKEF3YWl0X1AgPSAxKSkgb3IgKG5vdCBFIEcgKG5vdCAoRG9uZV9QID0gMSkpKSkpCnQALiAgICAgIDMgc3RlcHM6ICAgICAgIDAuMDAwMDI3IHNlYy4gIGNhcmQgPSAxNQp0AExFdmFsOiAobm90IEUgRiAobm90ICgobm90IChBd2FpdF9QID0gMSkpIG9yIChub3QgRSBHIChub3QgKERvbmVfUCA9IDEpKSkpKSkKdAAeICAgICAgMC4wMDAwMDcgc2VjLiAgY2FyZCA9IDAKdAAxLS0tIEFHICgoI0F3YWl0X1A9PTEgKSAtPiBBRiAoI0RvbmVfUCA9PSAxKSkgLS0tCnQAGUZvcm11bGEgbmFtZTogTUVBU1VSRTMgIAp0ABYJRXZhbHVhdGlvbjogZmFsc2UgICAKdAAnCVNhdC1zZXQgZ2VuZXJhdGlvbiB0aW1lOiAwLjAwMDIxNSBzZWMKdAAfCUV2YWx1YXRpb24gdGltZTogMC4wMDAyMTYgc2VjCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PSBDVEwgTUVNT1JZID09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAAdIFJTIG5vZGVzOiAgICAgICAgICAgICAgICAxMQp0AD4gRm9yZXN0KFJTKSBub2RlczogICAgICAgIDQ5IGFjdGl2ZXMsIDQ5IHBlYWssIDAgY29tcGFjdGlvbnMuCnQAOyBGb3Jlc3QoUlMpIHNpemU6ICAgICAgICAgMTI2NyBCeXRlcyBub3csIDEyNjcgQnl0ZXMgcGVhay4KdAAdIFBvdGVudGlhbCBSRyBub2RlczogICAgICAzOQp0AEAgRm9yZXN0KFJHKSBub2RlczogICAgICAgIDEyNiBhY3RpdmVzLCAxMjYgcGVhaywgMCBjb21wYWN0aW9ucy4KdAA7IEZvcmVzdChSRykgc2l6ZTogICAgICAgICAzNTM4IEJ5dGVzIG5vdywgMzUzOCBCeXRlcyBwZWFrLgp0ADwgRm9yZXN0KFJHK3JlYWwpIG5vZGVzOiAgIDQgYWN0aXZlcywgNCBwZWFrLCAwIGNvbXBhY3Rpb25zLgp0ADkgRm9yZXN0KFJHK3JlYWwpIHNpemU6ICAgIDEwOCBCeXRlcyBub3csIDEwOCBCeXRlcyBwZWFrLgp0AAEKdAABCnQAXFByb2Nlc3Npbmc6IChub3QgRSBGIChub3QgKChub3QgKEF3YWl0X1EgPSAxKSkgb3IgKG5vdCBFIEcgKG5vdCAoRG9uZV9RID0gMSkpKSkpKSAgLT4gIGJvb2wKdAAORXZhbDogQXdhaXRfUQp0ABQgICAgICAwLjAwMDAwNyBzZWMuCnQAFEV2YWw6IChBd2FpdF9RID0gMSkKdAAeICAgICAgMC4wMDAwMDYgc2VjLiAgY2FyZCA9IDMKdAAaRXZhbDogKG5vdCAoQXdhaXRfUSA9IDEpKQp0AB4gICAgICAwLjAwMDAwNyBzZWMuICBjYXJkID0gNAp0AA1FdmFsOiBEb25lX1EKdAAUICAgICAgMC4wMDAwMDUgc2VjLgp0ABNFdmFsOiAoRG9uZV9RID0gMSkKdAAeICAgICAgMC4wMDAwMDYgc2VjLiAgY2FyZCA9IDEKdAAZRXZhbDogKG5vdCAoRG9uZV9RID0gMSkpCnQAHiAgICAgIDAuMDAwMDA1IHNlYy4gIGNhcmQgPSA2CnQAHUV2YWw6IEUgRyAobm90IChEb25lX1EgPSAxKSkKdAAfRUc6IHN0ZXA9MSwgIFNBVCBzaXplPTYuMDAwMDAwCnQAGVIyID0gMTMgaW4gMSBpdGVyYXRpb25zLgp0AB4gICAgICAwLjAwMDAyMiBzZWMuICBjYXJkID0gNgp0ACNFdmFsOiAobm90IEUgRyAobm90IChEb25lX1EgPSAxKSkpCnQAHiAgICAgIDAuMDAwMDEwIHNlYy4gIGNhcmQgPSAxCnQAPEV2YWw6ICgobm90IChBd2FpdF9RID0gMSkpIG9yIChub3QgRSBHIChub3QgKERvbmVfUSA9IDEpKSkpCnQAHiAgICAgIDAuMDAwMDA5IHNlYy4gIGNhcmQgPSA0CnQAQkV2YWw6IChub3QgKChub3QgKEF3YWl0X1EgPSAxKSkgb3IgKG5vdCBFIEcgKG5vdCAoRG9uZV9RID0gMSkpKSkpCnQAHiAgICAgIDAuMDAwMDA4IHNlYy4gIGNhcmQgPSAzCnQARkV2YWw6IEUgRiAobm90ICgobm90IChBd2FpdF9RID0gMSkpIG9yIChub3QgRSBHIChub3QgKERvbmVfUSA9IDEpKSkpKQp0AC0gICAgICAzIHN0ZXBzOiAgICAgICAwLjAwMDAyOSBzZWMuICBjYXJkID0gNwp0AExFdmFsOiAobm90IEUgRiAobm90ICgobm90IChBd2FpdF9RID0gMSkpIG9yIChub3QgRSBHIChub3QgKERvbmVfUSA9IDEpKSkpKSkKdAAeICAgICAgMC4wMDAwMDggc2VjLiAgY2FyZCA9IDQKdAAxLS0tIEFHICgoI0F3YWl0X1E9PTEgKSAtPiBBRiAoI0RvbmVfUSA9PSAxKSkgLS0tCnQAGUZvcm11bGEgbmFtZTogTUVBU1VSRTQgIAp0ABYJRXZhbHVhdGlvbjogZmFsc2UgICAKdAAnCVNhdC1zZXQgZ2VuZXJhdGlvbiB0aW1lOiAwLjAwMDIwNSBzZWMKdAAfCUV2YWx1YXRpb24gdGltZTogMC4wMDAyMDcgc2VjCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PSBDVEwgTUVNT1JZID09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAAdIFJTIG5vZGVzOiAgICAgICAgICAgICAgICAxMQp0AD4gRm9yZXN0KFJTKSBub2RlczogICAgICAgIDUzIGFjdGl2ZXMsIDUzIHBlYWssIDAgY29tcGFjdGlvbnMuCnQAOyBGb3Jlc3QoUlMpIHNpemU6ICAgICAgICAgMTM3MSBCeXRlcyBub3csIDEzNzEgQnl0ZXMgcGVhay4KdAAdIFBvdGVudGlhbCBSRyBub2RlczogICAgICAzOQp0AEAgRm9yZXN0KFJHKSBub2RlczogICAgICAgIDEyNiBhY3RpdmVzLCAxMjYgcGVhaywgMCBjb21wYWN0aW9ucy4KdAA7IEZvcmVzdChSRykgc2l6ZTogICAgICAgICAzNTM4IEJ5dGVzIG5vdywgMzUzOCBCeXRlcyBwZWFrLgp0ADwgRm9yZXN0KFJHK3JlYWwpIG5vZGVzOiAgIDQgYWN0aXZlcywgNCBwZWFrLCAwIGNvbXBhY3Rpb25zLgp0ADkgRm9yZXN0KFJHK3JlYWwpIHNpemU6ICAgIDEwOCBCeXRlcyBub3csIDEwOCBCeXRlcyBwZWFrLgp0AAEKdAAET2suCnQAAQp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0gVElNRSA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAJSBWYXJpYWJsZSBvcmRlciBUaW1lOiAwLjAwMyAgICAgc2VjLgp0ACUgTlNGIGdlbi4gVGltZTogICAgICAgMC4wMDEgICAgIHNlYy4KdAAlIFJTIEdlbmVyYXRpb24gVGltZTogIDAuMDAwICAgICBzZWMuCnQAJSBUb3RhbCBSUyBUaW1lOiAgICAgICAwLjAwMSAgICAgc2VjLgp0ACUgU3RhdGlzdGljcyBUaW1lOiAgICAgMC4wMDAgICAgIHNlYy4KdAAlIENUTCBUaW1lOiAgICAgICAgICAgIDAuMDAyICAgICBzZWMuCnQAJSBUb3RhbCBUaW1lOiAgICAgICAgICAwLjAwNyAgICAgc2VjLgp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnEAfgAkeHNxAH4AAHcEAAABMnNyABFqYXZhLmxhbmcuQm9vbGVhbs0gcoDVnPruAgABWgAFdmFsdWV4cAFxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0cQB+ATRxAH4BNHEAfgE0eA + + diff --git a/anno3/vpc/consegne/3/3.5.jpg b/anno3/vpc/consegne/3/3.5.jpg new file mode 100644 index 0000000..e563bb1 Binary files /dev/null and b/anno3/vpc/consegne/3/3.5.jpg differ diff --git a/anno3/vpc/consegne/3/3.5.smv b/anno3/vpc/consegne/3/3.5.smv new file mode 100644 index 0000000..8079229 --- /dev/null +++ b/anno3/vpc/consegne/3/3.5.smv @@ -0,0 +1,40 @@ +MODULE main +VAR + turn: 1..2; + p: proc(turn, 1); + q: proc(turn, 2); +ASSIGN + init(turn) := 1; + next(turn) := case + p.state = done: 2; + q.state = done: 1; + TRUE: turn; + esac; + +CTLSPEC -- no mutual exclusion + AG (p.state != done | q.state != done) + +CTLSPEC -- no deadlock + AG ((p.state = await | q.state = await) -> AF (p.state = done | q.state = done)) + +CTLSPEC -- no individual starvation + AG (p.state = await -> AF p.state = done) +CTLSPEC + AG (q.state = await -> AF q.state = done) + +CTLSPEC -- prova: path senza starvation + AG (q.state = await -> EF q.state = done) + + + + +MODULE proc(turn, id) +VAR + state: {await, done}; +ASSIGN + init(state) := await; + next(state) := case + turn = id: {await, done}; + state = await: await; + state = done: await; + esac; \ No newline at end of file diff --git a/anno3/vpc/consegne/3/3.6.smv b/anno3/vpc/consegne/3/3.6.smv new file mode 100644 index 0000000..8c6aaba --- /dev/null +++ b/anno3/vpc/consegne/3/3.6.smv @@ -0,0 +1,52 @@ +MODULE main +VAR + wantP: boolean; + wantQ: boolean; + p: proc(wantP, wantQ); + q: proc(wantQ, wantP); +ASSIGN + init(wantP) := FALSE; + init(wantQ) := FALSE; + + next(wantP) := case + p.state = setTrue: TRUE; + p.state = setFalse: FALSE; + TRUE: wantP; + esac; + next(wantQ) := case + q.state = setTrue: TRUE; + q.state = setFalse: FALSE; + TRUE: wantQ; + esac; + +CTLSPEC -- no mutual exclusion + AG (p.state != critical | q.state != critical) + +CTLSPEC -- no deadlock + AG ((p.state = await | q.state = await) -> AF (p.state = critical | q.state = critical)) + +CTLSPEC -- no individual starvation + AG (p.state = await -> AF p.state = critical) +CTLSPEC + AG (q.state = await -> AF q.state = critical) + +CTLSPEC -- prova: path senza starvation + AG (q.state = await -> EF q.state = critical) + +CTLSPEC + EF(p.state = await -> AG(!(p.state = critical))) + + +MODULE proc(mine, other) +VAR + state: {local, await, critical, setTrue, setFalse}; +ASSIGN + init(state) := local; + next(state) := case + state = local: {local, await}; + state = await & other = FALSE: setTrue; + state = await: await; + state = setTrue: critical; + state = critical: setFalse; + state = setFalse: local; + esac; \ No newline at end of file diff --git a/anno3/vpc/consegne/3/analisi.org b/anno3/vpc/consegne/3/analisi.org index b27a700..2e53900 100644 --- a/anno3/vpc/consegne/3/analisi.org +++ b/anno3/vpc/consegne/3/analisi.org @@ -1,8 +1,34 @@ -* TODO [1/4] +# SCHELETRO: + +# * Algoritmo 3.5 +# Due processi iterano all'infinito seguendo questo pseudocodice + +# #+BEGIN_SRC +# #+END_SRC + +# ** NuSMV +# Si e` deciso di modellare l'algoritmo usando per ognuno dei due +# processi ... +# | CODE +# #+include 3.2.b.smv + +# ** GreatSPN +# ** TODO CCS +# ** Risultati + +Nella tabella mostriamo i risultati ottenuti +| | NuSMV | GreatSPN | +|---------------------+-------+----------| +| Mutua Esclusione | | | +| Assenza di deadlock | | | +| No Starvation | | | +* TODO [1/7] - [X] Cosa significa FAIRNESS running alla fine dei .smv -- [ ] Completa tabelle e immagine con greatspn - [ ] Riformula liveness - [ ] chiedi a lei di safety, liveness, fairness +- [ ] Vedi necessita` di Sync e / +- [ ] Finisci tutto con algebra dei processi +- [ ] Reachability graph vs Derivation Graph * TODO Proprieta` del modello @@ -42,14 +68,23 @@ while true: Si e` deciso di modellare l'algoritmo usando per ognuno dei due processi un'enumerazione di 4 stati ed una variabile turno di tipo intero. | state: {begin, wait, critical, done}; - #+include 3.2.b.smv +** GreatSPN +Il codice utilizzato per le proprieta` CTL e` il seguente: +#+BEGIN_SRC +AG(!(#Critical_P == 1) || !(#Critical_Q == 1)) = true +AG ((#Wait_P==1 || \#Critical_Q == 1) -> AF (#Critical_P == 1 || \#Critical_Q == 1)) = false +AG (#Wait_P==1 -> AF (#Critical_P == 1)) = false +#+END_SRC +[[./3.2.jpg]] +** TODO CCS +** Risultati Nella tabella mostriamo i risultati ottenuti | | NuSMV | GreatSPN | |---------------------+-------+----------| -| Mutua Esclusione | True | | -| Assenza di deadlock | True | | -| No Starvation | False | | +| Mutua Esclusione | True | True | +| Assenza di deadlock | False | False | +| No Starvation | False | False | Il risultato della possibilita` di deadlock non deve stupire: la specifica non obbliga un processo a terminare la fase begin. @@ -70,8 +105,118 @@ Trace Type: Counterexample -> State: 1.2 <- q.state = wait -> State: 1.3 <- - #+END_SRC Si vede che il processo q rimane nella fase begin e p, dopo essere entrato nella regione critica una volta, rimane bloccato in begin. Lo stesso trace mostra la possibilita` di starvation del processo. +La rete modellata con GreatSPN ci conferma quanto visto con NuSMV. + +Prendiamo in considerazione la seguente formula CTL +| AG (wₚ -> EF cₚ) +Sia GreatSPN che NuSMV ci mostrano che il sistema modellato rispetta +questa proprieta`. Questo significa che un processo in attesa di +entrare nella sezione critica ha la possibilita` di compiere +progresso, ma solo nel caso in cui, come si intuisce dal controesempio +precedente, l'altro processo decida di entrare in attesa a sua volta. + +* Algoritmo 3.5 +Due processi iterano all'infinito seguendo questo pseudocodice + +#+BEGIN_SRC +while true: + await turn = ID + turn <- (ID%2)+1 +#+END_SRC + +** NuSMV +Si e` deciso di modellare l'algoritmo usando per ognuno dei due +processi un'enumerazione di due stati e un contatore di turni intero +| state: {await, done}; +#+include 3.5.b.smv + +** GreatSPN +Il codice utilizzato per le proprieta` CTL e` il seguente: +#+BEGIN_SRC +AG(!(#Await_P == 1) || !(#Await_Q == 1)) = true +AG ((#Wait_P==1 || \#AWait_Q == 1) -> AF (#Done_P == 1 || \#Done_Q == 1)) = false +AG (#Await_P==1 -> AF (#Done_P == 1)) = false +#+END_SRC +[[./3.5.jpg]] +** TODO CCS +** Risultati +Nella tabella mostriamo i risultati ottenuti +| | NuSMV | GreatSPN | +|---------------------+-------+----------| +| Mutua Esclusione | true | true | +| Assenza di deadlock | false | false | +| No Starvation | false | false | +I risultati confermano il fatto che questo algoritmo e` solamente una +versione semplificata del precedente (/begin/ e /wait/ sono stati fusi +in await e /done/ rimosso) e pertanto il trace di controesempio +fornito da NuSMV e da GreatSPN presentano riflettono i risultati di +questa semplificazione. +- Possibilita` di deadlock: + #+BEGIN_SRC + – specification AG ((p.state = await | q.state = await) -> AF (p.state = done | q.state = done)) is false + – as demonstrated by the following execution sequence + Trace Description: CTL Counterexample + Trace Type: Counterexample + – Loop starts here + -> State: 1.1 <- + turn = 1 + p.state = await + q.state = await + -> State: 1.2 <- + #+END_SRC +- Possibilita` di starvation: i processi non compiono progresso + iterando infinite volte su /await/. + #+BEGIN_SRC + – specification AG (p.state = await -> AF p.state = done) is false + – as demonstrated by the following execution sequence + Trace Description: CTL Counterexample + Trace Type: Counterexample + – Loop starts here + -> State: 2.1 <- + turn = 1 + p.state = await + q.state = await + -> State: 2.2 <- + #+END_SRC + #+BEGIN_SRC + – specification AG (q.state = await -> AF q.state = done) is false + – as demonstrated by the following execution sequence + Trace Description: CTL Counterexample + Trace Type: Counterexample + – Loop starts here + -> State: 3.1 <- + turn = 1 + p.state = await + q.state = await + -> State: 3.2 <- + – specification AG (q.state = await -> EF q.state = done) is true + #+END_SRC +- Possibilita` di compiere progresso: + #+BEGIN_SRC + specification AG (q.state = await -> EF q.state = done) is true + #+END_SRC + +* Algoritmo 3.6 +Due processi iterano all'infinito seguendo questo pseudocodice +#+BEGIN_SRC +while true: + non-critical section + await wantQ = false + wantP <- true + critical section + wantP <- false +#+END_SRC + +** NuSMV +Si e` deciso di modellare l'algoritmo usando per ognuno dei due +processi ... +| CODE +#+include 3.6.smv + +** GreatSPN +** TODO CCS +** Risultati