The contract as a whole

Domain

The domain model as a UML class diagram: base types (Role / Asset / Event / DataTransfer), inheritance, «Enumeration» and «thirdParty» stereotypes, and named associations for domain-typed attributes.

Parties & norms

Parties (blue) with obligations (solid) and powers (dashed), debtor → creditor. Rules (yellow) point to their To role: green = Grant, red = Revoke, labelled with the permission.

Access policy

Roles (rows) × resources (columns). Policy controller: regulator.

• Rule1: pfizer grants mcdc read access to vaccineDose
• Rule2: pfizer grants worldcourier read access to vaccineDose.FDAapproval
• Rule3: pfizer grants mcdc read access to delivered
• Rule4: regulator revokes pfizer write access on temperature.value
• Rule5: regulator revokes pfizer write access on humidity.value
• Rule6: regulator revokes pfizer write access on shock.value
• Rule7: regulator revokes pfizer write access on lightExposure.value
• Rule8: regulator revokes pfizer write access on sealOpen.value
• Rule9: fda grants pfizer read access to withdrewApproval

Obligations

Rule: oRequestVaccineDosage
  Obligation: mcdc owes pfizer.
  Refers to oAgreedOnRequest, oDeliver, oAssign.
  Referred to by pTermination.
  # Specifier's note: To keep the contract in active state until the remain doses is less than the minimum requested quantity (end of performance) and the mcdc and pfizer terminate the agreement

  Scenario: oRequestVaccineDosage is fulfilled
    Given the contract is in force
    When "remain.value" is less than "minQuantity"
    And obligation "oAgreedOnRequest" has been fulfilled
    And obligation "oDeliver" has been fulfilled
    And obligation "oAssign" has been fulfilled
    And "mcdc" declares the agreement terminated ("mcdcTerminateAgreement")
    And "pfizer" declares the agreement terminated ("pfizerTerminateAgreement")
    Then obligation "oRequestVaccineDosage" is fulfilled

  Scenario: oRequestVaccineDosage is violated
    Given the contract is in force
    When any of the required conditions does not come about
    Then obligation "oRequestVaccineDosage" is violated

Rule: oAgreedOnRequest
  Obligation: mcdc owes pfizer.
  Referred to by oRequestVaccineDosage, oDeliver.
  # Specifier's note: A Request must satisfy all the conditions required in a particular order

  Scenario: oAgreedOnRequest is fulfilled
    Given "mcdc" submits a request ("requested")
    And "mcdc" agrees ("agreedFromG")
    When "pfizer" informs the negotiated lead time ("leadtimeINform") strictly before "agreedFromG"
    And "leadtimeINform", "requested", and "agreedFromG" all refer to the same "reqID"
    And "requested.dosage" is between "minQuantity" and "remain.value"
    Then obligation "oAgreedOnRequest" is fulfilled

  Scenario: oAgreedOnRequest is violated
    Given "mcdc" submits a request ("requested")
    And "mcdc" agrees ("agreedFromG")
    When any of the required conditions does not come about
    Then obligation "oAgreedOnRequest" is violated

Rule: oDeliver
  Obligation: pfizer owes mcdc.
  Access administered by regulator.
  Refers to oAgreedOnRequest.
  Referred to by oRequestVaccineDosage, oAssign, oPay.
  Access rule Rule1: pfizer grants mcdc read access to vaccineDose.
  Access rule Rule2: pfizer grants worldcourier read access to vaccineDose.FDAapproval.
  Access rule Rule3: pfizer grants mcdc read access to delivered.
  Access rule Rule4: regulator revokes pfizer write access on temperature.value.
  Access rule Rule5: regulator revokes pfizer write access on humidity.value.
  Access rule Rule6: regulator revokes pfizer write access on shock.value.
  Access rule Rule7: regulator revokes pfizer write access on lightExposure.value.
  Access rule Rule8: regulator revokes pfizer write access on sealOpen.value.

  Scenario: oDeliver is fulfilled
    Given "mcdc" submits a request ("requested")
    And obligation "oAgreedOnRequest" has been fulfilled
    And "mcdc" confirms ("confirmed")
    When "pfizer" gives notice of the delivery date ("notifiedOD") strictly before "confirmed"
    And "worldcourier" delivers ("delivered")
    And "delivered.delAddr" equals "confirmed.shipToLocation"
    And "vaccineDose.FDAapproval" holds
    And "delivered", "requested", "notifiedOD", and "confirmed" all refer to the same "reqID"
    And either "delivered.date" equals "notifiedOD.delD" or "pfizer" declares an outside risk ("outsideRisk"), "delivered.date" equals "outsideRisk.extendedDel", and "requested" and "outsideRisk" refer to the same "reqID"
    And no "temperature", "sealOpen", "humidity", "shock", or "lightExposure" alert occurs for the same "reqID" as "requested"
    Then obligation "oDeliver" is fulfilled

  Scenario: oDeliver is violated
    Given "mcdc" submits a request ("requested")
    And obligation "oAgreedOnRequest" has been fulfilled
    And "mcdc" confirms ("confirmed")
    When any of the required conditions does not come about
    Then obligation "oDeliver" is violated

