diff --git a/anno3/vpc/consegne/3/.#3.2.b.smv b/anno3/vpc/consegne/3/.#3.2.b.smv deleted file mode 120000 index 6d16a97..0000000 --- a/anno3/vpc/consegne/3/.#3.2.b.smv +++ /dev/null @@ -1 +0,0 @@ -user@thinkgentoo.14302:1588838104 \ No newline at end of file diff --git a/anno3/vpc/consegne/3/3.6-Measures.solution/PT.bnd b/anno3/vpc/consegne/3/3.6-Measures.solution/PT.bnd new file mode 100644 index 0000000..f845088 --- /dev/null +++ b/anno3/vpc/consegne/3/3.6-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.6-Measures.solution/PT.ctl b/anno3/vpc/consegne/3/3.6-Measures.solution/PT.ctl new file mode 100644 index 0000000..bfc8e84 --- /dev/null +++ b/anno3/vpc/consegne/3/3.6-Measures.solution/PT.ctl @@ -0,0 +1,8 @@ +% MEASURE1 +AG(!(#critical_P == 1) || !(#critical_Q == 1)) +% MEASURE2 +AG ((#await_P==1 || #await_Q == 1) -> AF (#critical_P == 1 || #critical_Q == 1)) +% MEASURE3 +AG(#await_P == 1 -> EF(#critical_Q==1 || #critical_P == 1)) +% MEASURE4 +AG (#await_P==1 -> AF (#critical_P == 1)) diff --git a/anno3/vpc/consegne/3/3.6-Measures.solution/PT.def b/anno3/vpc/consegne/3/3.6-Measures.solution/PT.def new file mode 100644 index 0000000..f9eee66 --- /dev/null +++ b/anno3/vpc/consegne/3/3.6-Measures.solution/PT.def @@ -0,0 +1,3 @@ +|256 +% +| diff --git a/anno3/vpc/consegne/3/3.6-Measures.solution/PT.ilpbnd b/anno3/vpc/consegne/3/3.6-Measures.solution/PT.ilpbnd new file mode 100644 index 0000000..aa47d0d --- /dev/null +++ b/anno3/vpc/consegne/3/3.6-Measures.solution/PT.ilpbnd @@ -0,0 +1,2 @@ +0 +0 diff --git a/anno3/vpc/consegne/3/3.6-Measures.solution/PT.net b/anno3/vpc/consegne/3/3.6-Measures.solution/PT.net new file mode 100644 index 0000000..8894082 --- /dev/null +++ b/anno3/vpc/consegne/3/3.6-Measures.solution/PT.net @@ -0,0 +1,90 @@ +|0| +| +f 0 14 0 10 0 0 0 +local_P 1 2.6666666666666665 1.0 2.9612499999999997 0.945625 0 +await_P 0 2.6666666666666665 2.3333333333333335 2.8518749999999997 2.1122916666666667 0 +SetTrue_P 0 2.6666666666666665 3.6666666666666665 2.857083333333333 3.6122916666666662 0 +critical_P 0 2.6666666666666665 5.166666666666667 3.0549999999999997 5.278958333333333 0 +setFalse_P 0 2.6666666666666665 6.666666666666667 2.857083333333333 6.695625 0 +wantP_FALSE 1 5.166666666666667 6.5 4.716458333333333 6.695625 0 +wantP_TRUE 0 4.0 6.166666666666667 4.320625 6.028958333333333 0 +wantQ_FALSE 1 6.0 2.3333333333333335 5.794583333333333 2.6122916666666667 0 +wantQ_TRUE 0 7.166666666666667 2.3333333333333335 6.39875 1.945625 0 +setFalse_Q 0 8.333333333333334 2.1666666666666665 8.518541666666666 2.3622916666666667 0 +critical_Q 0 8.333333333333334 3.6666666666666665 8.627916666666666 3.8622916666666662 0 +setTrue_Q 0 8.333333333333334 5.166666666666667 8.695625 5.195625 0 +await_Q 0 8.333333333333334 6.166666666666667 8.096666666666666 6.362291666666667 0 +local_Q 1 8.333333333333334 7.5 8.700833333333334 7.112291666666667 0 +T0 1.0 0 0 1 0 2.6666666666666665 1.6666666666666667 2.6458333333333335 1.4739583333333333 2.75 1.734375 0 + 1 1 0 0 + 1 + 1 2 0 0 + 0 +T8 1.0 0 0 2 0 2.6666666666666665 7.5 2.6458333333333335 7.307291666666667 2.75 7.567708333333333 0 + 1 5 1 0 +2.6666666666666665 7.25 + 1 7 0 0 + 2 + 1 1 2 0 +0.75 7.5 +0.75 1.0 + 1 6 1 0 +5.166666666666667 7.5 + 0 +T3 1.0 0 0 1 0 2.6666666666666665 5.833333333333333 2.6458333333333335 5.640625 2.75 5.901041666666667 0 + 1 4 0 0 + 1 + 1 5 0 0 + 0 +T1 1.0 0 0 2 0 2.6666666666666665 3.0 2.6458333333333335 2.8072916666666665 2.75 3.0677083333333335 0 + 1 2 0 0 + 1 8 0 0 + 2 + 1 3 0 0 + 1 8 1 0 +5.166666666666667 2.3333333333333335 + 0 +T2 1.0 0 0 2 0 2.6666666666666665 4.5 2.6458333333333335 4.307291666666667 2.75 4.567708333333333 0 + 1 3 0 0 + 1 6 1 0 +5.166666666666667 4.5 + 2 + 1 4 0 0 + 1 7 0 0 + 0 +T5 1.0 0 0 2 0 8.333333333333334 1.1666666666666667 8.3125 0.9739583333333334 8.416666666666666 1.234375 0 + 1 10 0 0 + 1 9 0 0 + 2 + 1 14 2 0 +10.0 1.1666666666666667 +10.0 7.5 + 1 8 1 0 +6.0 1.1666666666666667 + 0 +T6 1.0 0 0 1 0 8.333333333333334 6.833333333333333 8.3125 6.640625 8.416666666666666 6.901041666666667 0 + 1 14 0 0 + 1 + 1 13 0 0 + 0 +T7 1.0 0 0 2 0 8.333333333333334 5.666666666666667 8.3125 5.473958333333333 8.416666666666666 5.734375 0 + 1 13 0 0 + 1 6 0 0 + 2 + 1 12 0 0 + 1 6 1 0 +6.333333333333333 5.916666666666667 + 0 +T9 1.0 0 0 2 0 8.333333333333334 4.5 8.3125 4.307291666666667 8.416666666666666 4.567708333333333 0 + 1 12 0 0 + 1 8 1 0 +6.0 4.5 + 2 + 1 11 0 0 + 1 9 0 0 + 0 +T10 1.0 0 0 1 0 8.333333333333334 2.8333333333333335 8.286458333333334 2.640625 8.416666666666666 2.9010416666666665 0 + 1 11 0 0 + 1 + 1 10 0 0 + 0 diff --git a/anno3/vpc/consegne/3/3.6-Measures.solution/PT.pba b/anno3/vpc/consegne/3/3.6-Measures.solution/PT.pba new file mode 100644 index 0000000..aa74978 --- /dev/null +++ b/anno3/vpc/consegne/3/3.6-Measures.solution/PT.pba @@ -0,0 +1,8 @@ +6 +5 1 1 1 2 1 3 1 4 1 5 +4 1 1 1 2 1 3 1 7 +4 -1 1 -1 2 -1 3 1 6 +5 1 10 1 11 1 12 1 13 1 14 +3 1 9 -1 10 -1 11 +3 1 8 1 10 1 11 +0 diff --git a/anno3/vpc/consegne/3/3.6-Measures.solution/PT.pin b/anno3/vpc/consegne/3/3.6-Measures.solution/PT.pin new file mode 100644 index 0000000..1fcd58d --- /dev/null +++ b/anno3/vpc/consegne/3/3.6-Measures.solution/PT.pin @@ -0,0 +1,10 @@ +8 +5 1 10 1 11 1 12 1 13 1 14 +4 1 9 1 12 1 13 1 14 +3 1 8 1 10 1 11 +2 1 8 1 9 +5 1 1 1 2 1 3 1 4 1 5 +4 1 1 1 2 1 3 1 7 +3 1 4 1 5 1 6 +2 1 6 1 7 +0 diff --git a/anno3/vpc/consegne/3/3.6.PNPRO b/anno3/vpc/consegne/3/3.6.PNPRO new file mode 100644 index 0000000..f12252b --- /dev/null +++ b/anno3/vpc/consegne/3/3.6.PNPRO @@ -0,0 +1,133 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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 + + diff --git a/anno3/vpc/consegne/3/3.6.b.smv b/anno3/vpc/consegne/3/3.6.b.smv new file mode 100644 index 0000000..619d191 --- /dev/null +++ b/anno3/vpc/consegne/3/3.6.b.smv @@ -0,0 +1,43 @@ +MODULE main +VAR + wantP: boolean; + wantQ: boolean; + p: process proc(wantP, wantQ); + 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 = 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, await}; + state = await & other = FALSE: setTrue; + state = await: await; + state = setTrue: critical; + state = critical: setFalse; + state = setFalse: local; + esac; + next(mine) := case + state = setTrue: TRUE; + state = setFalse: FALSE; + TRUE: mine; + 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 index 8c6aaba..e002294 100644 --- a/anno3/vpc/consegne/3/3.6.smv +++ b/anno3/vpc/consegne/3/3.6.smv @@ -33,9 +33,6 @@ CTLSPEC 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 diff --git a/anno3/vpc/consegne/3/analisi.org b/anno3/vpc/consegne/3/analisi.org index 2e53900..b35fade 100644 --- a/anno3/vpc/consegne/3/analisi.org +++ b/anno3/vpc/consegne/3/analisi.org @@ -29,6 +29,9 @@ Nella tabella mostriamo i risultati ottenuti - [ ] Vedi necessita` di Sync e / - [ ] Finisci tutto con algebra dei processi - [ ] Reachability graph vs Derivation Graph +- [ ] 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? * TODO Proprieta` del modello @@ -73,7 +76,7 @@ processi un'enumerazione di 4 stati ed una variabile turno di tipo intero. 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 || \#Wait_Q == 1) -> AF (#Critical_P == 1 || \#Critical_Q == 1)) = false AG (#Wait_P==1 -> AF (#Critical_P == 1)) = false #+END_SRC [[./3.2.jpg]] @@ -213,10 +216,39 @@ while true: ** NuSMV Si e` deciso di modellare l'algoritmo usando per ognuno dei due -processi ... -| CODE +processi usando 5 stati per ogni processo +| state: {local, await, critical, setTrue, setFalse}; #+include 3.6.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)) +#+END_SRC + ** TODO CCS -** Risultati +** TODO Risultati +Nella tabella mostriamo i risultati ottenuti +| | NuSMV | GreatSPN | +|---------------------+-------+----------| +| Mutua Esclusione | false | false | +| Assenza di deadlock | true | false | +| No Starvation | true | false | + +L'incoerenza del risultato dell'assenza di deadlock e` spiegabile dal +fatto che nel caso di NuSMV non e` possibile che un processo rimanga +nel primo stato (/local/) per un tempo indefinito mentre nel caso di +GreatSPN e` possibile che il processo P vada nello spazio await e il +processo Q decida di rimanere nel loop /local_Q/ all'infinito. +Notiamo che se forziamo i processi a fare del progresso dallo stato +/local/, allora la formula CTL +| G(wₚ → F(cₚ∨c_{q}) +risulta rispettata. +Ancora meglio, piuttosto che rimuovere una transizione possibile, +possiamo restringere la verifica dell'assenza di deadlock alla +seguente formula CTL +| AG (wₚ → EF (cₚ || c_{q})) +| AG(#await_P == 1 -> EF(#critical_Q==1 || \#critical_P == 1)) +che risulta rispettata.