diff --git a/anno3/vpc/consegne/3/3.6.PNPRO b/anno3/vpc/consegne/3/3.6.PNPRO index f12252b..b3c23d3 100644 --- a/anno3/vpc/consegne/3/3.6.PNPRO +++ b/anno3/vpc/consegne/3/3.6.PNPRO @@ -92,7 +92,7 @@ - + @@ -125,9 +125,16 @@ + + + + + + + - rO0ABXNyABRqYXZhLnV0aWwuTGlua2VkTGlzdAwpU11KYIgiAwAAeHB3BAAAAKh0AJMbWzBtRVhFQzogL3Vzci9sb2NhbC9HcmVhdFNQTi9iaW4vRFNQTi1Ub29sIC1sb2FkICIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuNi1NZWFzdXJlcy5zb2x1dGlvbi9QVCIgLXBiYXNpcyAtZGV0ZWN0LWV4cCAtcHNmbCAtYm5kIAp0AHAbWzFtG1s0bUxPQURJTkcgUEVUUkkgTkVUIC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy42LU1lYXN1cmVzLnNvbHV0aW9uL1BUIChuZXQvZGVmKS4uLhtbMjJtG1syNG0KdAAPTUFSS0lORyBQQVI6IDAKdAAQUExBQ0VTOiAgICAgIDE0CnQAD1JBVEUgUEFSOiAgICAwCnQAEFRSQU5TSVRJT05TOiAxMgp0AA9NRUFTVVJFUzogICAgMAp0AChMT0FESU5HIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAABCnQAAQp0AB5DT01QVVRJTkcgUExBQ0UgRkxPVyBCQVNJUy4uLgp0ABJNPTEyLCBOPTE0LCBOMD0xNAp0ADlDb21wdXRhdGlvbiBvZiBGbG93IGJhc2lzOiBzdGVwIDEvMTIsIHxLfD0xMiwgcHJvZHVjdHM9MQp0AFMbWzFBICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgCnQAUhtbMUFDb21wdXRhdGlvbiBvZiBGbG93IGJhc2lzOiBjb21wbGV0ZWQgaW4gOCBzdGVwcywgfEt8PTYuICAgICAgICAgICAgICAgICAgICAgIAp0AEBGT1VORCA2IFZFQ1RPUlMgSU4gVEhFIFBMQUNFIEZMT1cgQkFTSVMgKDQgc2VtaWZsb3dzLCAyIGZsb3dzKS4KdAABCnQAAQp0ACdBbGwgcGxhY2VzIGFyZSBjb3ZlcmVkIGJ5IHNvbWUgUC1mbG93Lgp0AAEKdAAmVE9UQUwgVElNRTogW1VzZXIgMC4wMDBzLCBTeXMgMC4wMDBzXQp0ACdBVk9JRCBFWFBPTkVOVElBTCBHUk9XVEggT0YgU0VNSUZMT1dTLgp0AB1DT01QVVRJTkcgUExBQ0UgU0VNSUZMT1dTLi4uCnQAEk09MTIsIE49MTQsIE4wPTE0CnQAK0dlbmVyYXRpb24gb2YgU2VtaWZsb3dzOiBzdGVwIDEvMTIsIHxLfD0xMgp0AFMbWzFBICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgCnQAUBtbMUFHZW5lcmF0aW9uIG9mIFNlbWlmbG93czogY29tcGxldGVkIGluIDggc3RlcHMsIHxLfD04LiAgICAgICAgICAgICAgICAgICAgICAKdAAZRk9VTkQgOCBQTEFDRSBTRU1JRkxPV1MuCnQAAQp0AAEKdAArQWxsIHBsYWNlcyBhcmUgY292ZXJlZCBieSBzb21lIFAtc2VtaWZsb3cuCnQAAQp0ACZUT1RBTCBUSU1FOiBbVXNlciAwLjAwMHMsIFN5cyAwLjAwMHNdCnQALENPTVBVVElORyBQTEFDRSBCT1VORFMgRlJPTSBQLVNFTUlGTE9XUyAuLi4KdAAnG1swWBtbMzJtIFBST0NFU1MgRVhJVEVEIE5PUk1BTExZLhtbMG0KdACkG1swbUVYRUM6IHBlcmwgLWUgJ2FsYXJtIDUgOyBleGVjICIvdXNyL2xvY2FsL0dyZWF0U1BOL2Jpbi9EU1BOLVRvb2wgLWxvYWQgXCIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuNi1NZWFzdXJlcy5zb2x1dGlvbi9QVFwiIC1sb2FkLWJuZCAtaWxwLWJuZCIgJwp0AHAbWzFtG1s0bUxPQURJTkcgUEVUUkkgTkVUIC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy42LU1lYXN1cmVzLnNvbHV0aW9uL1BUIChuZXQvZGVmKS4uLhtbMjJtG1syNG0KdAAPTUFSS0lORyBQQVI6IDAKdAAQUExBQ0VTOiAgICAgIDE0CnQAD1JBVEUgUEFSOiAgICAwCnQAEFRSQU5TSVRJT05TOiAxMgp0AA9NRUFTVVJFUzogICAgMAp0AChMT0FESU5HIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAABCnQAAQp0ABVMT0FESU5HIEJORCBGSUxFIC4uLgp0ACVDT01QVVRJTkcgUExBQ0UgQk9VTkRTIFVTSU5HIElMUCAuLi4KdAAYQWxsIHBsYWNlcyBhcmUgYm91bmRlZC4KcQB+ACR0AHUbWzBtRVhFQzogL3Vzci9sb2NhbC9HcmVhdFNQTi9iaW4vUkdNRUREMyAiL2hvbWUvdXNlci9VTklUTy9hbm5vMy92cGMvY29uc2VnbmUvMy8zLjYtTWVhc3VyZXMuc29sdXRpb24vUFQiIC1NRVRBICAtQwp0ACBSYW5kb20gc2VlZHM6IDE1ODg5MzI5NDkgMjA0NTYzCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAARR3JlYXRTUE4vTWVkZGx5Lgp0ADggIENvcHlyaWdodCAoQykgMTk4Ny0yMDE4LCBVbml2ZXJzaXR5IG9mIFRvcmlubywgSXRhbHkuCnQAMSAgU2VuZCBmaWxlcyBuZXRuYW1lLm5ldCwgLmRlZiB0byBlLW1haWwgYWRkcmVzcwp0ACsgIGJlY2N1dGlAZGkudW5pdG8uaXQgaWYgeW91IGZpbmQgYW55IGJ1Zy4KdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0AB9CYXNlZCBvbiBNRURETFkgdmVyc2lvbiAwLjE2LjAKdABGICBDb3B5cmlnaHQgKEMpIDIwMDksIElvd2EgU3RhdGUgVW5pdmVyc2l0eSBSZXNlYXJjaCBGb3VuZGF0aW9uLCBJbmMuCnQAKSAgd2Vic2l0ZTogaHR0cDovL21lZGRseS5zb3VyY2Vmb3JnZS5uZXQKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0AClVc2luZyBwZXItZXZlbnQgc2F0dXJhdGlvbiAoc2F0LXByZWdlbikuCnQAG1VzaW5nIGZhc3QgTlNGIGdlbmVyYXRpb24uCnQAElByb2Nlc3MgSUQ6IDMxODg4CnQAS01PREVMIE5BTUU6IC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy42LU1lYXN1cmVzLnNvbHV0aW9uL1BUCnQAHSAgMTQgcGxhY2VzLCAxMiB0cmFuc2l0aW9ucy4KdAAnVXNlZCBNZW1vcnkgZm9yIGVuY29kaW5nIG5ldDogMzU1ODQ4S0IKdABVT3BlbmluZyBmaWxlOiAvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuNi1NZWFzdXJlcy5zb2x1dGlvbi9QVC5ibmQgT0suCnQAWE9wZW5pbmcgZmlsZTogL2hvbWUvdXNlci9VTklUTy9hbm5vMy92cGMvY29uc2VnbmUvMy8zLjYtTWVhc3VyZXMuc29sdXRpb24vUFQuaWxwYm5kIE9LLgp0ABBJTlBVVCBBUkNTOiAgMTQKdAAQT1VUUFVUIEFSQ1M6IDE0CnQAD0lOSElCIEFSQ1M6ICAwCnQAD1RFU1QgQVJDUzogICA0CnQAEFBMQUNFUzogICAgICAxNAp0ABBUUkFOU0lUSU9OUzogMTIKdAAPSU5WQVJJQU5UUzogIDYKdAAPUC1TRU1JRkxPV1M6IDgKdAAWTUFYIElOVkFSSUFOVCBDQVJEOiAxCnQAAQp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09IFZBUklBQkxFIE9SREVSID09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAPFZhcmlhYmxlIG9yZGVyIG1ldGhvZDogTWV0YS1oZXVyaXN0aWMgdXNpbmcgd2VpZ2h0ZWQgc2NvcmUuCnQAUSAgTUVUSE9EICAgICAgICAgICAgICBTQ09SRSAgICAgICAgU1dJUiAgICAgICBTT1VQUyBESVNDT1VOVCAgV0VJR0hUICAgICAgIFRJTUUgCnQAVSAgU0xPICAgICAgICAgICAgICAgIDEwNi41OSAgICAgICAgICA5NSAgICAgICAgICA1MSAgICAgICAgMSAgIDEuMTIyICAgMC4wMDAxMjcgc2VjLgp0AFUgIFNMTytGb3JjZSAgICAgICAgICAgNTYuMzIgICAgICAgICAgNjQgICAgICAgICAgNDUgICAgICAgIDEgICAgMC44OCAgICA2LjFlLTA1IHNlYy4KdABVICBTTE8tMTYgICAgICAgICAgICAgIDc1LjgxICAgICAgICAgIDk1ICAgICAgICAgIDUxICAgICAgICAxICAgMC43OTggICAgNi4yZS0wNSBzZWMuCnQAVSAgU0xPLTE2K0ZvcmNlICAgICAgIDU4LjMwNCAgICAgICAgICA2NCAgICAgICAgICA0NSAgICAgICAgMSAgIDAuOTExICAgIDQuOGUtMDUgc2VjLgp0AFUgIFRPVjIgICAgICAgICAgICAgICA1MC45MDQgICAgICAgICAgNTYgICAgICAgICAgNDIgICAgICAgIDEgICAwLjkwOSAgICAzLjllLTA1IHNlYy4KdABVICBUT1YyK0ZvcmNlICAgICAgICAgNjEuMzc0ICAgICAgICAgIDUzICAgICAgICAgIDQyICAgICAgICAxICAgMS4xNTggICAgICA1ZS0wNSBzZWMuCnQAVSAgTk9BQ0syICAgICAgICAgICAgMTQ1Ljg5OSAgICAgICAgIDEyOSAgICAgICAgICA1OSAgICAgICAgMSAgIDEuMTMxICAgIDMuNmUtMDUgc2VjLgp0AFUgIE5PQUNLMitGb3JjZSAgICAgICAgNDEuMTYgICAgICAgICAgNDIgICAgICAgICAgMzkgICAgICAgIDEgICAgMC45OCAgICA1LjllLTA1IHNlYy4KdABVICBBQ00gICAgICAgICAgICAgICAxMDQuMTMzICAgICAgICAgMTAzICAgICAgICAgIDU0ICAgICAgICAxICAgMS4wMTEgICAgNi40ZS0wNSBzZWMuCnQAVSAgQUNNK0ZvcmNlICAgICAgICAgIDYxLjM0NCAgICAgICAgICA0OCAgICAgICAgICA0MSAgICAgICAgMSAgIDEuMjc4ICAgIDQuN2UtMDUgc2VjLgp0AFUgIENNMiAgICAgICAgICAgICAgICAgMTA3LjEgICAgICAgICAgODQgICAgICAgICAgNDkgICAgICAgIDEgICAxLjI3NSAgICAzLjJlLTA1IHNlYy4KdABVICBDTTIrRm9yY2UgICAgICAgICAgNTIuNzUyICAgICAgICAgIDQ4ICAgICAgICAgIDQxICAgICAgICAxICAgMS4wOTkgICAgNC43ZS0wNSBzZWMuCnQAVSAgUCAgICAgICAgICAgICAgICAgMTMzLjIyMyAgICAgICAgIDEyNyAgICAgICAgICA2NiAgICAgICAgMSAgIDEuMDQ5ICAgICAgM2UtMDUgc2VjLgp0AFUgIEdQICAgICAgICAgICAgICAgICAxMDQuNjcgICAgICAgICAgOTAgICAgICAgICAgNTIgICAgICAgIDEgICAxLjE2MyAgICA4LjVlLTA1IHNlYy4KdABVICBHUCtGb3JjZSAgICAgICAgICAgNTUuMTI1ICAgICAgICAgIDQ5ICAgICAgICAgIDM5ICAgICAgICAxICAgMS4xMjUgICAgNS40ZS0wNSBzZWMuCnQAQE1ldGEtaGV1cmlzdGljOiBzZWxlY3RpbmcgbWV0aG9kIE5PQUNLMitGb3JjZSB3aXRoIHNjb3JlOiA0MS4xNgp0AClUaW1lIHRvIGNvbXB1dGUgdmFyaWFibGUgb3JkZXI6IDAuMDAxMzExCnQAAQp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09IFNUQVJUIEZJUklORyBSVUxFUyBFTkNPRElORyA9PT09PT09PT09PT09PT09PT09PT09PT09CnQALEVuY29kZWQgMTIgdHJhbnNpdGlvbiBpbiAxIHByaW9yaXR5IGdyb3Vwcy4KdAAgVGltZSB0byBidWlsZCBhbGwgTlNGczogMC4wMDA2OQp0AAEKdABQPT09PT09PT09PT09PT09PT09PT09PT09PSBSRUFDSEFCSUxJVFkgU0VUIEdFTkVSQVRJT04gPT09PT09PT09PT09PT09PT09PT09PT09PQp0ABVTcGxpdDogU3BsaXRTdWJ0cmFjdAp0AB1SUyBnZW5lcmF0aW9uIHRpbWU6IDAuMDAwMTk1CnQAHUNvbXB1dGluZyB2YXJpYWJsZSBib3VuZHMuLi4KdAABCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09IE1FTU9SWSA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAApIFRvdGFsIE1lbW9yeSBVc2VkOiAgICAgICAzNTU4NDggS0J5dGVzLgp0AAEKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PSBDVEwgRVZBTFVBVElPTiA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0AAEKdABgUHJvY2Vzc2luZzogKG5vdCBFIEYgKG5vdCAoKG5vdCAoYXdhaXRfUCA9IDEpKSBvciAobm90IEUgRyAobm90IChjcml0aWNhbF9QID0gMSkpKSkpKSAgLT4gIGJvb2wKdAAORXZhbDogYXdhaXRfUAp0ABQgICAgICAwLjAwMDAyMiBzZWMuCnQAFEV2YWw6IChhd2FpdF9QID0gMSkKdAAeICAgICAgMC4wMDAwMzIgc2VjLiAgY2FyZCA9IDUKdAAaRXZhbDogKG5vdCAoYXdhaXRfUCA9IDEpKQp0AB8gICAgICAwLjAwMDAxNCBzZWMuICBjYXJkID0gMjAKdAARRXZhbDogY3JpdGljYWxfUAp0ABQgICAgICAwLjAwMDAwNSBzZWMuCnQAF0V2YWw6IChjcml0aWNhbF9QID0gMSkKdAAeICAgICAgMC4wMDAwMDkgc2VjLiAgY2FyZCA9IDUKdAAdRXZhbDogKG5vdCAoY3JpdGljYWxfUCA9IDEpKQp0AB8gICAgICAwLjAwMDAwNSBzZWMuICBjYXJkID0gMjAKdAAhRXZhbDogRSBHIChub3QgKGNyaXRpY2FsX1AgPSAxKSkKdAAgRUc6IHN0ZXA9MSwgIFNBVCBzaXplPTIwLjAwMDAwMAp0ABlSMiA9IDU4IGluIDEgaXRlcmF0aW9ucy4KdAAfICAgICAgMC4wMDAxMDggc2VjLiAgY2FyZCA9IDIwCnQAJ0V2YWw6IChub3QgRSBHIChub3QgKGNyaXRpY2FsX1AgPSAxKSkpCnQAHiAgICAgIDAuMDAwMDA2IHNlYy4gIGNhcmQgPSA1CnQAQEV2YWw6ICgobm90IChhd2FpdF9QID0gMSkpIG9yIChub3QgRSBHIChub3QgKGNyaXRpY2FsX1AgPSAxKSkpKQp0AB8gICAgICAwLjAwMDAwNyBzZWMuICBjYXJkID0gMjAKdABGRXZhbDogKG5vdCAoKG5vdCAoYXdhaXRfUCA9IDEpKSBvciAobm90IEUgRyAobm90IChjcml0aWNhbF9QID0gMSkpKSkpCnQAHiAgICAgIDAuMDAwMDM2IHNlYy4gIGNhcmQgPSA1CnQASkV2YWw6IEUgRiAobm90ICgobm90IChhd2FpdF9QID0gMSkpIG9yIChub3QgRSBHIChub3QgKGNyaXRpY2FsX1AgPSAxKSkpKSkKdAAzICAgICAgNCBzdGVwczogICAgICAgMC4wMDAwNTkgc2VjLiAgY2FyZCA9IDI1IChSUykKdABQRXZhbDogKG5vdCBFIEYgKG5vdCAoKG5vdCAoYXdhaXRfUCA9IDEpKSBvciAobm90IEUgRyAobm90IChjcml0aWNhbF9QID0gMSkpKSkpKQp0ABsgICAgICBbTk9UIFRSVUVdICBjYXJkID0gMAp0ADItLS0gQUcgKCNhd2FpdF9QPT0xIC0+IEFGICgjY3JpdGljYWxfUCA9PSAxKSkgLS0tCnQAGUZvcm11bGEgbmFtZTogTUVBU1VSRTAgIAp0ABYJRXZhbHVhdGlvbjogZmFsc2UgICAKdAAmCVNhdC1zZXQgZ2VuZXJhdGlvbiB0aW1lOiAwLjAwMDQ4IHNlYwp0AB8JRXZhbHVhdGlvbiB0aW1lOiAwLjAwMDQ4MiBzZWMKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09IENUTCBNRU1PUlkgPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0AB0gUlMgbm9kZXM6ICAgICAgICAgICAgICAgIDI3CnQAPiBGb3Jlc3QoUlMpIG5vZGVzOiAgICAgICAgODcgYWN0aXZlcywgODcgcGVhaywgMCBjb21wYWN0aW9ucy4KdAA7IEZvcmVzdChSUykgc2l6ZTogICAgICAgICAyMTY5IEJ5dGVzIG5vdywgMjE2OSBCeXRlcyBwZWFrLgp0AB0gUG90ZW50aWFsIFJHIG5vZGVzOiAgICAgIDg4CnQAQCBGb3Jlc3QoUkcpIG5vZGVzOiAgICAgICAgMzc3IGFjdGl2ZXMsIDM3NyBwZWFrLCAwIGNvbXBhY3Rpb25zLgp0AD0gRm9yZXN0KFJHKSBzaXplOiAgICAgICAgIDEwODExIEJ5dGVzIG5vdywgMTA4MTEgQnl0ZXMgcGVhay4KdAA8IEZvcmVzdChSRytyZWFsKSBub2RlczogICAyIGFjdGl2ZXMsIDIgcGVhaywgMCBjb21wYWN0aW9ucy4KdAA3IEZvcmVzdChSRytyZWFsKSBzaXplOiAgICA1NCBCeXRlcyBub3csIDU0IEJ5dGVzIHBlYWsuCnQAAQp0AARPay4KdAABCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PSBUSU1FID09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAAlIFZhcmlhYmxlIG9yZGVyIFRpbWU6IDAuMDAyICAgICBzZWMuCnQAJSBOU0YgZ2VuLiBUaW1lOiAgICAgICAwLjAwMSAgICAgc2VjLgp0ACUgUlMgR2VuZXJhdGlvbiBUaW1lOiAgMC4wMDAgICAgIHNlYy4KdAAlIFRvdGFsIFJTIFRpbWU6ICAgICAgIDAuMDAxICAgICBzZWMuCnQAJSBTdGF0aXN0aWNzIFRpbWU6ICAgICAwLjAwMCAgICAgc2VjLgp0ACUgQ1RMIFRpbWU6ICAgICAgICAgICAgMC4wMDEgICAgIHNlYy4KdAAlIFRvdGFsIFRpbWU6ICAgICAgICAgIDAuMDA1ICAgICBzZWMuCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KcQB+ACR4c3EAfgAAdwQAAACoc3IAEWphdmEubGFuZy5Cb29sZWFuzSBygNWc+u4CAAFaAAV2YWx1ZXhwAXEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKpxAH4AqnEAfgCqcQB+AKp4 + rO0ABXNyABRqYXZhLnV0aWwuTGlua2VkTGlzdAwpU11KYIgiAwAAeHB3BAAAAK50AJMbWzBtRVhFQzogL3Vzci9sb2NhbC9HcmVhdFNQTi9iaW4vRFNQTi1Ub29sIC1sb2FkICIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuNi1NZWFzdXJlcy5zb2x1dGlvbi9QVCIgLXBiYXNpcyAtZGV0ZWN0LWV4cCAtcHNmbCAtYm5kIAp0AHAbWzFtG1s0bUxPQURJTkcgUEVUUkkgTkVUIC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy42LU1lYXN1cmVzLnNvbHV0aW9uL1BUIChuZXQvZGVmKS4uLhtbMjJtG1syNG0KdAAPTUFSS0lORyBQQVI6IDAKdAAQUExBQ0VTOiAgICAgIDE0CnQAD1JBVEUgUEFSOiAgICAwCnQAEFRSQU5TSVRJT05TOiAxMgp0AA9NRUFTVVJFUzogICAgMAp0AChMT0FESU5HIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAABCnQAAQp0AB5DT01QVVRJTkcgUExBQ0UgRkxPVyBCQVNJUy4uLgp0ABJNPTEyLCBOPTE0LCBOMD0xNAp0ADlDb21wdXRhdGlvbiBvZiBGbG93IGJhc2lzOiBzdGVwIDEvMTIsIHxLfD0xMiwgcHJvZHVjdHM9MQp0AFMbWzFBICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgCnQAUhtbMUFDb21wdXRhdGlvbiBvZiBGbG93IGJhc2lzOiBjb21wbGV0ZWQgaW4gOCBzdGVwcywgfEt8PTYuICAgICAgICAgICAgICAgICAgICAgIAp0AEBGT1VORCA2IFZFQ1RPUlMgSU4gVEhFIFBMQUNFIEZMT1cgQkFTSVMgKDQgc2VtaWZsb3dzLCAyIGZsb3dzKS4KdAABCnQAAQp0ACdBbGwgcGxhY2VzIGFyZSBjb3ZlcmVkIGJ5IHNvbWUgUC1mbG93Lgp0AAEKdAAmVE9UQUwgVElNRTogW1VzZXIgMC4wMDBzLCBTeXMgMC4wMDBzXQp0ACdBVk9JRCBFWFBPTkVOVElBTCBHUk9XVEggT0YgU0VNSUZMT1dTLgp0AB1DT01QVVRJTkcgUExBQ0UgU0VNSUZMT1dTLi4uCnQAEk09MTIsIE49MTQsIE4wPTE0CnQAK0dlbmVyYXRpb24gb2YgU2VtaWZsb3dzOiBzdGVwIDEvMTIsIHxLfD0xMgp0AFMbWzFBICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgCnQAUBtbMUFHZW5lcmF0aW9uIG9mIFNlbWlmbG93czogY29tcGxldGVkIGluIDggc3RlcHMsIHxLfD04LiAgICAgICAgICAgICAgICAgICAgICAKdAAZRk9VTkQgOCBQTEFDRSBTRU1JRkxPV1MuCnQAAQp0AAEKdAArQWxsIHBsYWNlcyBhcmUgY292ZXJlZCBieSBzb21lIFAtc2VtaWZsb3cuCnQAAQp0ACZUT1RBTCBUSU1FOiBbVXNlciAwLjAwMHMsIFN5cyAwLjAwMHNdCnQALENPTVBVVElORyBQTEFDRSBCT1VORFMgRlJPTSBQLVNFTUlGTE9XUyAuLi4KdAAnG1swWBtbMzJtIFBST0NFU1MgRVhJVEVEIE5PUk1BTExZLhtbMG0KdACkG1swbUVYRUM6IHBlcmwgLWUgJ2FsYXJtIDUgOyBleGVjICIvdXNyL2xvY2FsL0dyZWF0U1BOL2Jpbi9EU1BOLVRvb2wgLWxvYWQgXCIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuNi1NZWFzdXJlcy5zb2x1dGlvbi9QVFwiIC1sb2FkLWJuZCAtaWxwLWJuZCIgJwp0AHAbWzFtG1s0bUxPQURJTkcgUEVUUkkgTkVUIC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy42LU1lYXN1cmVzLnNvbHV0aW9uL1BUIChuZXQvZGVmKS4uLhtbMjJtG1syNG0KdAAPTUFSS0lORyBQQVI6IDAKdAAQUExBQ0VTOiAgICAgIDE0CnQAD1JBVEUgUEFSOiAgICAwCnQAEFRSQU5TSVRJT05TOiAxMgp0AA9NRUFTVVJFUzogICAgMAp0AChMT0FESU5HIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAABCnQAAQp0ABVMT0FESU5HIEJORCBGSUxFIC4uLgp0ACVDT01QVVRJTkcgUExBQ0UgQk9VTkRTIFVTSU5HIElMUCAuLi4KdAAYQWxsIHBsYWNlcyBhcmUgYm91bmRlZC4KcQB+ACR0AHgbWzBtRVhFQzogL3Vzci9sb2NhbC9HcmVhdFNQTi9iaW4vUkdNRUREMyAiL2hvbWUvdXNlci9VTklUTy9hbm5vMy92cGMvY29uc2VnbmUvMy8zLjYtTWVhc3VyZXMuc29sdXRpb24vUFQiIC1NRVRBICAtYyAtQwp0ACBSYW5kb20gc2VlZHM6IDE1ODg5NDQwOTggNjcwMTUwCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAARR3JlYXRTUE4vTWVkZGx5Lgp0ADggIENvcHlyaWdodCAoQykgMTk4Ny0yMDE4LCBVbml2ZXJzaXR5IG9mIFRvcmlubywgSXRhbHkuCnQAMSAgU2VuZCBmaWxlcyBuZXRuYW1lLm5ldCwgLmRlZiB0byBlLW1haWwgYWRkcmVzcwp0ACsgIGJlY2N1dGlAZGkudW5pdG8uaXQgaWYgeW91IGZpbmQgYW55IGJ1Zy4KdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0AB9CYXNlZCBvbiBNRURETFkgdmVyc2lvbiAwLjE2LjAKdABGICBDb3B5cmlnaHQgKEMpIDIwMDksIElvd2EgU3RhdGUgVW5pdmVyc2l0eSBSZXNlYXJjaCBGb3VuZGF0aW9uLCBJbmMuCnQAKSAgd2Vic2l0ZTogaHR0cDovL21lZGRseS5zb3VyY2Vmb3JnZS5uZXQKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0AClVc2luZyBwZXItZXZlbnQgc2F0dXJhdGlvbiAoc2F0LXByZWdlbikuCnQAG1VzaW5nIGZhc3QgTlNGIGdlbmVyYXRpb24uCnQAEVByb2Nlc3MgSUQ6IDgxOTIKdABLTU9ERUwgTkFNRTogL2hvbWUvdXNlci9VTklUTy9hbm5vMy92cGMvY29uc2VnbmUvMy8zLjYtTWVhc3VyZXMuc29sdXRpb24vUFQKdAAdICAxNCBwbGFjZXMsIDEyIHRyYW5zaXRpb25zLgp0ACdVc2VkIE1lbW9yeSBmb3IgZW5jb2RpbmcgbmV0OiAzODEzMzZLQgp0AFVPcGVuaW5nIGZpbGU6IC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy42LU1lYXN1cmVzLnNvbHV0aW9uL1BULmJuZCBPSy4KdABYT3BlbmluZyBmaWxlOiAvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuNi1NZWFzdXJlcy5zb2x1dGlvbi9QVC5pbHBibmQgT0suCnQAEElOUFVUIEFSQ1M6ICAxNAp0ABBPVVRQVVQgQVJDUzogMTQKdAAPSU5ISUIgQVJDUzogIDAKdAAPVEVTVCBBUkNTOiAgIDQKdAAQUExBQ0VTOiAgICAgIDE0CnQAEFRSQU5TSVRJT05TOiAxMgp0AA9JTlZBUklBTlRTOiAgNgp0AA9QLVNFTUlGTE9XUzogOAp0ABZNQVggSU5WQVJJQU5UIENBUkQ6IDEKdAABCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0gVkFSSUFCTEUgT1JERVIgPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAA8VmFyaWFibGUgb3JkZXIgbWV0aG9kOiBNZXRhLWhldXJpc3RpYyB1c2luZyB3ZWlnaHRlZCBzY29yZS4KdABRICBNRVRIT0QgICAgICAgICAgICAgIFNDT1JFICAgICAgICBTV0lSICAgICAgIFNPVVBTIERJU0NPVU5UICBXRUlHSFQgICAgICAgVElNRSAKdABVICBTTE8gICAgICAgICAgICAgICAgMTA2LjU5ICAgICAgICAgIDk1ICAgICAgICAgIDUxICAgICAgICAxICAgMS4xMjIgICAwLjAwMDMwNSBzZWMuCnQAVSAgU0xPK0ZvcmNlICAgICAgICAgICA1Ni4zMiAgICAgICAgICA2NCAgICAgICAgICA0NSAgICAgICAgMSAgICAwLjg4ICAgICAgOGUtMDUgc2VjLgp0AFUgIFNMTy0xNiAgICAgICAgICAgICAgNzUuODEgICAgICAgICAgOTUgICAgICAgICAgNTEgICAgICAgIDEgICAwLjc5OCAgIDAuMDAwMTQxIHNlYy4KdABVICBTTE8tMTYrRm9yY2UgICAgICAgNTguMzA0ICAgICAgICAgIDY0ICAgICAgICAgIDQ1ICAgICAgICAxICAgMC45MTEgICAgNS4zZS0wNSBzZWMuCnQAVSAgVE9WMiAgICAgICAgICAgICAgIDUwLjkwNCAgICAgICAgICA1NiAgICAgICAgICA0MiAgICAgICAgMSAgIDAuOTA5ICAgIDUuNWUtMDUgc2VjLgp0AFUgIFRPVjIrRm9yY2UgICAgICAgICA2MS4zNzQgICAgICAgICAgNTMgICAgICAgICAgNDIgICAgICAgIDEgICAxLjE1OCAgICAzLjllLTA1IHNlYy4KdABVICBOT0FDSzIgICAgICAgICAgICAxNDUuODk5ICAgICAgICAgMTI5ICAgICAgICAgIDU5ICAgICAgICAxICAgMS4xMzEgICAgMi45ZS0wNSBzZWMuCnQAVSAgTk9BQ0syK0ZvcmNlICAgICAgICA0MS4xNiAgICAgICAgICA0MiAgICAgICAgICAzOSAgICAgICAgMSAgICAwLjk4ICAgICAgNWUtMDUgc2VjLgp0AFUgIEFDTSAgICAgICAgICAgICAgIDEwNC4xMzMgICAgICAgICAxMDMgICAgICAgICAgNTQgICAgICAgIDEgICAxLjAxMSAgICA4LjRlLTA1IHNlYy4KdABVICBBQ00rRm9yY2UgICAgICAgICAgNjEuMzQ0ICAgICAgICAgIDQ4ICAgICAgICAgIDQxICAgICAgICAxICAgMS4yNzggICAgNC40ZS0wNSBzZWMuCnQAVSAgQ00yICAgICAgICAgICAgICAgICAxMDcuMSAgICAgICAgICA4NCAgICAgICAgICA0OSAgICAgICAgMSAgIDEuMjc1ICAgIDIuOGUtMDUgc2VjLgp0AFUgIENNMitGb3JjZSAgICAgICAgICA1Mi43NTIgICAgICAgICAgNDggICAgICAgICAgNDEgICAgICAgIDEgICAxLjA5OSAgICAgIDNlLTA1IHNlYy4KdABVICBQICAgICAgICAgICAgICAgICAxMzMuMjIzICAgICAgICAgMTI3ICAgICAgICAgIDY2ICAgICAgICAxICAgMS4wNDkgICAgMi4yZS0wNSBzZWMuCnQAVSAgR1AgICAgICAgICAgICAgICAgIDEwNC42NyAgICAgICAgICA5MCAgICAgICAgICA1MiAgICAgICAgMSAgIDEuMTYzICAgIDguN2UtMDUgc2VjLgp0AFUgIEdQK0ZvcmNlICAgICAgICAgICA1NS4xMjUgICAgICAgICAgNDkgICAgICAgICAgMzkgICAgICAgIDEgICAxLjEyNSAgICAzLjRlLTA1IHNlYy4KdABATWV0YS1oZXVyaXN0aWM6IHNlbGVjdGluZyBtZXRob2QgTk9BQ0syK0ZvcmNlIHdpdGggc2NvcmU6IDQxLjE2CnQAJ1RpbWUgdG8gY29tcHV0ZSB2YXJpYWJsZSBvcmRlcjogMC4wMDE5CnQAAQp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09IFNUQVJUIEZJUklORyBSVUxFUyBFTkNPRElORyA9PT09PT09PT09PT09PT09PT09PT09PT09CnQALEVuY29kZWQgMTIgdHJhbnNpdGlvbiBpbiAxIHByaW9yaXR5IGdyb3Vwcy4KdAAhVGltZSB0byBidWlsZCBhbGwgTlNGczogMC4wMDEwNTUKdAABCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT0gUkVBQ0hBQklMSVRZIFNFVCBHRU5FUkFUSU9OID09PT09PT09PT09PT09PT09PT09PT09PT0KdAAVU3BsaXQ6IFNwbGl0U3VidHJhY3QKdAAdUlMgZ2VuZXJhdGlvbiB0aW1lOiAwLjAwMDEyOQp0AB1Db21wdXRpbmcgdmFyaWFibGUgYm91bmRzLi4uCnQAAQp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PSBNRU1PUlkgPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAKSBUb3RhbCBNZW1vcnkgVXNlZDogICAgICAgMzgxMzM2IEtCeXRlcy4KdAABCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0gQ1RMIEVWQUxVQVRJT04gPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAABCnQAR1Byb2Nlc3Npbmc6IChub3QgRSBGIChub3QgKG5vdCBFIEcgKG5vdCAoY3JpdGljYWxfUCA9IDEpKSkpKSAgLT4gIGJvb2wKdAARRXZhbDogY3JpdGljYWxfUAp0ABQgICAgICAwLjAwMDAyNSBzZWMuCnQAF0V2YWw6IChjcml0aWNhbF9QID0gMSkKdAAeICAgICAgMC4wMDAwMjMgc2VjLiAgY2FyZCA9IDUKdAAdRXZhbDogKG5vdCAoY3JpdGljYWxfUCA9IDEpKQp0AB8gICAgICAwLjAwMDAxNiBzZWMuICBjYXJkID0gMjAKdAAhRXZhbDogRSBHIChub3QgKGNyaXRpY2FsX1AgPSAxKSkKdAAgRUc6IHN0ZXA9MSwgIFNBVCBzaXplPTIwLjAwMDAwMAp0ABlSMiA9IDQ1IGluIDEgaXRlcmF0aW9ucy4KdAAfICAgICAgMC4wMDAwNzggc2VjLiAgY2FyZCA9IDIwCnQAJ0V2YWw6IChub3QgRSBHIChub3QgKGNyaXRpY2FsX1AgPSAxKSkpCnQAHiAgICAgIDAuMDAwMDA2IHNlYy4gIGNhcmQgPSA1CnQALUV2YWw6IChub3QgKG5vdCBFIEcgKG5vdCAoY3JpdGljYWxfUCA9IDEpKSkpCnQAHyAgICAgIDAuMDAwMDA0IHNlYy4gIGNhcmQgPSAyMAp0ADFFdmFsOiBFIEYgKG5vdCAobm90IEUgRyAobm90IChjcml0aWNhbF9QID0gMSkpKSkKdAAzICAgICAgMSBzdGVwczogICAgICAgMC4wMDAwMDkgc2VjLiAgY2FyZCA9IDI1IChSUykKdAA3RXZhbDogKG5vdCBFIEYgKG5vdCAobm90IEUgRyAobm90IChjcml0aWNhbF9QID0gMSkpKSkpCnQAGyAgICAgIFtOT1QgVFJVRV0gIGNhcmQgPSAwCnQAIS0tLSBBRyhBRigjY3JpdGljYWxfUCA9PSAxKSkgLS0tCnQAGUZvcm11bGEgbmFtZTogTUVBU1VSRTAgIAp0ABYJRXZhbHVhdGlvbjogZmFsc2UgICAKdAAnCVNhdC1zZXQgZ2VuZXJhdGlvbiB0aW1lOiAwLjAwMDI3MyBzZWMKdAAfCUV2YWx1YXRpb24gdGltZTogMC4wMDAyNzcgc2VjCnQAAQp0ABxHZW5lcmF0ZWQgY291bnRlci1leGFtcGxlOiAKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09IFRyYWNlID09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0AElJbml0aWFsIHN0YXRlIGlzOiBsb2NhbF9RKDEpLCB3YW50UV9GQUxTRSgxKSwgbG9jYWxfUCgxKSwgd2FudFBfRkFMU0UoMSkKdABGSW5pdGlhbCBzdGF0ZSBzYXRpc2ZpZXM6IEUgRiAobm90IChub3QgRSBHIChub3QgKGNyaXRpY2FsX1AgPSAxKSkpKS4gCnQAAQp0ADoxOiBsb2NhbF9RKDEpLCB3YW50UV9GQUxTRSgxKSwgbG9jYWxfUCgxKSwgd2FudFBfRkFMU0UoMSkKdABBICBTdGF0ZSAxLiBzYXRpc2ZpZXM6IEUgRyAobm90IChjcml0aWNhbF9QID0gMSkpLiBTdGFydCBvZiBsb29wLgp0AAEKdAA+ICAxLjE6IGxvY2FsX1EoMSksIHdhbnRRX0ZBTFNFKDEpLCBsb2NhbF9QKDEpLCB3YW50UF9GQUxTRSgxKQp0ADQgICAgU3RhdGUgMS4xLiBkb2VzIG5vdCBzYXRpc2Z5OiAoY3JpdGljYWxfUCA9IDEpLiAKdAABCnQAHyAgMS4yOiBsb29wIGJhY2sgdG8gc3RhdGUgMS4xLgp0AAEKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09IENUTCBNRU1PUlkgPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0AB0gUlMgbm9kZXM6ICAgICAgICAgICAgICAgIDI3CnQAPiBGb3Jlc3QoUlMpIG5vZGVzOiAgICAgICAgODAgYWN0aXZlcywgODAgcGVhaywgMCBjb21wYWN0aW9ucy4KdAA7IEZvcmVzdChSUykgc2l6ZTogICAgICAgICAxOTg4IEJ5dGVzIG5vdywgMTk4OCBCeXRlcyBwZWFrLgp0AB0gUG90ZW50aWFsIFJHIG5vZGVzOiAgICAgIDg4CnQAQCBGb3Jlc3QoUkcpIG5vZGVzOiAgICAgICAgMzc3IGFjdGl2ZXMsIDM3NyBwZWFrLCAwIGNvbXBhY3Rpb25zLgp0AD0gRm9yZXN0KFJHKSBzaXplOiAgICAgICAgIDEwODExIEJ5dGVzIG5vdywgMTA4MTEgQnl0ZXMgcGVhay4KdAA8IEZvcmVzdChSRytyZWFsKSBub2RlczogICAxIGFjdGl2ZXMsIDEgcGVhaywgMCBjb21wYWN0aW9ucy4KdAA3IEZvcmVzdChSRytyZWFsKSBzaXplOiAgICAyNyBCeXRlcyBub3csIDI3IEJ5dGVzIHBlYWsuCnQAAQp0AARPay4KdAABCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PSBUSU1FID09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAAlIFZhcmlhYmxlIG9yZGVyIFRpbWU6IDAuMDAyICAgICBzZWMuCnQAJSBOU0YgZ2VuLiBUaW1lOiAgICAgICAwLjAwMSAgICAgc2VjLgp0ACUgUlMgR2VuZXJhdGlvbiBUaW1lOiAgMC4wMDAgICAgIHNlYy4KdAAlIFRvdGFsIFJTIFRpbWU6ICAgICAgIDAuMDAxICAgICBzZWMuCnQAJSBTdGF0aXN0aWNzIFRpbWU6ICAgICAwLjAwMCAgICAgc2VjLgp0ACUgQ1RMIFRpbWU6ICAgICAgICAgICAgMC4wMDEgICAgIHNlYy4KdAAlIFRvdGFsIFRpbWU6ICAgICAgICAgIDAuMDA2ICAgICBzZWMuCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KcQB+ACR4c3EAfgAAdwQAAACuc3IAEWphdmEubGFuZy5Cb29sZWFuzSBygNWc+u4CAAFaAAV2YWx1ZXhwAXEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALBxAH4AsHEAfgCwcQB+ALB4 diff --git a/anno3/vpc/consegne/3/3.6.jpg b/anno3/vpc/consegne/3/3.6.jpg new file mode 100644 index 0000000..8549c0b Binary files /dev/null and b/anno3/vpc/consegne/3/3.6.jpg differ diff --git a/anno3/vpc/consegne/3/3.8-Measures.solution/PT.bnd b/anno3/vpc/consegne/3/3.8-Measures.solution/PT.bnd new file mode 100644 index 0000000..f845088 --- /dev/null +++ b/anno3/vpc/consegne/3/3.8-Measures.solution/PT.bnd @@ -0,0 +1,14 @@ +0 1 +0 1 +0 1 +0 1 +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.8-Measures.solution/PT.ctl b/anno3/vpc/consegne/3/3.8-Measures.solution/PT.ctl new file mode 100644 index 0000000..1aa033b --- /dev/null +++ b/anno3/vpc/consegne/3/3.8-Measures.solution/PT.ctl @@ -0,0 +1,2 @@ +% MEASURE0 +AG(#await_P == 1 -> EF(#critical_Q==1 || #critical_P == 1)) diff --git a/anno3/vpc/consegne/3/3.8-Measures.solution/PT.def b/anno3/vpc/consegne/3/3.8-Measures.solution/PT.def new file mode 100644 index 0000000..f9eee66 --- /dev/null +++ b/anno3/vpc/consegne/3/3.8-Measures.solution/PT.def @@ -0,0 +1,3 @@ +|256 +% +| diff --git a/anno3/vpc/consegne/3/3.8-Measures.solution/PT.ilpbnd b/anno3/vpc/consegne/3/3.8-Measures.solution/PT.ilpbnd new file mode 100644 index 0000000..aa47d0d --- /dev/null +++ b/anno3/vpc/consegne/3/3.8-Measures.solution/PT.ilpbnd @@ -0,0 +1,2 @@ +0 +0 diff --git a/anno3/vpc/consegne/3/3.8-Measures.solution/PT.net b/anno3/vpc/consegne/3/3.8-Measures.solution/PT.net new file mode 100644 index 0000000..7271b95 --- /dev/null +++ b/anno3/vpc/consegne/3/3.8-Measures.solution/PT.net @@ -0,0 +1,105 @@ +|0| +| +f 0 14 0 12 0 0 0 +local_P 1 3.0 1.3333333333333333 3.294583333333333 1.2789583333333334 0 +await_P 0 3.0 4.333333333333333 3.185208333333333 4.112291666666667 0 +SetTrue_P 0 3.0 2.6666666666666665 3.1904166666666662 2.6122916666666667 0 +critical_P 0 3.0 5.5 3.388333333333333 5.612291666666667 0 +setFalse_P 0 3.0 7.0 3.1904166666666662 7.028958333333333 0 +wantP_FALSE 1 4.5 7.0 4.049791666666667 7.195625 0 +wantP_TRUE 0 4.5 6.0 4.820625 5.862291666666667 0 +wantQ_FALSE 1 6.333333333333333 2.6666666666666665 6.127916666666667 2.9456249999999997 0 +wantQ_TRUE 0 7.5 2.6666666666666665 6.732083333333333 2.278958333333333 0 +setFalse_Q 0 8.666666666666666 2.5 8.851875 2.6956249999999997 0 +critical_Q 0 8.666666666666666 4.0 8.96125 4.195625 0 +setTrue_Q 0 8.666666666666666 6.666666666666667 9.028958333333334 6.695625 0 +await_Q 0 8.666666666666666 5.166666666666667 8.43 5.362291666666667 0 +local_Q 1 8.666666666666666 7.833333333333333 9.034166666666666 7.445625 0 +T0 1.0 0 0 1 0 3.0 2.0 2.9791666666666665 1.8072916666666667 3.0833333333333335 2.0677083333333335 0 + 1 1 0 0 + 1 + 1 3 0 0 + 0 +T8 1.0 0 0 2 0 3.0 7.833333333333333 2.9791666666666665 7.640625 3.0833333333333335 7.901041666666667 0 + 1 5 1 0 +3.0 7.583333333333333 + 1 7 0 0 + 2 + 1 1 2 0 +1.0833333333333333 7.833333333333333 +1.0833333333333333 1.3333333333333333 + 1 6 1 0 +5.5 7.833333333333333 + 0 +T3 1.0 0 0 1 0 3.0 6.166666666666667 2.9791666666666665 5.973958333333333 3.0833333333333335 6.234375 0 + 1 4 0 0 + 1 + 1 5 0 0 + 0 +T1 1.0 0 0 2 0 3.0 5.0 2.9791666666666665 4.807291666666667 3.0833333333333335 5.067708333333333 0 + 1 2 0 0 + 1 8 1 0 +5.166666666666667 4.166666666666667 + 2 + 1 8 1 0 +5.25 4.25 + 1 4 0 0 + 0 +T2 1.0 0 0 2 0 3.0 3.3333333333333335 2.9791666666666665 3.140625 3.0833333333333335 3.4010416666666665 0 + 1 3 0 0 + -1 6 1 0 +4.166666666666667 3.3333333333333335 + 2 + -1 7 1 0 +4.333333333333333 3.6666666666666665 + 1 2 0 0 + 0 +T00 1.0 0 0 1 0 1.6666666666666667 1.0 1.6197916666666667 0.8072916666666666 1.75 1.0677083333333333 0 + 1 1 1 0 +2.4166666666666665 0.9166666666666666 + 1 + 1 1 0 0 + 0 +T4 1.0 0 0 1 1 9.5 8.333333333333334 9.479166666666666 8.140625 9.583333333333334 8.401041666666666 0 + 1 14 0 0 + 1 + 1 14 1 0 +9.0 8.25 + 0 +T5 1.0 0 0 2 0 8.666666666666666 1.5 8.645833333333334 1.3072916666666667 8.75 1.5677083333333333 0 + 1 10 0 0 + 1 9 0 0 + 2 + 1 14 2 0 +10.333333333333334 1.5 +10.333333333333334 7.833333333333333 + 1 8 1 0 +6.333333333333333 1.5 + 0 +T6 1.0 0 0 1 0 8.666666666666666 7.166666666666667 8.645833333333334 6.973958333333333 8.75 7.234375 0 + 1 14 0 0 + 1 + 1 12 0 0 + 0 +T7 1.0 0 0 2 0 8.666666666666666 4.666666666666667 8.645833333333334 4.473958333333333 8.75 4.734375 0 + 1 13 0 0 + 1 6 0 0 + 2 + 1 6 1 0 +6.583333333333333 6.0 + 1 11 0 0 + 0 +T9 1.0 0 0 2 0 8.666666666666666 6.166666666666667 8.645833333333334 5.973958333333333 8.75 6.234375 0 + 1 12 0 0 + -1 8 1 0 +7.166666666666667 6.166666666666667 + 2 + -1 9 1 0 +6.75 6.75 + 1 13 0 0 + 0 +T10 1.0 0 0 1 0 8.666666666666666 3.1666666666666665 8.619791666666666 2.9739583333333335 8.75 3.234375 0 + 1 11 0 0 + 1 + 1 10 0 0 + 0 diff --git a/anno3/vpc/consegne/3/3.8-Measures.solution/PT.pba b/anno3/vpc/consegne/3/3.8-Measures.solution/PT.pba new file mode 100644 index 0000000..a33d892 --- /dev/null +++ b/anno3/vpc/consegne/3/3.8-Measures.solution/PT.pba @@ -0,0 +1,8 @@ +6 +5 1 1 1 2 1 3 1 4 1 5 +4 -1 2 -1 4 -1 5 1 7 +4 1 2 1 4 1 5 1 6 +5 1 10 1 11 1 12 1 13 1 14 +4 1 9 -1 10 -1 11 -1 13 +4 1 8 1 10 1 11 1 13 +0 diff --git a/anno3/vpc/consegne/3/3.8-Measures.solution/PT.pin b/anno3/vpc/consegne/3/3.8-Measures.solution/PT.pin new file mode 100644 index 0000000..e8276a8 --- /dev/null +++ b/anno3/vpc/consegne/3/3.8-Measures.solution/PT.pin @@ -0,0 +1,10 @@ +8 +5 1 10 1 11 1 12 1 13 1 14 +3 1 9 1 12 1 14 +4 1 8 1 10 1 11 1 13 +2 1 8 1 9 +5 1 1 1 2 1 3 1 4 1 5 +3 1 1 1 3 1 7 +4 1 2 1 4 1 5 1 6 +2 1 6 1 7 +0 diff --git a/anno3/vpc/consegne/3/3.8.PNPRO b/anno3/vpc/consegne/3/3.8.PNPRO new file mode 100644 index 0000000..c47158b --- /dev/null +++ b/anno3/vpc/consegne/3/3.8.PNPRO @@ -0,0 +1,122 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + rO0ABXNyABRqYXZhLnV0aWwuTGlua2VkTGlzdAwpU11KYIgiAwAAeHB3BAAAAM90AJMbWzBtRVhFQzogL3Vzci9sb2NhbC9HcmVhdFNQTi9iaW4vRFNQTi1Ub29sIC1sb2FkICIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuOC1NZWFzdXJlcy5zb2x1dGlvbi9QVCIgLXBiYXNpcyAtZGV0ZWN0LWV4cCAtcHNmbCAtYm5kIAp0AHAbWzFtG1s0bUxPQURJTkcgUEVUUkkgTkVUIC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy44LU1lYXN1cmVzLnNvbHV0aW9uL1BUIChuZXQvZGVmKS4uLhtbMjJtG1syNG0KdAAPTUFSS0lORyBQQVI6IDAKdAAQUExBQ0VTOiAgICAgIDE0CnQAD1JBVEUgUEFSOiAgICAwCnQAEFRSQU5TSVRJT05TOiAxMgp0AA9NRUFTVVJFUzogICAgMAp0AChMT0FESU5HIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAABCnQAAQp0AB5DT01QVVRJTkcgUExBQ0UgRkxPVyBCQVNJUy4uLgp0ABJNPTEyLCBOPTE0LCBOMD0xNAp0ADlDb21wdXRhdGlvbiBvZiBGbG93IGJhc2lzOiBzdGVwIDEvMTIsIHxLfD0xMiwgcHJvZHVjdHM9MQp0AFMbWzFBICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgCnQAUhtbMUFDb21wdXRhdGlvbiBvZiBGbG93IGJhc2lzOiBjb21wbGV0ZWQgaW4gOCBzdGVwcywgfEt8PTYuICAgICAgICAgICAgICAgICAgICAgIAp0AEBGT1VORCA2IFZFQ1RPUlMgSU4gVEhFIFBMQUNFIEZMT1cgQkFTSVMgKDQgc2VtaWZsb3dzLCAyIGZsb3dzKS4KdAABCnQAAQp0ACdBbGwgcGxhY2VzIGFyZSBjb3ZlcmVkIGJ5IHNvbWUgUC1mbG93Lgp0AAEKdAAmVE9UQUwgVElNRTogW1VzZXIgMC4wMDBzLCBTeXMgMC4wMDBzXQp0ACdBVk9JRCBFWFBPTkVOVElBTCBHUk9XVEggT0YgU0VNSUZMT1dTLgp0AB1DT01QVVRJTkcgUExBQ0UgU0VNSUZMT1dTLi4uCnQAEk09MTIsIE49MTQsIE4wPTE0CnQAK0dlbmVyYXRpb24gb2YgU2VtaWZsb3dzOiBzdGVwIDEvMTIsIHxLfD0xMgp0AFMbWzFBICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgCnQAUBtbMUFHZW5lcmF0aW9uIG9mIFNlbWlmbG93czogY29tcGxldGVkIGluIDggc3RlcHMsIHxLfD04LiAgICAgICAgICAgICAgICAgICAgICAKdAAZRk9VTkQgOCBQTEFDRSBTRU1JRkxPV1MuCnQAAQp0AAEKdAArQWxsIHBsYWNlcyBhcmUgY292ZXJlZCBieSBzb21lIFAtc2VtaWZsb3cuCnQAAQp0ACZUT1RBTCBUSU1FOiBbVXNlciAwLjAwMHMsIFN5cyAwLjAwMHNdCnQALENPTVBVVElORyBQTEFDRSBCT1VORFMgRlJPTSBQLVNFTUlGTE9XUyAuLi4KdAAnG1swWBtbMzJtIFBST0NFU1MgRVhJVEVEIE5PUk1BTExZLhtbMG0KdACkG1swbUVYRUM6IHBlcmwgLWUgJ2FsYXJtIDUgOyBleGVjICIvdXNyL2xvY2FsL0dyZWF0U1BOL2Jpbi9EU1BOLVRvb2wgLWxvYWQgXCIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuOC1NZWFzdXJlcy5zb2x1dGlvbi9QVFwiIC1sb2FkLWJuZCAtaWxwLWJuZCIgJwp0AHAbWzFtG1s0bUxPQURJTkcgUEVUUkkgTkVUIC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy44LU1lYXN1cmVzLnNvbHV0aW9uL1BUIChuZXQvZGVmKS4uLhtbMjJtG1syNG0KdAAPTUFSS0lORyBQQVI6IDAKdAAQUExBQ0VTOiAgICAgIDE0CnQAD1JBVEUgUEFSOiAgICAwCnQAEFRSQU5TSVRJT05TOiAxMgp0AA9NRUFTVVJFUzogICAgMAp0AChMT0FESU5HIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAABCnQAAQp0ABVMT0FESU5HIEJORCBGSUxFIC4uLgp0ACVDT01QVVRJTkcgUExBQ0UgQk9VTkRTIFVTSU5HIElMUCAuLi4KdAAYQWxsIHBsYWNlcyBhcmUgYm91bmRlZC4KcQB+ACR0AHgbWzBtRVhFQzogL3Vzci9sb2NhbC9HcmVhdFNQTi9iaW4vUkdNRUREMyAiL2hvbWUvdXNlci9VTklUTy9hbm5vMy92cGMvY29uc2VnbmUvMy8zLjgtTWVhc3VyZXMuc29sdXRpb24vUFQiIC1NRVRBICAtYyAtQwp0ACBSYW5kb20gc2VlZHM6IDE1ODg5NDc1NDkgNDI2NTA2CnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAARR3JlYXRTUE4vTWVkZGx5Lgp0ADggIENvcHlyaWdodCAoQykgMTk4Ny0yMDE4LCBVbml2ZXJzaXR5IG9mIFRvcmlubywgSXRhbHkuCnQAMSAgU2VuZCBmaWxlcyBuZXRuYW1lLm5ldCwgLmRlZiB0byBlLW1haWwgYWRkcmVzcwp0ACsgIGJlY2N1dGlAZGkudW5pdG8uaXQgaWYgeW91IGZpbmQgYW55IGJ1Zy4KdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0AB9CYXNlZCBvbiBNRURETFkgdmVyc2lvbiAwLjE2LjAKdABGICBDb3B5cmlnaHQgKEMpIDIwMDksIElvd2EgU3RhdGUgVW5pdmVyc2l0eSBSZXNlYXJjaCBGb3VuZGF0aW9uLCBJbmMuCnQAKSAgd2Vic2l0ZTogaHR0cDovL21lZGRseS5zb3VyY2Vmb3JnZS5uZXQKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0AClVc2luZyBwZXItZXZlbnQgc2F0dXJhdGlvbiAoc2F0LXByZWdlbikuCnQAG1VzaW5nIGZhc3QgTlNGIGdlbmVyYXRpb24uCnQAElByb2Nlc3MgSUQ6IDE0NDUxCnQAS01PREVMIE5BTUU6IC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy44LU1lYXN1cmVzLnNvbHV0aW9uL1BUCnQAHSAgMTQgcGxhY2VzLCAxMiB0cmFuc2l0aW9ucy4KdAAnVXNlZCBNZW1vcnkgZm9yIGVuY29kaW5nIG5ldDogMzk0NTY0S0IKdABVT3BlbmluZyBmaWxlOiAvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuOC1NZWFzdXJlcy5zb2x1dGlvbi9QVC5ibmQgT0suCnQAWE9wZW5pbmcgZmlsZTogL2hvbWUvdXNlci9VTklUTy9hbm5vMy92cGMvY29uc2VnbmUvMy8zLjgtTWVhc3VyZXMuc29sdXRpb24vUFQuaWxwYm5kIE9LLgp0ABBJTlBVVCBBUkNTOiAgMTQKdAAQT1VUUFVUIEFSQ1M6IDE0CnQAD0lOSElCIEFSQ1M6ICAwCnQAD1RFU1QgQVJDUzogICA0CnQAEFBMQUNFUzogICAgICAxNAp0ABBUUkFOU0lUSU9OUzogMTIKdAAPSU5WQVJJQU5UUzogIDYKdAAPUC1TRU1JRkxPV1M6IDgKdAAWTUFYIElOVkFSSUFOVCBDQVJEOiAxCnQAAQp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09IFZBUklBQkxFIE9SREVSID09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAPFZhcmlhYmxlIG9yZGVyIG1ldGhvZDogTWV0YS1oZXVyaXN0aWMgdXNpbmcgd2VpZ2h0ZWQgc2NvcmUuCnQAUSAgTUVUSE9EICAgICAgICAgICAgICBTQ09SRSAgICAgICAgU1dJUiAgICAgICBTT1VQUyBESVNDT1VOVCAgV0VJR0hUICAgICAgIFRJTUUgCnQAVSAgU0xPICAgICAgICAgICAgICAgICA2Ny4zMiAgICAgICAgICA2MCAgICAgICAgICA0MyAgICAgICAgMSAgIDEuMTIyICAgICAwLjAwMDMgc2VjLgp0AFUgIFNMTytGb3JjZSAgICAgICAgICAgNDMuMTIgICAgICAgICAgNDkgICAgICAgICAgNDIgICAgICAgIDEgICAgMC44OCAgICA2LjhlLTA1IHNlYy4KdABVICBTTE8tMTYgICAgICAgICAgICAgIDQ3Ljg4ICAgICAgICAgIDYwICAgICAgICAgIDQzICAgICAgICAxICAgMC43OTggICAgNy42ZS0wNSBzZWMuCnQAVSAgU0xPLTE2K0ZvcmNlICAgICAgIDQ0LjYzOSAgICAgICAgICA0OSAgICAgICAgICA0MiAgICAgICAgMSAgIDAuOTExICAgIDQuNmUtMDUgc2VjLgp0AFUgIFRPVjIgICAgICAgICAgICAgICA1NS40NDkgICAgICAgICAgNjEgICAgICAgICAgNDMgICAgICAgIDEgICAwLjkwOSAgICA1LjNlLTA1IHNlYy4KdABVICBUT1YyK0ZvcmNlICAgICAgICAgNTUuNTg0ICAgICAgICAgIDQ4ICAgICAgICAgIDQxICAgICAgICAxICAgMS4xNTggICAgNC41ZS0wNSBzZWMuCnQAVSAgTk9BQ0syICAgICAgICAgICAgMTc2LjQzNiAgICAgICAgIDE1NiAgICAgICAgICA2NyAgICAgICAgMSAgIDEuMTMxICAgIDMuMmUtMDUgc2VjLgp0AFUgIE5PQUNLMitGb3JjZSAgICAgICAgNDYuMDYgICAgICAgICAgNDcgICAgICAgICAgNDAgICAgICAgIDEgICAgMC45OCAgICA0LjNlLTA1IHNlYy4KdABVICBBQ00gICAgICAgICAgICAgICAgNjUuNzE1ICAgICAgICAgIDY1ICAgICAgICAgIDQ0ICAgICAgICAxICAgMS4wMTEgICAgNi43ZS0wNSBzZWMuCnQAVSAgQUNNK0ZvcmNlICAgICAgICAgIDcyLjg0NiAgICAgICAgICA1NyAgICAgICAgICA0MiAgICAgICAgMSAgIDEuMjc4ICAgIDMuMmUtMDUgc2VjLgp0AFUgIENNMiAgICAgICAgICAgICAgICA4Mi44NzUgICAgICAgICAgNjUgICAgICAgICAgNDQgICAgICAgIDEgICAxLjI3NSAgICAyLjNlLTA1IHNlYy4KdABVICBDTTIrRm9yY2UgICAgICAgICAgNjIuNjQzICAgICAgICAgIDU3ICAgICAgICAgIDQyICAgICAgICAxICAgMS4wOTkgICAgMi45ZS0wNSBzZWMuCnQAVSAgUCAgICAgICAgICAgICAgICAgMTE3LjQ4OCAgICAgICAgIDExMiAgICAgICAgICA1OSAgICAgICAgMSAgIDEuMDQ5ICAgIDIuNmUtMDUgc2VjLgp0AFUgIEdQICAgICAgICAgICAgICAgICA1MC4wMDkgICAgICAgICAgNDMgICAgICAgICAgMzcgICAgICAgIDEgICAxLjE2MyAgIDAuMDAwMTU0IHNlYy4KdABVICBHUCtGb3JjZSAgICAgICAgICAgICAgIDU0ICAgICAgICAgIDQ4ICAgICAgICAgIDM4ICAgICAgICAxICAgMS4xMjUgICAgNS40ZS0wNSBzZWMuCnQAPU1ldGEtaGV1cmlzdGljOiBzZWxlY3RpbmcgbWV0aG9kIFNMTytGb3JjZSB3aXRoIHNjb3JlOiA0My4xMgp0ACZUaW1lIHRvIGNvbXB1dGUgdmFyaWFibGUgb3JkZXI6IDAuMDAyCnQAAQp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09IFNUQVJUIEZJUklORyBSVUxFUyBFTkNPRElORyA9PT09PT09PT09PT09PT09PT09PT09PT09CnQALEVuY29kZWQgMTIgdHJhbnNpdGlvbiBpbiAxIHByaW9yaXR5IGdyb3Vwcy4KdAAhVGltZSB0byBidWlsZCBhbGwgTlNGczogMC4wMDA0MDIKdAABCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT0gUkVBQ0hBQklMSVRZIFNFVCBHRU5FUkFUSU9OID09PT09PT09PT09PT09PT09PT09PT09PT0KdAAVU3BsaXQ6IFNwbGl0U3VidHJhY3QKdAAdUlMgZ2VuZXJhdGlvbiB0aW1lOiAwLjAwMDEwNAp0AB1Db21wdXRpbmcgdmFyaWFibGUgYm91bmRzLi4uCnQAAQp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PSBNRU1PUlkgPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAKSBUb3RhbCBNZW1vcnkgVXNlZDogICAgICAgMzk0NTY0IEtCeXRlcy4KdAABCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0gQ1RMIEVWQUxVQVRJT04gPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAABCnQAalByb2Nlc3Npbmc6IChub3QgRSBGIChub3QgKChub3QgKGF3YWl0X1AgPSAxKSkgb3IgRSBGICgoY3JpdGljYWxfUSA9IDEpIG9yIChjcml0aWNhbF9QID0gMSkpKSkpICAtPiAgYm9vbAp0AA5FdmFsOiBhd2FpdF9QCnQAFCAgICAgIDAuMDAwMDE4IHNlYy4KdAAURXZhbDogKGF3YWl0X1AgPSAxKQp0AB4gICAgICAwLjAwMDAzMSBzZWMuICBjYXJkID0gNQp0ABpFdmFsOiAobm90IChhd2FpdF9QID0gMSkpCnQAHyAgICAgIDAuMDAwMDIwIHNlYy4gIGNhcmQgPSAxNgp0ABFFdmFsOiBjcml0aWNhbF9RCnQAFCAgICAgIDAuMDAwMDA1IHNlYy4KdAAXRXZhbDogKGNyaXRpY2FsX1EgPSAxKQp0AB4gICAgICAwLjAwMDAxNSBzZWMuICBjYXJkID0gMwp0ABFFdmFsOiBjcml0aWNhbF9QCnQAFCAgICAgIDAuMDAwMDA0IHNlYy4KdAAXRXZhbDogKGNyaXRpY2FsX1AgPSAxKQp0AB4gICAgICAwLjAwMDAxNyBzZWMuICBjYXJkID0gMwp0AC1FdmFsOiAoKGNyaXRpY2FsX1EgPSAxKSBvciAoY3JpdGljYWxfUCA9IDEpKQp0AB4gICAgICAwLjAwMDAxMSBzZWMuICBjYXJkID0gNgp0ADFFdmFsOiBFIEYgKChjcml0aWNhbF9RID0gMSkgb3IgKGNyaXRpY2FsX1AgPSAxKSkKdAAuICAgICAgNSBzdGVwczogICAgICAgMC4wMDAzNDUgc2VjLiAgY2FyZCA9IDI0CnQASkV2YWw6ICgobm90IChhd2FpdF9QID0gMSkpIG9yIEUgRiAoKGNyaXRpY2FsX1EgPSAxKSBvciAoY3JpdGljYWxfUCA9IDEpKSkKdAAfICAgICAgMC4wMDAwMTYgc2VjLiAgY2FyZCA9IDI0CnQAUEV2YWw6IChub3QgKChub3QgKGF3YWl0X1AgPSAxKSkgb3IgRSBGICgoY3JpdGljYWxfUSA9IDEpIG9yIChjcml0aWNhbF9QID0gMSkpKSkKdAAeICAgICAgMC4wMDAwMjAgc2VjLiAgY2FyZCA9IDEKdABURXZhbDogRSBGIChub3QgKChub3QgKGF3YWl0X1AgPSAxKSkgb3IgRSBGICgoY3JpdGljYWxfUSA9IDEpIG9yIChjcml0aWNhbF9QID0gMSkpKSkKdAAuICAgICAgOCBzdGVwczogICAgICAgMC4wMDAyOTEgc2VjLiAgY2FyZCA9IDI1CnQAWkV2YWw6IChub3QgRSBGIChub3QgKChub3QgKGF3YWl0X1AgPSAxKSkgb3IgRSBGICgoY3JpdGljYWxfUSA9IDEpIG9yIChjcml0aWNhbF9QID0gMSkpKSkpCnQAHiAgICAgIDAuMDAwMDExIHNlYy4gIGNhcmQgPSAwCnQARC0tLSBBRygjYXdhaXRfUCA9PSAxIC0+IEVGKCNjcml0aWNhbF9RPT0xIHx8ICNjcml0aWNhbF9QID09IDEpKSAtLS0KdAAZRm9ybXVsYSBuYW1lOiBNRUFTVVJFMCAgCnQAFglFdmFsdWF0aW9uOiBmYWxzZSAgIAp0ACcJU2F0LXNldCBnZW5lcmF0aW9uIHRpbWU6IDAuMDAwOTIzIHNlYwp0AB8JRXZhbHVhdGlvbiB0aW1lOiAwLjAwMDkyNCBzZWMKdAABCnQAHEdlbmVyYXRlZCBjb3VudGVyLWV4YW1wbGU6IAp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0gVHJhY2UgPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQASUluaXRpYWwgc3RhdGUgaXM6IGxvY2FsX1AoMSksIHdhbnRQX0ZBTFNFKDEpLCB3YW50UV9GQUxTRSgxKSwgbG9jYWxfUSgxKQp0AGlJbml0aWFsIHN0YXRlIHNhdGlzZmllczogRSBGIChub3QgKChub3QgKGF3YWl0X1AgPSAxKSkgb3IgRSBGICgoY3JpdGljYWxfUSA9IDEpIG9yIChjcml0aWNhbF9QID0gMSkpKSkuIAp0AAEKdAA6MTogbG9jYWxfUCgxKSwgd2FudFBfRkFMU0UoMSksIHdhbnRRX0ZBTFNFKDEpLCBsb2NhbF9RKDEpCnQAXCAgU3RhdGUgMS4gc2F0aXNmaWVzOiAoKG5vdCAoYXdhaXRfUCA9IDEpKSBvciBFIEYgKChjcml0aWNhbF9RID0gMSkgb3IgKGNyaXRpY2FsX1AgPSAxKSkpLiAKdAABCnQAPiAgMS4xOiBsb2NhbF9QKDEpLCB3YW50UF9GQUxTRSgxKSwgd2FudFFfRkFMU0UoMSksIGxvY2FsX1EoMSkKdAAxICAgIFN0YXRlIDEuMS4gZG9lcyBub3Qgc2F0aXNmeTogKGF3YWl0X1AgPSAxKS4gCnQAAQp0ADwyOiBsb2NhbF9QKDEpLCB3YW50UF9GQUxTRSgxKSwgd2FudFFfRkFMU0UoMSksIHNldFRydWVfUSgxKQp0AFwgIFN0YXRlIDIuIHNhdGlzZmllczogKChub3QgKGF3YWl0X1AgPSAxKSkgb3IgRSBGICgoY3JpdGljYWxfUSA9IDEpIG9yIChjcml0aWNhbF9QID0gMSkpKS4gCnQAAQp0AEAgIDIuMTogbG9jYWxfUCgxKSwgd2FudFBfRkFMU0UoMSksIHdhbnRRX0ZBTFNFKDEpLCBzZXRUcnVlX1EoMSkKdAAxICAgIFN0YXRlIDIuMS4gZG9lcyBub3Qgc2F0aXNmeTogKGF3YWl0X1AgPSAxKS4gCnQAAQp0ADkzOiBsb2NhbF9QKDEpLCB3YW50UF9GQUxTRSgxKSwgYXdhaXRfUSgxKSwgd2FudFFfVFJVRSgxKQp0AFwgIFN0YXRlIDMuIHNhdGlzZmllczogKChub3QgKGF3YWl0X1AgPSAxKSkgb3IgRSBGICgoY3JpdGljYWxfUSA9IDEpIG9yIChjcml0aWNhbF9QID0gMSkpKS4gCnQAAQp0AD0gIDMuMTogbG9jYWxfUCgxKSwgd2FudFBfRkFMU0UoMSksIGF3YWl0X1EoMSksIHdhbnRRX1RSVUUoMSkKdAAxICAgIFN0YXRlIDMuMS4gZG9lcyBub3Qgc2F0aXNmeTogKGF3YWl0X1AgPSAxKS4gCnQAAQp0ADs0OiBTZXRUcnVlX1AoMSksIHdhbnRQX0ZBTFNFKDEpLCBhd2FpdF9RKDEpLCB3YW50UV9UUlVFKDEpCnQAXCAgU3RhdGUgNC4gc2F0aXNmaWVzOiAoKG5vdCAoYXdhaXRfUCA9IDEpKSBvciBFIEYgKChjcml0aWNhbF9RID0gMSkgb3IgKGNyaXRpY2FsX1AgPSAxKSkpLiAKdAABCnQAPyAgNC4xOiBTZXRUcnVlX1AoMSksIHdhbnRQX0ZBTFNFKDEpLCBhd2FpdF9RKDEpLCB3YW50UV9UUlVFKDEpCnQAMSAgICBTdGF0ZSA0LjEuIGRvZXMgbm90IHNhdGlzZnk6IChhd2FpdF9QID0gMSkuIAp0AAEKdAA4NTogd2FudFBfVFJVRSgxKSwgYXdhaXRfUCgxKSwgYXdhaXRfUSgxKSwgd2FudFFfVFJVRSgxKQp0AGMgIFN0YXRlIDUuIGRvZXMgbm90IHNhdGlzZnk6ICgobm90IChhd2FpdF9QID0gMSkpIG9yIEUgRiAoKGNyaXRpY2FsX1EgPSAxKSBvciAoY3JpdGljYWxfUCA9IDEpKSkuIAp0AAEKdAA8ICA1LjE6IHdhbnRQX1RSVUUoMSksIGF3YWl0X1AoMSksIGF3YWl0X1EoMSksIHdhbnRRX1RSVUUoMSkKdAAsICAgIFN0YXRlIDUuMS5MLiBzYXRpc2ZpZXM6IChhd2FpdF9QID0gMSkuIAp0AAEKdACHICAgIFN0YXRlIDUuMS5SLiBkb2VzIG5vdCBzYXRpc2Z5OiBFIEYgKChjcml0aWNhbF9RID0gMSkgb3IgKGNyaXRpY2FsX1AgPSAxKSkuIENvdWxkIG5vdCBzaG93IGEgY291bnRlci1leGFtcGxlIGZvciB0aGlzIEVDVEwgZm9ybXVsYS4KdAABCnQAAQp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0gQ1RMIE1FTU9SWSA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAHSBSUyBub2RlczogICAgICAgICAgICAgICAgMzMKdABAIEZvcmVzdChSUykgbm9kZXM6ICAgICAgICA0MTMgYWN0aXZlcywgNDEzIHBlYWssIDAgY29tcGFjdGlvbnMuCnQAPSBGb3Jlc3QoUlMpIHNpemU6ICAgICAgICAgMTAzODMgQnl0ZXMgbm93LCAxMDM4MyBCeXRlcyBwZWFrLgp0AB4gUG90ZW50aWFsIFJHIG5vZGVzOiAgICAgIDEwNAp0AEAgRm9yZXN0KFJHKSBub2RlczogICAgICAgIDI4NSBhY3RpdmVzLCAzMzUgcGVhaywgMCBjb21wYWN0aW9ucy4KdAA7IEZvcmVzdChSRykgc2l6ZTogICAgICAgICA4MDkxIEJ5dGVzIG5vdywgOTU4NSBCeXRlcyBwZWFrLgp0ADwgRm9yZXN0KFJHK3JlYWwpIG5vZGVzOiAgIDMgYWN0aXZlcywgMyBwZWFrLCAwIGNvbXBhY3Rpb25zLgp0ADcgRm9yZXN0KFJHK3JlYWwpIHNpemU6ICAgIDgxIEJ5dGVzIG5vdywgODEgQnl0ZXMgcGVhay4KdAABCnQABE9rLgp0AAEKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09IFRJTUUgPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0ACUgVmFyaWFibGUgb3JkZXIgVGltZTogMC4wMDIgICAgIHNlYy4KdAAlIE5TRiBnZW4uIFRpbWU6ICAgICAgIDAuMDAwICAgICBzZWMuCnQAJSBSUyBHZW5lcmF0aW9uIFRpbWU6ICAwLjAwMCAgICAgc2VjLgp0ACUgVG90YWwgUlMgVGltZTogICAgICAgMC4wMDEgICAgIHNlYy4KdAAlIFN0YXRpc3RpY3MgVGltZTogICAgIDAuMDAwICAgICBzZWMuCnQAJSBDVEwgVGltZTogICAgICAgICAgICAwLjAwMSAgICAgc2VjLgp0ACUgVG90YWwgVGltZTogICAgICAgICAgMC4wMDUgICAgIHNlYy4KdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQpxAH4AJHhzcQB+AAB3BAAAAM9zcgARamF2YS5sYW5nLkJvb2xlYW7NIHKA1Zz67gIAAVoABXZhbHVleHABcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0XEAfgDRcQB+ANFxAH4A0Xg + + diff --git a/anno3/vpc/consegne/3/3.8.jpg b/anno3/vpc/consegne/3/3.8.jpg new file mode 100644 index 0000000..5dbc179 Binary files /dev/null and b/anno3/vpc/consegne/3/3.8.jpg differ diff --git a/anno3/vpc/consegne/3/3.8.smv b/anno3/vpc/consegne/3/3.8.smv new file mode 100644 index 0000000..6da56ed --- /dev/null +++ b/anno3/vpc/consegne/3/3.8.smv @@ -0,0 +1,49 @@ +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) + + +MODULE proc(mine, other) +VAR + state: {local, await, critical, setTrue, setFalse}; +ASSIGN + init(state) := local; + next(state) := case + state = local: {local, setTrue}; + state = await & other = FALSE: critical; + state = await: await; + state = setTrue: await; + state = critical: setFalse; + state = setFalse: local; + esac; \ No newline at end of file diff --git a/anno3/vpc/consegne/3/3.9-Measures.solution/PT.bnd b/anno3/vpc/consegne/3/3.9-Measures.solution/PT.bnd new file mode 100644 index 0000000..6afc04b --- /dev/null +++ b/anno3/vpc/consegne/3/3.9-Measures.solution/PT.bnd @@ -0,0 +1,16 @@ +0 1 +0 1 +0 1 +0 1 +0 1 +0 1 +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.9-Measures.solution/PT.ctl b/anno3/vpc/consegne/3/3.9-Measures.solution/PT.ctl new file mode 100644 index 0000000..18db1fe --- /dev/null +++ b/anno3/vpc/consegne/3/3.9-Measures.solution/PT.ctl @@ -0,0 +1,2 @@ +% MEASURE0 +AG (#setTrue_Q==1 -> AF (#critical_Q == 1)) diff --git a/anno3/vpc/consegne/3/3.9-Measures.solution/PT.def b/anno3/vpc/consegne/3/3.9-Measures.solution/PT.def new file mode 100644 index 0000000..f9eee66 --- /dev/null +++ b/anno3/vpc/consegne/3/3.9-Measures.solution/PT.def @@ -0,0 +1,3 @@ +|256 +% +| diff --git a/anno3/vpc/consegne/3/3.9-Measures.solution/PT.ilpbnd b/anno3/vpc/consegne/3/3.9-Measures.solution/PT.ilpbnd new file mode 100644 index 0000000..aa47d0d --- /dev/null +++ b/anno3/vpc/consegne/3/3.9-Measures.solution/PT.ilpbnd @@ -0,0 +1,2 @@ +0 +0 diff --git a/anno3/vpc/consegne/3/3.9-Measures.solution/PT.net b/anno3/vpc/consegne/3/3.9-Measures.solution/PT.net new file mode 100644 index 0000000..1dbe0bc --- /dev/null +++ b/anno3/vpc/consegne/3/3.9-Measures.solution/PT.net @@ -0,0 +1,166 @@ +|0| +| +f 0 16 0 16 0 0 0 +local_P 1 3.3333333333333335 1.6666666666666667 3.6279166666666662 1.6122916666666667 0 +setTrue_P 0 3.3333333333333335 3.0 3.5341666666666662 2.9456249999999997 0 +critical_P 0 3.3333333333333335 6.5 3.7216666666666662 6.612291666666667 0 +setFalse_P 0 3.3333333333333335 7.666666666666667 3.5237499999999997 7.695625 0 +wantP_FALSE 1 7.833333333333333 7.666666666666667 7.383125 7.862291666666667 0 +wantP_TRUE 0 4.666666666666667 7.5 5.070625 7.445625 0 +While 0 3.3333333333333335 4.5 3.169583333333333 4.695625 0 +P0 0 4.0 5.333333333333333 3.9560416666666662 5.528958333333333 0 +wantQ_FALSE 1 7.5 2.8333333333333335 7.044583333333333 3.028958333333333 0 +wantQ_TRUE 0 7.833333333333333 4.833333333333333 7.39875 5.028958333333333 0 +local_Q 1 10.833333333333334 1.5 11.1175 1.445625 0 +setTrue_Q 0 10.833333333333334 2.8333333333333335 11.278958333333334 2.778958333333333 0 +critical_Q 0 10.833333333333334 6.333333333333333 11.21125 6.445625 0 +setFalse_Q 0 10.833333333333334 7.5 11.018541666666666 7.528958333333333 0 +While_ 0 10.833333333333334 4.333333333333333 10.888333333333334 4.612291666666667 0 +P1 0 8.833333333333334 6.333333333333333 8.789375 6.528958333333333 0 +T0 1.0 0 0 1 0 3.3333333333333335 2.3333333333333335 3.3125 2.140625 3.4166666666666665 2.4010416666666665 0 + 1 1 0 0 + 1 + 1 2 0 0 + 0 +reset_transition 1.0 0 0 2 0 3.3333333333333335 8.166666666666666 2.8802083333333335 8.557291666666666 3.4166666666666665 8.234375 0 + 1 4 1 0 +3.3333333333333335 7.916666666666667 + 1 6 0 0 + 2 + -1 1 2 0 +0.75 8.166666666666666 +0.75 1.6666666666666667 + 1 5 1 0 +5.833333333333333 8.166666666666666 + 0 +T3 1.0 0 0 1 0 3.3333333333333335 7.0 3.3125 6.807291666666667 3.4166666666666665 7.067708333333333 0 + 1 3 0 0 + 1 + 1 4 0 0 + 0 +T2 1.0 0 0 2 0 3.3333333333333335 3.8333333333333335 3.3125 3.640625 3.4166666666666665 3.9010416666666665 0 + 1 2 0 0 + -1 5 1 0 +4.5 3.6666666666666665 + 2 + -1 6 1 0 +2.3333333333333335 4.0 + 1 7 0 0 + 0 +T00 1.0 0 0 1 0 2.0 1.3333333333333333 1.953125 1.140625 2.0833333333333335 1.4010416666666667 0 + 1 1 1 0 +2.75 1.25 + 1 + 1 1 0 0 + 0 +T1 1.0 0 0 2 2 1.0 5.166666666666667 0.9791666666666666 4.973958333333333 1.0833333333333333 5.234375 0 + 1 7 0 0 + -1 9 1 0 +2.5 2.9166666666666665 + 2 + 1 3 2 0 +1.5 6.333333333333333 +1.9166666666666667 6.583333333333333 + -1 9 1 0 +0.5833333333333334 5.583333333333333 + 0 +T4 1.0 0 0 3 3 5.0 5.0 4.979166666666667 4.807291666666667 5.083333333333333 5.067708333333333 0 + 1 7 0 0 + -1 6 1 0 +8.416666666666666 3.5833333333333335 + -1 10 2 0 +4.416666666666667 3.5833333333333335 +5.916666666666667 3.25 + 3 + 1 8 0 0 + -1 5 2 0 +6.416666666666667 5.666666666666667 +8.333333333333334 7.416666666666667 + -1 10 2 0 +3.25 6.583333333333333 +4.666666666666667 6.333333333333333 + 0 +T5 1.0 0 0 2 1 3.3333333333333335 5.666666666666667 3.3125 5.473958333333333 3.4166666666666665 5.734375 0 + 1 8 0 0 + -1 5 1 0 +4.083333333333333 6.25 + 2 + 1 7 0 0 + -1 6 3 0 +0.5 6.083333333333333 +0.3333333333333333 9.25 +7.75 9.083333333333334 + 0 +T15 1.0 0 0 1 0 10.833333333333334 2.1666666666666665 10.786458333333334 1.9739583333333333 10.916666666666666 2.234375 0 + 1 11 0 0 + 1 + 1 12 0 0 + 0 +reset_Transition 1.0 0 0 1 0 10.833333333333334 8.0 10.359375 8.390625 10.916666666666666 8.067708333333334 0 + 1 14 1 0 +10.833333333333334 7.75 + 1 + -1 11 2 0 +7.5 8.0 +7.5 1.5 + 0 +T9 1.0 0 0 1 0 10.833333333333334 6.833333333333333 10.8125 6.640625 10.916666666666666 6.901041666666667 0 + 1 13 0 0 + 1 + 1 14 0 0 + 0 +T12 1.0 0 0 2 0 10.833333333333334 3.6666666666666665 10.786458333333334 3.4739583333333335 10.916666666666666 3.734375 0 + 1 12 0 0 + -1 9 0 0 + 2 + 1 15 0 0 + -1 10 4 0 +13.666666666666666 3.6666666666666665 +14.0 8.333333333333334 +9.75 8.583333333333334 +9.583333333333334 8.5 + 0 +T100 1.0 0 0 1 0 9.5 1.1666666666666667 9.427083333333334 0.9739583333333334 9.583333333333334 1.234375 0 + 1 11 1 0 +10.25 1.0833333333333333 + 1 + 1 11 0 0 + 0 +T11 1.0 0 0 2 1 10.833333333333334 5.5 10.786458333333334 5.307291666666667 10.916666666666666 5.567708333333333 0 + 1 16 1 0 +10.833333333333334 5.916666666666667 + -1 9 2 0 +10.2587890625 5.50703125 +10.083333333333334 6.25 + 2 + 1 15 0 0 + -1 10 2 0 +12.416666666666666 5.916666666666667 +9.25 6.833333333333333 + 0 +T6 1.0 0 0 3 2 9.333333333333334 5.0 7.979166666666667 1.390625 9.416666666666666 5.067708333333333 0 + 1 15 0 0 + -1 6 1 0 +9.25 4.083333333333333 + 1 10 0 0 + 3 + 1 16 0 0 + -1 6 2 0 +10.0 5.0 +10.0 7.333333333333333 + 1 9 0 0 + 0 +T7 1.0 0 0 2 1 13.166666666666666 5.166666666666667 13.145833333333334 4.973958333333333 13.25 5.234375 0 + 1 15 0 0 + -1 5 2 0 +13.166666666666666 3.25 +6.333333333333333 4.0 + 2 + 1 13 1 0 +13.166666666666666 6.333333333333333 + -1 5 4 0 +13.5 5.166666666666667 +13.416666666666666 9.0 +11.0 9.166666666666666 +7.25 9.083333333333334 + 0 diff --git a/anno3/vpc/consegne/3/3.9-Measures.solution/PT.pba b/anno3/vpc/consegne/3/3.9-Measures.solution/PT.pba new file mode 100644 index 0000000..7ebe769 --- /dev/null +++ b/anno3/vpc/consegne/3/3.9-Measures.solution/PT.pba @@ -0,0 +1,7 @@ +5 +2 1 9 1 10 +6 1 11 1 12 1 13 1 14 1 15 1 16 +4 -1 3 -1 4 1 6 -1 7 +4 1 3 1 4 1 5 1 7 +6 1 1 1 2 1 3 1 4 1 7 1 8 +0 diff --git a/anno3/vpc/consegne/3/3.9-Measures.solution/PT.pin b/anno3/vpc/consegne/3/3.9-Measures.solution/PT.pin new file mode 100644 index 0000000..0c105f0 --- /dev/null +++ b/anno3/vpc/consegne/3/3.9-Measures.solution/PT.pin @@ -0,0 +1,8 @@ +6 +6 1 1 1 2 1 3 1 4 1 7 1 8 +4 1 1 1 2 1 6 1 8 +4 1 3 1 4 1 5 1 7 +2 1 5 1 6 +6 1 11 1 12 1 13 1 14 1 15 1 16 +2 1 9 1 10 +0 diff --git a/anno3/vpc/consegne/3/3.9.PNPRO b/anno3/vpc/consegne/3/3.9.PNPRO new file mode 100644 index 0000000..da0e072 --- /dev/null +++ b/anno3/vpc/consegne/3/3.9.PNPRO @@ -0,0 +1,223 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + rO0ABXNyABRqYXZhLnV0aWwuTGlua2VkTGlzdAwpU11KYIgiAwAAeHB3BAAAAMF0AJMbWzBtRVhFQzogL3Vzci9sb2NhbC9HcmVhdFNQTi9iaW4vRFNQTi1Ub29sIC1sb2FkICIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuOS1NZWFzdXJlcy5zb2x1dGlvbi9QVCIgLXBiYXNpcyAtZGV0ZWN0LWV4cCAtcHNmbCAtYm5kIAp0AHAbWzFtG1s0bUxPQURJTkcgUEVUUkkgTkVUIC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy45LU1lYXN1cmVzLnNvbHV0aW9uL1BUIChuZXQvZGVmKS4uLhtbMjJtG1syNG0KdAAPTUFSS0lORyBQQVI6IDAKdAAQUExBQ0VTOiAgICAgIDE2CnQAD1JBVEUgUEFSOiAgICAwCnQAEFRSQU5TSVRJT05TOiAxNgp0AA9NRUFTVVJFUzogICAgMAp0AChMT0FESU5HIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAABCnQAAQp0AB5DT01QVVRJTkcgUExBQ0UgRkxPVyBCQVNJUy4uLgp0ABJNPTE2LCBOPTE2LCBOMD0xNgp0ADlDb21wdXRhdGlvbiBvZiBGbG93IGJhc2lzOiBzdGVwIDEvMTYsIHxLfD0xNCwgcHJvZHVjdHM9MQp0AFMbWzFBICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgCnQAUxtbMUFDb21wdXRhdGlvbiBvZiBGbG93IGJhc2lzOiBjb21wbGV0ZWQgaW4gMTEgc3RlcHMsIHxLfD01LiAgICAgICAgICAgICAgICAgICAgICAKdABARk9VTkQgNSBWRUNUT1JTIElOIFRIRSBQTEFDRSBGTE9XIEJBU0lTICg0IHNlbWlmbG93cywgMSBmbG93cykuCnQAAQp0AAEKdAAnQWxsIHBsYWNlcyBhcmUgY292ZXJlZCBieSBzb21lIFAtZmxvdy4KdAABCnQAJlRPVEFMIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAAnQVZPSUQgRVhQT05FTlRJQUwgR1JPV1RIIE9GIFNFTUlGTE9XUy4KdAAdQ09NUFVUSU5HIFBMQUNFIFNFTUlGTE9XUy4uLgp0ABJNPTE2LCBOPTE2LCBOMD0xNgp0ACtHZW5lcmF0aW9uIG9mIFNlbWlmbG93czogc3RlcCAxLzE2LCB8S3w9MTQKdABTG1sxQSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAp0AFEbWzFBR2VuZXJhdGlvbiBvZiBTZW1pZmxvd3M6IGNvbXBsZXRlZCBpbiAxMSBzdGVwcywgfEt8PTYuICAgICAgICAgICAgICAgICAgICAgIAp0ABlGT1VORCA2IFBMQUNFIFNFTUlGTE9XUy4KdAABCnQAAQp0ACtBbGwgcGxhY2VzIGFyZSBjb3ZlcmVkIGJ5IHNvbWUgUC1zZW1pZmxvdy4KdAABCnQAJlRPVEFMIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAAsQ09NUFVUSU5HIFBMQUNFIEJPVU5EUyBGUk9NIFAtU0VNSUZMT1dTIC4uLgp0ACcbWzBYG1szMm0gUFJPQ0VTUyBFWElURUQgTk9STUFMTFkuG1swbQp0AKQbWzBtRVhFQzogcGVybCAtZSAnYWxhcm0gNSA7IGV4ZWMgIi91c3IvbG9jYWwvR3JlYXRTUE4vYmluL0RTUE4tVG9vbCAtbG9hZCBcIi9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy45LU1lYXN1cmVzLnNvbHV0aW9uL1BUXCIgLWxvYWQtYm5kIC1pbHAtYm5kIiAnCnQAcBtbMW0bWzRtTE9BRElORyBQRVRSSSBORVQgL2hvbWUvdXNlci9VTklUTy9hbm5vMy92cGMvY29uc2VnbmUvMy8zLjktTWVhc3VyZXMuc29sdXRpb24vUFQgKG5ldC9kZWYpLi4uG1syMm0bWzI0bQp0AA9NQVJLSU5HIFBBUjogMAp0ABBQTEFDRVM6ICAgICAgMTYKdAAPUkFURSBQQVI6ICAgIDAKdAAQVFJBTlNJVElPTlM6IDE2CnQAD01FQVNVUkVTOiAgICAwCnQAKExPQURJTkcgVElNRTogW1VzZXIgMC4wMDBzLCBTeXMgMC4wMDBzXQp0AAEKdAABCnQAFUxPQURJTkcgQk5EIEZJTEUgLi4uCnQAJUNPTVBVVElORyBQTEFDRSBCT1VORFMgVVNJTkcgSUxQIC4uLgp0ABhBbGwgcGxhY2VzIGFyZSBib3VuZGVkLgpxAH4AJHQAeBtbMG1FWEVDOiAvdXNyL2xvY2FsL0dyZWF0U1BOL2Jpbi9SR01FREQzICIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuOS1NZWFzdXJlcy5zb2x1dGlvbi9QVCIgLU1FVEEgIC1jIC1DCnQAIFJhbmRvbSBzZWVkczogMTU4ODk1ODU4MSAyMDE5ODYKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0ABFHcmVhdFNQTi9NZWRkbHkuCnQAOCAgQ29weXJpZ2h0IChDKSAxOTg3LTIwMTgsIFVuaXZlcnNpdHkgb2YgVG9yaW5vLCBJdGFseS4KdAAxICBTZW5kIGZpbGVzIG5ldG5hbWUubmV0LCAuZGVmIHRvIGUtbWFpbCBhZGRyZXNzCnQAKyAgYmVjY3V0aUBkaS51bml0by5pdCBpZiB5b3UgZmluZCBhbnkgYnVnLgp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAH0Jhc2VkIG9uIE1FRERMWSB2ZXJzaW9uIDAuMTYuMAp0AEYgIENvcHlyaWdodCAoQykgMjAwOSwgSW93YSBTdGF0ZSBVbml2ZXJzaXR5IFJlc2VhcmNoIEZvdW5kYXRpb24sIEluYy4KdAApICB3ZWJzaXRlOiBodHRwOi8vbWVkZGx5LnNvdXJjZWZvcmdlLm5ldAp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAKVVzaW5nIHBlci1ldmVudCBzYXR1cmF0aW9uIChzYXQtcHJlZ2VuKS4KdAAbVXNpbmcgZmFzdCBOU0YgZ2VuZXJhdGlvbi4KdAASUHJvY2VzcyBJRDogMjUwMzcKdABLTU9ERUwgTkFNRTogL2hvbWUvdXNlci9VTklUTy9hbm5vMy92cGMvY29uc2VnbmUvMy8zLjktTWVhc3VyZXMuc29sdXRpb24vUFQKdAAdICAxNiBwbGFjZXMsIDE2IHRyYW5zaXRpb25zLgp0ACdVc2VkIE1lbW9yeSBmb3IgZW5jb2RpbmcgbmV0OiA0NTUxNDBLQgp0AFVPcGVuaW5nIGZpbGU6IC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy45LU1lYXN1cmVzLnNvbHV0aW9uL1BULmJuZCBPSy4KdABYT3BlbmluZyBmaWxlOiAvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuOS1NZWFzdXJlcy5zb2x1dGlvbi9QVC5pbHBibmQgT0suCnQAEElOUFVUIEFSQ1M6ICAyMQp0ABBPVVRQVVQgQVJDUzogMjEKdAAPSU5ISUIgQVJDUzogIDAKdAAPVEVTVCBBUkNTOiAgIDYKdAAQUExBQ0VTOiAgICAgIDE2CnQAEFRSQU5TSVRJT05TOiAxNgp0AA9JTlZBUklBTlRTOiAgNQp0AA9QLVNFTUlGTE9XUzogNgp0ABZNQVggSU5WQVJJQU5UIENBUkQ6IDEKdAABCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0gVkFSSUFCTEUgT1JERVIgPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAA8VmFyaWFibGUgb3JkZXIgbWV0aG9kOiBNZXRhLWhldXJpc3RpYyB1c2luZyB3ZWlnaHRlZCBzY29yZS4KdABRICBNRVRIT0QgICAgICAgICAgICAgIFNDT1JFICAgICAgICBTV0lSICAgICAgIFNPVVBTIERJU0NPVU5UICBXRUlHSFQgICAgICAgVElNRSAKdABVICBTTE8gICAgICAgICAgICAgICAxNjcuMTc4ICAgICAgICAgMTQ5ICAgICAgICAgIDgwICAgICAgICAxICAgMS4xMjIgICAwLjAwMDE5OCBzZWMuCnQAVSAgU0xPK0ZvcmNlICAgICAgICAgICA2Ny43NiAgICAgICAgICA3NyAgICAgICAgICA2MSAgICAgICAgMSAgICAwLjg4ICAgIDcuMWUtMDUgc2VjLgp0AFUgIFNMTy0xNiAgICAgICAgICAgIDExOC45MDIgICAgICAgICAxNDkgICAgICAgICAgODAgICAgICAgIDEgICAwLjc5OCAgICA5LjVlLTA1IHNlYy4KdABVICBTTE8tMTYrRm9yY2UgICAgICAgNzAuMTQ3ICAgICAgICAgIDc3ICAgICAgICAgIDYxICAgICAgICAxICAgMC45MTEgICAgNi40ZS0wNSBzZWMuCnQAVSAgVE9WMiAgICAgICAgICAgICAgMTYwLjg5MyAgICAgICAgIDE3NyAgICAgICAgICA3OSAgICAgICAgMSAgIDAuOTA5ICAgIDkuOWUtMDUgc2VjLgp0AFUgIFRPVjIrRm9yY2UgICAgICAgICA5Ny4yNzIgICAgICAgICAgODQgICAgICAgICAgNzcgICAgICAgIDEgICAxLjE1OCAgICA4LjVlLTA1IHNlYy4KdABVICBOT0FDSzIgICAgICAgICAgICAyMTAuMzY2ICAgICAgICAgMTg2ICAgICAgICAgIDgxICAgICAgICAxICAgMS4xMzEgICAgNi45ZS0wNSBzZWMuCnQAVSAgTk9BQ0syK0ZvcmNlICAgICAgICA4NS4yNiAgICAgICAgICA4NyAgICAgICAgICA3NiAgICAgICAgMSAgICAwLjk4ICAgIDYuMmUtMDUgc2VjLgp0AFUgIEFDTSAgICAgICAgICAgICAgIDIxMS4yOTkgICAgICAgICAyMDkgICAgICAgICAgODMgICAgICAgIDEgICAxLjAxMSAgICA4LjVlLTA1IHNlYy4KdABVICBBQ00rRm9yY2UgICAgICAgICAgIDg5LjQ2ICAgICAgICAgIDcwICAgICAgICAgIDU3ICAgICAgICAxICAgMS4yNzggICAgNS40ZS0wNSBzZWMuCnQAVSAgQ00yICAgICAgICAgICAgICAgMTI4Ljc3NSAgICAgICAgIDEwMSAgICAgICAgICA2NCAgICAgICAgMSAgIDEuMjc1ICAgIDUuMmUtMDUgc2VjLgp0AFUgIENNMitGb3JjZSAgICAgICAgICAgNzYuOTMgICAgICAgICAgNzAgICAgICAgICAgNTcgICAgICAgIDEgICAxLjA5OSAgICAzLjhlLTA1IHNlYy4KdABVICBQICAgICAgICAgICAgICAgICAxMjEuNjg0ICAgICAgICAgMTE2ICAgICAgICAgIDk3ICAgICAgICAxICAgMS4wNDkgICAgMy40ZS0wNSBzZWMuCnQAVSAgR1AgICAgICAgICAgICAgICAgIDg3LjIyNSAgICAgICAgICA3NSAgICAgICAgICA2NiAgICAgICAgMSAgIDEuMTYzICAgMC4wMDAyMTIgc2VjLgp0AFUgIEdQK0ZvcmNlICAgICAgICAgICA3MC44NzUgICAgICAgICAgNjMgICAgICAgICAgNTQgICAgICAgIDEgICAxLjEyNSAgICA1LjVlLTA1IHNlYy4KdAA9TWV0YS1oZXVyaXN0aWM6IHNlbGVjdGluZyBtZXRob2QgU0xPK0ZvcmNlIHdpdGggc2NvcmU6IDY3Ljc2CnQAKVRpbWUgdG8gY29tcHV0ZSB2YXJpYWJsZSBvcmRlcjogMC4wMDI0OTQKdAABCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT0gU1RBUlQgRklSSU5HIFJVTEVTIEVOQ09ESU5HID09PT09PT09PT09PT09PT09PT09PT09PT0KdAAsRW5jb2RlZCAxNiB0cmFuc2l0aW9uIGluIDEgcHJpb3JpdHkgZ3JvdXBzLgp0ACFUaW1lIHRvIGJ1aWxkIGFsbCBOU0ZzOiAwLjAwMDkzOQp0AAEKdABQPT09PT09PT09PT09PT09PT09PT09PT09PSBSRUFDSEFCSUxJVFkgU0VUIEdFTkVSQVRJT04gPT09PT09PT09PT09PT09PT09PT09PT09PQp0ABVTcGxpdDogU3BsaXRTdWJ0cmFjdAp0AB1SUyBnZW5lcmF0aW9uIHRpbWU6IDAuMDAwNTcxCnQAHUNvbXB1dGluZyB2YXJpYWJsZSBib3VuZHMuLi4KdAABCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09IE1FTU9SWSA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAApIFRvdGFsIE1lbW9yeSBVc2VkOiAgICAgICA0NTUxNDAgS0J5dGVzLgp0AAEKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PSBDVEwgRVZBTFVBVElPTiA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0AAEKdABiUHJvY2Vzc2luZzogKG5vdCBFIEYgKG5vdCAoKG5vdCAoc2V0VHJ1ZV9RID0gMSkpIG9yIChub3QgRSBHIChub3QgKGNyaXRpY2FsX1EgPSAxKSkpKSkpICAtPiAgYm9vbAp0ABBFdmFsOiBzZXRUcnVlX1EKdAAUICAgICAgMC4wMDAwMjAgc2VjLgp0ABZFdmFsOiAoc2V0VHJ1ZV9RID0gMSkKdAAeICAgICAgMC4wMDAwNTIgc2VjLiAgY2FyZCA9IDkKdAAcRXZhbDogKG5vdCAoc2V0VHJ1ZV9RID0gMSkpCnQAHyAgICAgIDAuMDAwMDUwIHNlYy4gIGNhcmQgPSAyOAp0ABFFdmFsOiBjcml0aWNhbF9RCnQAFCAgICAgIDAuMDAwMDA0IHNlYy4KdAAXRXZhbDogKGNyaXRpY2FsX1EgPSAxKQp0AB4gICAgICAwLjAwMDAyMSBzZWMuICBjYXJkID0gNAp0AB1FdmFsOiAobm90IChjcml0aWNhbF9RID0gMSkpCnQAHyAgICAgIDAuMDAwMDI0IHNlYy4gIGNhcmQgPSAzMwp0ACFFdmFsOiBFIEcgKG5vdCAoY3JpdGljYWxfUSA9IDEpKQp0ACBFRzogc3RlcD0xLCAgU0FUIHNpemU9MzMuMDAwMDAwCnQAGlIyID0gMTk3IGluIDEgaXRlcmF0aW9ucy4KdAAfICAgICAgMC4wMDAyMzIgc2VjLiAgY2FyZCA9IDMzCnQAJ0V2YWw6IChub3QgRSBHIChub3QgKGNyaXRpY2FsX1EgPSAxKSkpCnQAHiAgICAgIDAuMDAwMDE2IHNlYy4gIGNhcmQgPSA0CnQAQkV2YWw6ICgobm90IChzZXRUcnVlX1EgPSAxKSkgb3IgKG5vdCBFIEcgKG5vdCAoY3JpdGljYWxfUSA9IDEpKSkpCnQAHyAgICAgIDAuMDAwMDE1IHNlYy4gIGNhcmQgPSAyOAp0AEhFdmFsOiAobm90ICgobm90IChzZXRUcnVlX1EgPSAxKSkgb3IgKG5vdCBFIEcgKG5vdCAoY3JpdGljYWxfUSA9IDEpKSkpKQp0AB4gICAgICAwLjAwMDE0MCBzZWMuICBjYXJkID0gOQp0AExFdmFsOiBFIEYgKG5vdCAoKG5vdCAoc2V0VHJ1ZV9RID0gMSkpIG9yIChub3QgRSBHIChub3QgKGNyaXRpY2FsX1EgPSAxKSkpKSkKdAAuICAgICAgNyBzdGVwczogICAgICAgMC4wMDA5Mzcgc2VjLiAgY2FyZCA9IDY2CnQAUkV2YWw6IChub3QgRSBGIChub3QgKChub3QgKHNldFRydWVfUSA9IDEpKSBvciAobm90IEUgRyAobm90IChjcml0aWNhbF9RID0gMSkpKSkpKQp0AB4gICAgICAwLjAwMDAyNiBzZWMuICBjYXJkID0gMAp0ADQtLS0gQUcgKCNzZXRUcnVlX1E9PTEgLT4gQUYgKCNjcml0aWNhbF9RID09IDEpKSAtLS0KdAAZRm9ybXVsYSBuYW1lOiBNRUFTVVJFMCAgCnQAFglFdmFsdWF0aW9uOiBmYWxzZSAgIAp0ACcJU2F0LXNldCBnZW5lcmF0aW9uIHRpbWU6IDAuMDAxOTE3IHNlYwp0AB8JRXZhbHVhdGlvbiB0aW1lOiAwLjAwMTkxOSBzZWMKdAABCnQAHEdlbmVyYXRlZCBjb3VudGVyLWV4YW1wbGU6IAp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0gVHJhY2UgPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQASUluaXRpYWwgc3RhdGUgaXM6IGxvY2FsX1EoMSksIHdhbnRRX0ZBTFNFKDEpLCB3YW50UF9GQUxTRSgxKSwgbG9jYWxfUCgxKQp0AGFJbml0aWFsIHN0YXRlIHNhdGlzZmllczogRSBGIChub3QgKChub3QgKHNldFRydWVfUSA9IDEpKSBvciAobm90IEUgRyAobm90IChjcml0aWNhbF9RID0gMSkpKSkpLiAKdAABCnQAOjE6IGxvY2FsX1EoMSksIHdhbnRRX0ZBTFNFKDEpLCB3YW50UF9GQUxTRSgxKSwgbG9jYWxfUCgxKQp0AFQgIFN0YXRlIDEuIHNhdGlzZmllczogKChub3QgKHNldFRydWVfUSA9IDEpKSBvciAobm90IEUgRyAobm90IChjcml0aWNhbF9RID0gMSkpKSkuIAp0AAEKdAA+ICAxLjE6IGxvY2FsX1EoMSksIHdhbnRRX0ZBTFNFKDEpLCB3YW50UF9GQUxTRSgxKSwgbG9jYWxfUCgxKQp0ADMgICAgU3RhdGUgMS4xLiBkb2VzIG5vdCBzYXRpc2Z5OiAoc2V0VHJ1ZV9RID0gMSkuIAp0AAEKdAA8Mjogc2V0VHJ1ZV9RKDEpLCB3YW50UV9GQUxTRSgxKSwgd2FudFBfRkFMU0UoMSksIGxvY2FsX1AoMSkKdABbICBTdGF0ZSAyLiBkb2VzIG5vdCBzYXRpc2Z5OiAoKG5vdCAoc2V0VHJ1ZV9RID0gMSkpIG9yIChub3QgRSBHIChub3QgKGNyaXRpY2FsX1EgPSAxKSkpKS4gCnQAAQp0AEAgIDIuMTogc2V0VHJ1ZV9RKDEpLCB3YW50UV9GQUxTRSgxKSwgd2FudFBfRkFMU0UoMSksIGxvY2FsX1AoMSkKdAAuICAgIFN0YXRlIDIuMS5MLiBzYXRpc2ZpZXM6IChzZXRUcnVlX1EgPSAxKS4gCnQAAQp0AEcgICAgU3RhdGUgMi4xLlIuIHNhdGlzZmllczogRSBHIChub3QgKGNyaXRpY2FsX1EgPSAxKSkuIFN0YXJ0IG9mIGxvb3AuCnQAAQp0AEYgICAgMi4xLlIuMTogc2V0VHJ1ZV9RKDEpLCB3YW50UV9GQUxTRSgxKSwgd2FudFBfRkFMU0UoMSksIGxvY2FsX1AoMSkKdAA6ICAgICAgU3RhdGUgMi4xLlIuMS4gZG9lcyBub3Qgc2F0aXNmeTogKGNyaXRpY2FsX1EgPSAxKS4gCnQAAQp0ACkgICAgMi4xLlIuMjogbG9vcCBiYWNrIHRvIHN0YXRlIDIuMS5SLjEuCnQAAQp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0gQ1RMIE1FTU9SWSA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAHSBSUyBub2RlczogICAgICAgICAgICAgICAgNDcKdABAIEZvcmVzdChSUykgbm9kZXM6ICAgICAgICA3MjMgYWN0aXZlcywgNzIzIHBlYWssIDAgY29tcGFjdGlvbnMuCnQAPSBGb3Jlc3QoUlMpIHNpemU6ICAgICAgICAgMTgwNjkgQnl0ZXMgbm93LCAxODA2OSBCeXRlcyBwZWFrLgp0AB4gUG90ZW50aWFsIFJHIG5vZGVzOiAgICAgIDEzNQp0AEAgRm9yZXN0KFJHKSBub2RlczogICAgICAgIDUyMiBhY3RpdmVzLCA2NzcgcGVhaywgMCBjb21wYWN0aW9ucy4KdAA9IEZvcmVzdChSRykgc2l6ZTogICAgICAgICAxNDk2NiBCeXRlcyBub3csIDE5NTM1IEJ5dGVzIHBlYWsuCnQAPCBGb3Jlc3QoUkcrcmVhbCkgbm9kZXM6ICAgMiBhY3RpdmVzLCAyIHBlYWssIDAgY29tcGFjdGlvbnMuCnQANyBGb3Jlc3QoUkcrcmVhbCkgc2l6ZTogICAgNTQgQnl0ZXMgbm93LCA1NCBCeXRlcyBwZWFrLgp0AAEKdAAET2suCnQAAQp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0gVElNRSA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAJSBWYXJpYWJsZSBvcmRlciBUaW1lOiAwLjAwMyAgICAgc2VjLgp0ACUgTlNGIGdlbi4gVGltZTogICAgICAgMC4wMDEgICAgIHNlYy4KdAAlIFJTIEdlbmVyYXRpb24gVGltZTogIDAuMDAxICAgICBzZWMuCnQAJSBUb3RhbCBSUyBUaW1lOiAgICAgICAwLjAwMiAgICAgc2VjLgp0ACUgU3RhdGlzdGljcyBUaW1lOiAgICAgMC4wMDAgICAgIHNlYy4KdAAlIENUTCBUaW1lOiAgICAgICAgICAgIDAuMDAzICAgICBzZWMuCnQAJSBUb3RhbCBUaW1lOiAgICAgICAgICAwLjAwOSAgICAgc2VjLgp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnEAfgAkeHNxAH4AAHcEAAAAwXNyABFqYXZhLmxhbmcuQm9vbGVhbs0gcoDVnPruAgABWgAFdmFsdWV4cAFxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMNxAH4Aw3EAfgDDcQB+AMN4 + + diff --git a/anno3/vpc/consegne/3/3.9.jpg b/anno3/vpc/consegne/3/3.9.jpg new file mode 100644 index 0000000..13bd23d Binary files /dev/null and b/anno3/vpc/consegne/3/3.9.jpg differ diff --git a/anno3/vpc/consegne/3/3.9.smv b/anno3/vpc/consegne/3/3.9.smv new file mode 100644 index 0000000..e03b0c0 --- /dev/null +++ b/anno3/vpc/consegne/3/3.9.smv @@ -0,0 +1,46 @@ +MODULE main +VAR + wantP: boolean; + wantQ: boolean; + p: process proc(wantP, wantQ); -- PROCESS: http://nusmv.fbk.eu/NuSMV/userman/v21/nusmv_3.html#SEC27 + q: process proc(wantQ, wantP); +ASSIGN + init(wantP) := FALSE; + init(wantQ) := FALSE; + +CTLSPEC -- no mutual exclusion + AG (p.state != critical | q.state != critical) + +CTLSPEC -- no deadlock + AG ((p.state = setTrue | q.state = setTrue) -> AF (p.state = critical | q.state = critical)) + +CTLSPEC -- no individual starvation + AG (p.state = setTrue -> AF p.state = critical) +CTLSPEC + AG (q.state = setTrue -> AF q.state = critical) + + +MODULE proc(mine, other) +VAR + state: {local, critical, setTrue, setFalse, resetTrue, resetFalse}; +ASSIGN + init(state) := local; + next(state) := case + state = local: {local, setTrue}; + state = setTrue & other = TRUE: resetFalse; + state = setTrue & other = FALSE: critical; + state = resetFalse: resetTrue; + state = resetTrue & other = TRUE: resetFalse; + state = resetTrue & other = FALSE: critical; + state = critical: setFalse; + state = setFalse: local; + esac; + next(mine) := case + state = setTrue: TRUE; + state = setFalse: FALSE; + state = resetTrue: TRUE; + state = resetFalse: FALSE; + TRUE: mine; + esac; +FAIRNESS + running \ No newline at end of file diff --git a/anno3/vpc/consegne/3/analisi.org b/anno3/vpc/consegne/3/analisi.org index aebf098..83d4a3c 100644 --- a/anno3/vpc/consegne/3/analisi.org +++ b/anno3/vpc/consegne/3/analisi.org @@ -15,7 +15,6 @@ # ** GreatSPN # ** TODO CCS # ** Risultati - Nella tabella mostriamo i risultati ottenuti | | NuSMV | GreatSPN | |---------------------+-------+----------| @@ -32,7 +31,8 @@ Nella tabella mostriamo i risultati ottenuti - [ ] Controlla in 3.6 Starvation: nusmv no, greatspn si` - [ ] 3.6, dealock: correttezza spiegazione della differenza greatspn nusmv? - [ ] 3.6, starvation: perche` nusmv con processi non ha starvation? -- [ ] 3.6, perche` Amparore ha detto che deadlock: AG(EF(#critical_P == 1)) ?? +- [ ] 3.6, Amparore ha detto che deadlock: AG(EF(#critical_P == 1)) ?? +- [ ] 3.6, inserisci controesempi dove necessario NOTA: nel caso di Ampararore, la formula: | da qualsiasi stato e` sempre possibile arrivare a critical_P == 1 @@ -231,6 +231,7 @@ AG(!(#critical_P == 1) || !(#critical_Q == 1)) AG ((#await_P==1 || \#await_Q == 1) -> AF (#critical_P == 1 || \#critical_Q == 1)) AG (#await_P==1 -> AF (#critical_P == 1)) #+END_SRC +[[./3.6.jpg]] ** TODO CCS ** TODO Risultati @@ -256,3 +257,364 @@ seguente formula CTL | AG (wā‚š ā†’ EF (cā‚š || c_{q})) | AG(#await_P == 1 -> EF(#critical_Q==1 || \#critical_P == 1)) che risulta rispettata. +* Algoritmo 3.8 +Due processi iterano all'infinito seguendo questo pseudocodice + +#+BEGIN_SRC +while true: + non-critical section + wantP <- true + await wantQ = false + critical section + wantP <- false +#+END_SRC + +** NuSMV +Si e` deciso di modellare l'algoritmo allo stesso modo del precedente. +#+include 3.8.b.smv +** GreatSPN +Il codice utilizzato per le proprieta` CTL e` il seguente: +#+BEGIN_SRC +AG(!(#critical_P == 1) || !(#critical_Q == 1)) +AG ((#await_P==1 || \#await_Q == 1) -> AF (#critical_P == 1 || \#critical_Q == 1)) +AG (#await_P==1 -> AF (#critical_P == 1)) +AG (#await_Q==1 -> AF (#critical_Q == 1)) +#+END_SRC +Inoltre, per confermare alcune ipotesi, si e` testata anche la +seguente formula CTL: +| AG(#await_P == 1 -> EF(#critical_Q==1 || \#critical_P == 1)) +che conferma la presenza di deadlock causata dalle due variabili booleane. +[[./3.8.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 | +Questo algoritmo rispetto al precedente garantisce la mutua +esclusione, ma non ci permette di evitare il deadlock (e di +conseguenza neanche la starvation individuale). + +Di seguito riportiamo la traccia di NuSMV che mostra che il deadlock +avviene quando i progetti eseguono /setTrue/ nello stesso momento. +#+BEGIN_SRC +-- specification AG ((p.state = await | q.state = await) -> AF (p.state = critical | q.state = critical)) is false +-- as demonstrated by the following execution sequence +Trace Description: CTL Counterexample +Trace Type: Counterexample + -> State: 1.1 <- + wantP = FALSE + wantQ = FALSE + p.state = local + q.state = local + -> State: 1.2 <- + p.state = setTrue + q.state = setTrue + -- Loop starts here + -> State: 1.3 <- + wantP = TRUE + wantQ = TRUE + p.state = await + q.state = await + -> State: 1.4 <- +#+END_SRC +Mostriamo invece il controesempio generato da GreatSPN che ci mostra +una condizione di starvation individuale, dove, come in precedenza, il +processo Q rimane in /local_Q/. +#+BEGIN_SRC +Generated counter-example: +==================================== Trace ==================================== +Initial state is: local_P(1), wantP_FALSE(1), wantQ_FALSE(1), local_Q(1) +Initial state satisfies: E F (not ((not (await_P = 1)) or (not E G (not (critical_P = 1))))). + +1: local_P(1), wantP_FALSE(1), wantQ_FALSE(1), local_Q(1) + State 1. satisfies: ((not (await_P = 1)) or (not E G (not (critical_P = 1)))). + + 1.1: local_P(1), wantP_FALSE(1), wantQ_FALSE(1), local_Q(1) + State 1.1. does not satisfy: (await_P = 1). + +2: SetTrue_P(1), wantP_FALSE(1), wantQ_FALSE(1), local_Q(1) + State 2. satisfies: ((not (await_P = 1)) or (not E G (not (critical_P = 1)))). + + 2.1: SetTrue_P(1), wantP_FALSE(1), wantQ_FALSE(1), local_Q(1) + State 2.1. does not satisfy: (await_P = 1). + +3: wantP_TRUE(1), await_P(1), wantQ_FALSE(1), local_Q(1) + State 3. does not satisfy: ((not (await_P = 1)) or (not E G (not (critical_P = 1)))). + + 3.1: wantP_TRUE(1), await_P(1), wantQ_FALSE(1), local_Q(1) + State 3.1.L. satisfies: (await_P = 1). + + State 3.1.R. satisfies: E G (not (critical_P = 1)). Start of loop. + + 3.1.R.1: wantP_TRUE(1), await_P(1), wantQ_FALSE(1), local_Q(1) + State 3.1.R.1. does not satisfy: (critical_P = 1). + + 3.1.R.2: loop back to state 3.1.R.1. +#+END_SRC + +* Algoritmo 3.9 +Due processi iterano all'infinito seguendo questo pseudocodice + +#+BEGIN_SRC +while true: + non-critical section + wantP <- true + while wantQ + wantP <- false + wantP <- true + critical section + wantP <- false +#+END_SRC +(l'altro processo segue uno pseudocodice simmetrico) + +** NuSMV +Si e` deciso di modellare l'algoritmo usando per ognuno dei due +processi utilizzando l'espressione /process/ per simulare di NuSMV e +per ciascun process una variabile /state/ di tipo enumerazione +| state: {local, critical, setTrue, setFalse, resetTrue, resetFalse}; +Benche` non fosse necessario distinguere il set della variabile +booleana /wantP/, si e` preferito farlo in quanto l'enumerazione di +tutti gli stati possibili, come evidenziato dal codice che segue, non +risulta complesso. +#+include 3.9.smv + +** GreatSPN +Il codice utilizzato per le proprieta` CTL e` il seguente: +#+BEGIN_SRC +AG(!(#critical_P == 1) || !(#critical_Q == 1)) +AG ((#setTrue_P==1 || \#setTrue_Q == 1) -> AF (#critical_P == 1 || \#critical_Q == 1)) +AG (#setTrue_P==1 -> AF (#critical_P == 1)) +AG (#setTrue_Q==1 -> AF (#critical_Q == 1)) +#+END_SRC +Inoltre, per confermare alcune ipotesi, si e` testata anche la +seguente formula CTL: +| AG(#setTrue_P == 1 -> EF(#critical_Q==1 || \#critical_P == 1)) +che conferma la presenza di deadlock causata dalle due variabili +booleane. +[[./3.9.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 | + +Il deadlock si verifica quando i entrambe le variabili booleane sono +uguali a /true/. +Ad esempio, se si esegue in locksetop il loop con la +condizione booleana sulla variabile dell'altro processo, si verifica +la condizione di deadlock. +Viene riportato il trace di NuSMV che conferma questa ipotesi. +GreatSPN fallisce per mancanza di RAM sulla macchina usata ma e` +facile riprodurre il deadlock manualmente. +#+BEGIN_SRC +-- specification AG ((p.state = setTrue | q.state = setTrue) -> AF (p.state = critical | q.state = critical)) is false +-- as demonstrated by the following execution sequence +Trace Description: CTL Counterexample +Trace Type: Counterexample + -> State: 1.1 <- + wantP = FALSE + wantQ = FALSE + p.state = local + q.state = local + -> Input: 1.2 <- + _process_selector_ = p + running = FALSE + q.running = FALSE + p.running = TRUE + -> State: 1.2 <- + p.state = setTrue + -> Input: 1.3 <- + -> State: 1.3 <- + wantP = TRUE + p.state = critical + -> Input: 1.4 <- + -> State: 1.4 <- + p.state = setFalse + -> Input: 1.5 <- + _process_selector_ = q + q.running = TRUE + p.running = FALSE + -> State: 1.5 <- + q.state = setTrue + -> Input: 1.6 <- + -> State: 1.6 <- + wantQ = TRUE + q.state = resetFalse + -> Input: 1.7 <- + _process_selector_ = p + q.running = FALSE + p.running = TRUE + -> State: 1.7 <- + wantP = FALSE + p.state = local + -> Input: 1.8 <- + -> State: 1.8 <- + p.state = setTrue + -> Input: 1.9 <- + -- Loop starts here + -> State: 1.9 <- + wantP = TRUE + p.state = resetFalse + -> Input: 1.10 <- + _process_selector_ = q + q.running = TRUE + p.running = FALSE + -> State: 1.10 <- + wantQ = FALSE + q.state = resetTrue + -> Input: 1.11 <- + -- Loop starts here + -> State: 1.11 <- + wantQ = TRUE + q.state = resetFalse + -> Input: 1.12 <- + _process_selector_ = p + q.running = FALSE + p.running = TRUE + -> State: 1.12 <- + wantP = FALSE + p.state = resetTrue + -> Input: 1.13 <- + -- Loop starts here + -> State: 1.13 <- + wantP = TRUE + p.state = resetFalse + -> Input: 1.14 <- + _process_selector_ = q + q.running = TRUE + p.running = FALSE + -> State: 1.14 <- + wantQ = FALSE + q.state = resetTrue + -> Input: 1.15 <- + -- Loop starts here + -> State: 1.15 <- + wantQ = TRUE + q.state = resetFalse + -> Input: 1.16 <- + _process_selector_ = p + q.running = FALSE + p.running = TRUE + -> State: 1.16 <- + wantP = FALSE + p.state = resetTrue + -> Input: 1.17 <- + -> State: 1.17 <- + wantP = TRUE + p.state = resetFalse +#+END_SRC +Di seguito il trace che conferma la presenza di starvation +individuale, sia in GreatSPN che NuSMV. +#+BEGIN_SRC +Generated counter-example: +==================================== Trace ==================================== +Initial state is: local_Q(1), wantQ_FALSE(1), wantP_FALSE(1), local_P(1) +Initial state satisfies: E F (not ((not (setTrue_Q = 1)) or (not E G (not (critical_Q = 1))))). + +1: local_Q(1), wantQ_FALSE(1), wantP_FALSE(1), local_P(1) + State 1. satisfies: ((not (setTrue_Q = 1)) or (not E G (not (critical_Q = 1)))). + + 1.1: local_Q(1), wantQ_FALSE(1), wantP_FALSE(1), local_P(1) + State 1.1. does not satisfy: (setTrue_Q = 1). + +2: setTrue_Q(1), wantQ_FALSE(1), wantP_FALSE(1), local_P(1) + State 2. does not satisfy: ((not (setTrue_Q = 1)) or (not E G (not (critical_Q = 1)))). + + 2.1: setTrue_Q(1), wantQ_FALSE(1), wantP_FALSE(1), local_P(1) + State 2.1.L. satisfies: (setTrue_Q = 1). + + State 2.1.R. satisfies: E G (not (critical_Q = 1)). Start of loop. + + 2.1.R.1: setTrue_Q(1), wantQ_FALSE(1), wantP_FALSE(1), local_P(1) + State 2.1.R.1. does not satisfy: (critical_Q = 1). + + 2.1.R.2: loop back to state 2.1.R.1. +#+END_SRC +#+BEGIN_SRC +-- specification AG (q.state = setTrue -> AF q.state = critical) is false +-- as demonstrated by the following execution sequence +Trace Description: CTL Counterexample +Trace Type: Counterexample + -> State: 3.1 <- + wantP = FALSE + wantQ = FALSE + p.state = local + q.state = local + -> Input: 3.2 <- + _process_selector_ = q + running = FALSE + q.running = TRUE + p.running = FALSE + -> State: 3.2 <- + q.state = setTrue + -> Input: 3.3 <- + _process_selector_ = p + q.running = FALSE + p.running = TRUE + -> State: 3.3 <- + p.state = setTrue + -> Input: 3.4 <- + -> State: 3.4 <- + wantP = TRUE + p.state = critical + -> Input: 3.5 <- + _process_selector_ = q + q.running = TRUE + p.running = FALSE + -> State: 3.5 <- + wantQ = TRUE + q.state = resetFalse + -> Input: 3.6 <- + _process_selector_ = p + q.running = FALSE + p.running = TRUE + -- Loop starts here + -> State: 3.6 <- + p.state = setFalse + -> Input: 3.7 <- + _process_selector_ = main + running = TRUE + p.running = FALSE + -- Loop starts here + -> State: 3.7 <- + -> Input: 3.8 <- + _process_selector_ = q + running = FALSE + q.running = TRUE + -> State: 3.8 <- + wantQ = FALSE + q.state = resetTrue + -> Input: 3.9 <- + _process_selector_ = p + q.running = FALSE + p.running = TRUE + -> State: 3.9 <- + wantP = FALSE + p.state = local + -> Input: 3.10 <- + -> State: 3.10 <- + p.state = setTrue + -> Input: 3.11 <- + -> State: 3.11 <- + wantP = TRUE + p.state = critical + -> Input: 3.12 <- + _process_selector_ = q + q.running = TRUE + p.running = FALSE + -> State: 3.12 <- + wantQ = TRUE + q.state = resetFalse + -> Input: 3.13 <- + _process_selector_ = p + q.running = FALSE + p.running = TRUE + -> State: 3.13 <- + p.state = setFalse +#+END_SRC