Rule: oAssign
  Obligation: mcdc owes pfizer.
  Refers to oDeliver.
  Referred to by oRequestVaccineDosage.
  Access rule Rule1: pfizer grants mcdc read access to vaccineDose.
  Access rule Rule3: pfizer grants mcdc read access to delivered.
  # Specifier's note: Calculate the remains of the doses and the price of the doses delivered when the required doses are delivered, fulfilling all the agreed-upon conditions

  Scenario: oAssign is fulfilled
    Given "mcdc" submits a request ("requested")
    And "worldcourier" delivers ("delivered")
    And "delivered" and "requested" refer to the same "reqID"
    When when obligation "oDeliver" has been fulfilled, "remain.value" is reduced by "delivered.dosage" and "paidAmount.value" is set to "delivered.dosage" × "vaccineDose.price"
    And "delivered" and "requested" refer to the same "reqID"
    Then obligation "oAssign" is fulfilled

  Scenario: oAssign is violated
    Given "mcdc" submits a request ("requested")
    And "worldcourier" delivers ("delivered")
    And "delivered" and "requested" refer to the same "reqID"
    When any of the required conditions does not come about
    Then obligation "oAssign" is violated

Surviving obligations

These remain enforceable after the contract has ended.

Rule: oPay
  Surviving obligation (still owed after the contract ends): mcdc owes pfizer.
  Refers to oDeliver.
  Access rule Rule1: pfizer grants mcdc read access to vaccineDose.
  Access rule Rule2: pfizer grants worldcourier read access to vaccineDose.FDAapproval.
  Access rule Rule3: pfizer grants mcdc read access to delivered.
  # Specifier's note: Checking the agreed terms necessary to activate and complete the payment process

  Scenario: oPay is fulfilled
    Given "mcdc" submits a request ("requested")
    And "mcdc" records an invoice ("invoiced")
    And "vaccineDose.FDAapproval" holds
    And "invoiced", "requested", and "delivered" all refer to the same "reqID"
    And obligation "oDeliver" has been fulfilled
    And "worldcourier" delivers ("delivered") strictly before "invoiced"
    When "mcdc" pays ("paid") strictly before 30 days after "invoiced.date"
    And "invoiced", "requested", and "paid" all refer to the same "reqID"
    And "paid.amount" equals "paidAmount.value"
    Then obligation "oPay" is fulfilled

  Scenario: oPay is violated
    Given "mcdc" submits a request ("requested")
    And "mcdc" records an invoice ("invoiced")
    And "vaccineDose.FDAapproval" holds
    And "invoiced", "requested", and "delivered" all refer to the same "reqID"
    And obligation "oDeliver" has been fulfilled
    And "worldcourier" delivers ("delivered") strictly before "invoiced"
    When "paid" does not occur strictly before 30 days after "invoiced.date"
    Then obligation "oPay" is violated

Rule: oWithdrewApproval
  Surviving obligation (still owed after the contract ends): pfizer owes mcdc.
  Access rule Rule1: pfizer grants mcdc read access to vaccineDose.
  Access rule Rule2: pfizer grants worldcourier read access to vaccineDose.FDAapproval.
  Access rule Rule9: fda grants pfizer read access to withdrewApproval.
  # Specifier's note: FDA approval monitoring where mcdc must pay for vaccine doses already approved by FDA

  Scenario: oWithdrewApproval is fulfilled
    Given "fda" withdraws approval ("withdrewApproval")
    When "vaccineDose.FDAapproval" is set to false
    Then obligation "oWithdrewApproval" is fulfilled

  Scenario: oWithdrewApproval is violated
    Given "fda" withdraws approval ("withdrewApproval")
    When any of the required conditions does not come about
    Then obligation "oWithdrewApproval" is violated

Powers

Rule: pStopWork
  Power held by mcdc against pfizer.
  # Specifier's note: mcdc has the power to stop the work if one of the following four events occurs

  Scenario Outline: pStopWork is exercised
    Given "<party>" issues a stop-work order ("<event>")
    When "mcdc" issues a stop-work order ("govStopWork")
    Then the contract is terminated
    Examples:
      | party | event |
      | mcdc | lawStopWork |
      | regulator | adminStopWork |
      | regulator | regulationStopWork |
      | regulator | judicialStopWork |

Rule: pTermination
  Power held by pfizer against mcdc.
  Refers to oRequestVaccineDosage.
  # Specifier's note: Terminate the contract at the end of the performance

  Scenario: pTermination is exercised
    Given obligation "oRequestVaccineDosage" has been fulfilled
    When "pfizer" exercises the power
    Then the contract is terminated

Specification

The SymboleoAC source this documentation was generated from, coloured as in the editor. Identifiers in the text above jump to their declaration here; inside the source, references are linked to their declarations.

1Domain covidVaccineProcurementD2  Manufacturer isA Role with name: String, org: String, dept: String;3  Government isA Role with name: String, org: String, dept: String;4  Regulator isA Role thirdParty with name: String, org: String, dept: String;5  WorldCourier isA Role thirdParty with name: String, org: String, dept: String;6  FDA isA Role thirdParty with name: String, org: String, dept: String;7  Invoiced isA Event with Env reqID : String, Env noOfDoses : Number, Env date : Date,  performer: Government, controller: Government;8  Paid isA Event with Env reqID : String, Env amount : Number, performer: Government, controller: Government;9  Requested isA Event with Env reqID : String, Env dosage : Number, Env date : Date, performer: Government, controller: Government;10  LeadtimeInformedNegotiated isA Event with Env reqID : String, Env date : Date, performer: Manufacturer, controller: Manufacturer;11  NotifiedOfDelivery isA Event with Env reqID : String, Env delD : Date, performer: Manufacturer, controller: Manufacturer;12  Location isAn Enumeration(Ottawa, Toronto, Montrial, Vancover);13  Confirmed isA Event with Env reqID : String, Env shipToLocation: Location, performer: Government, controller: Government;14  Delivered isA Event with Env reqID : String, Env dosage : Number, Env delAddr : Location, Env date: Date, performer: WorldCourier, controller: Manufacturer;15  VaccineDose isA Asset with  price : Number, FDAapproval : Boolean, owner: Manufacturer;16  StopWork isA Event with performer: Government, controller: Government;17  ThirdPartyStopWork isA Event with performer: Regulator, controller: Regulator;18  Agreed isA Event with Env reqID: String, performer: Government, controller: Government;19  Risk isA Event with Env reqID: String, Env extendedDel: Date, performer: Manufacturer, controller: Manufacturer;20  Remain isA Asset with value:Number, owner: Government;21  PaidAmount isA Asset with value:Number, owner: Government;22  WithdrewApproval isA Event with performer: FDA, controller: FDA;23  TerminateAgreementG isA Event with performer: Government, controller: Government;24  TerminateAgreementM isA Event with performer: Manufacturer, controller: Manufacturer;25  Alert isA DataTransfer with Env value: Number, Env sensorTimestamp:String, condition: String, window: String, count: String, Env reqID : String, controller:Manufacturer, performer:Regulator;26 27endDomain 28  29TimeGranularity is days30Contract VaccineProcurementC (pfizerP :Manufacturer, mcdcP:Government, regulatorP: Regulator, fdaP: FDA, worldcourierP: WorldCourier,31approval : Boolean, unitPrice : Number, minQuantity : Number, maxQuantity:Number)32 33Declarations34  regulator: Regulator with name:= regulatorP.name, org:= regulatorP.org, dept:= regulatorP.dept;35  pfizer: Manufacturer with name:= pfizerP.name, org:= pfizerP.org, dept:= pfizerP.dept;36  mcdc: Government with name:= mcdcP.name, org:= mcdcP.org, dept:= mcdcP.dept;37  fda: FDA with name:= fdaP.name, org:= fdaP.org, dept:= fdaP.dept;38  worldcourier: WorldCourier with name:= worldcourierP.name, org:= worldcourierP.org, dept:= worldcourierP.dept;39 40  requested : Requested  with performer:= mcdc, controller:= mcdc;41  leadtimeINform : LeadtimeInformedNegotiated  with performer:= pfizer, controller:= pfizer;42  notifiedOD : NotifiedOfDelivery  with performer:= pfizer, controller:= pfizer;43  delivered : Delivered  with performer:= worldcourier, controller:= pfizer;44  invoiced : Invoiced with performer:= mcdc, controller:= mcdc;45  paid : Paid with performer:= mcdc, controller:= mcdc;46  confirmed: Confirmed with performer:= mcdc, controller:= mcdc;47  lawStopWork: StopWork with performer:= mcdc, controller:= mcdc;48  regulationStopWork:ThirdPartyStopWork with performer:= regulator, controller:= regulator;49  judicialStopWork:ThirdPartyStopWork with performer:= regulator, controller:= regulator;50  adminStopWork: ThirdPartyStopWork with performer:= regulator, controller:= regulator;51  govStopWork: StopWork with performer:= mcdc, controller:= mcdc;52  vaccineDose : VaccineDose with  price := unitPrice, FDAapproval := approval, owner:=pfizer;53  agreedFromG: Agreed with performer:= mcdc, controller:= mcdc;54  outsideRisk: Risk with performer:= pfizer, controller:= pfizer;55  remain: Remain with value:= maxQuantity, owner:=mcdc;56  paidAmount:PaidAmount with value:=0, owner:=mcdc;57  withdrewApproval: WithdrewApproval  with performer:= fda, controller:= fda;58  mcdcTerminateAgreement: TerminateAgreementG with performer:= mcdc, controller:= mcdc;59  pfizerTerminateAgreement: TerminateAgreementM with performer:= pfizer, controller:= pfizer;60  // sensors61  temperature: Alert with condition := "value > -80", window := "10", count := "5", controller := pfizer, performer := regulator;62  humidity : Alert with condition := "value > 70", window := "15", count := "3", controller := pfizer, performer := regulator;63  shock : Alert with condition := "value > 5",  window := "", count := "", controller := pfizer, performer := regulator;64  lightExposure : Alert with condition := "value > 0",  window := "", count := "", controller := pfizer, performer := regulator;65  sealOpen : Alert with condition := "value > 0", window := "",  count := "", controller := pfizer, performer := regulator;66 67Preconditions68  vaccineDose.FDAapproval==true;69 70Obligations71// To keep the contract in active state until the remain doses is less than the minimum requested quantity (end of performance) and the mcdc and pfizer terminate the agreement72  oRequestVaccineDosage: O(mcdc, pfizer,73    true,74    (remain.value < minQuantity)75      and Happens(Fulfilled(obligations.oAgreedOnRequest))76      and Happens(Fulfilled(obligations.oDeliver))77      and Happens(Fulfilled(obligations.oAssign))78      and Happens(mcdcTerminateAgreement)79      and Happens(pfizerTerminateAgreement)80  ); // 3.281 82 // A Request must satisfy all the conditions required in a particular order83  oAgreedOnRequest: Happens(requested) -> O(mcdc, pfizer,84    Happens(agreedFromG),85    ShappensBefore(leadtimeINform, agreedFromG)86      and leadtimeINform.reqID == requested.reqID87      and agreedFromG.reqID == requested.reqID88      and (requested.dosage >= minQuantity and requested.dosage <= remain.value)89  );90 91 // A delivery obligation is achieved if the delivering operation satisfies all the conditions required in a particular order92 // and (delivered.temperature <= temperature) // and Happens(Fulfilled(obligations.oMonitorColdChain))93  oDeliver: Happens(requested) -> O(pfizer, mcdc,94    Happens(Fulfilled(obligations.oAgreedOnRequest))95      and Happens(confirmed),96    ShappensBefore(notifiedOD, confirmed)97      and Happens(delivered)98      and delivered.delAddr == confirmed.shipToLocation99      and vaccineDose.FDAapproval == true100      and delivered.reqID == requested.reqID101      and notifiedOD.reqID == requested.reqID102      and confirmed.reqID == requested.reqID103      and ((delivered.date == notifiedOD.delD) or (Happens(outsideRisk) and delivered.date == outsideRisk.extendedDel and requested.reqID == outsideRisk.reqID))104      and (not Happens(temperature) or temperature.reqID != requested.reqID)105      and (not Happens(sealOpen) or sealOpen.reqID != requested.reqID)106      and (not Happens(humidity) or humidity.reqID != requested.reqID)107      and (not Happens(shock) or shock.reqID != requested.reqID)108      and (not Happens(lightExposure) or lightExposure.reqID != requested.reqID)109  ) with Controller regulator;110 111  // Calculate the remains of the doses and the price of the doses delivered when the required doses are delivered, fulfilling all the agreed-upon conditions 											112  oAssign: Happens(requested) -> O(mcdc, pfizer,113    Happens(delivered)114      and delivered.reqID == requested.reqID,115    HappensAssign(Fulfilled(obligations.oDeliver), remain.value := remain.value - delivered.dosage; paidAmount.value := delivered.dosage * vaccineDose.price)116      and delivered.reqID == requested.reqID117  );118 119Surviving Obligations120// Checking the agreed terms necessary to activate and complete the payment process121  oPay: Happens(requested) -> Obligation(mcdc, pfizer,122    Happens(invoiced)123      and vaccineDose.FDAapproval == true124      and invoiced.reqID == requested.reqID125      and Happens(Fulfilled(obligations.oDeliver))126      and ShappensBefore(delivered, invoiced)127      and delivered.reqID == requested.reqID,128    ShappensBefore(paid, Date.add(invoiced.date, 30, days))129      and invoiced.reqID == requested.reqID130      and invoiced.reqID == paid.reqID131      and paid.amount == paidAmount.value132  )	;133 134// FDA approval monitoring where mcdc must pay for vaccine doses already approved by FDA					135  oWithdrewApproval: O(pfizer, mcdc,136    Happens(withdrewApproval),137    Assign(vaccineDose.FDAapproval := false)138  );139 140Powers141// mcdc has the power to stop the work if one of the following four events occurs142  pStopWork: Happens(lawStopWork) or Happens(adminStopWork) or Happens(regulationStopWork) or Happens(judicialStopWork) -> P(mcdc, pfizer,143    Happens(govStopWork),144    Terminated(self)145  );146 147// Terminate the contract at the end of the performance148  pTermination: Happens(Fulfilled(obligations.oRequestVaccineDosage)) -> P(pfizer, mcdc,149    true,150    Terminated(self)151  );152 153ACPolicy with Controller regulator154  Rule1: Grant read To mcdc On vaccineDose by pfizer; // give read permission to government to read information vaccineDose155  Rule2: Grant read To worldcourier On vaccineDose.FDAapproval by pfizer;156  Rule3: Grant read To mcdc On delivered by pfizer;157  Rule4: Revoke write To pfizer On temperature.value by regulator; // we took the right of controller to write (constraint)158  Rule5: Revoke write To pfizer On humidity.value by regulator;159  Rule6: Revoke write To pfizer On shock.value by regulator;160  Rule7: Revoke write To pfizer On lightExposure.value by regulator;161  Rule8: Revoke write To pfizer On sealOpen.value by regulator;162  Rule9: Grant read To pfizer On withdrewApproval by fda; // permission by FDA to mcde to see the state163endContract164