module Contexts where
open import Notation
open import Data.Product
open import Relation.Unary  as R1
open import Relation.Binary as R2

module C-Global where
  postulate
    Time : Set
    next : Time  Time
    prev : Time  Time

  Always :  {l}(P : Time  Set l)  Set _
  Always P = (t : Time)  P t

  postulate
    ⟨_⟩FunctionalˍDesignˍDocument     : Set  Set
    ⟨_⟩FunctionˍImplementationˍRecord : Set  Set
    ⟨_⟩FunctionˍTestˍReport           : Set  Set
    ⟨_⟩FunctionˍOperationˍLog         : Set  Set

  record ⟨_⟩FunctionˍDevelopmentˍEvidence(A : Set) : Set where
    field
      functionalˍdesignˍdocument     :  A ⟩FunctionalˍDesignˍDocument
      functionˍimplementationˍrecord :  A ⟩FunctionˍImplementationˍRecord
      functionˍtestˍreport           :  A ⟩FunctionˍTestˍReport

  ⟨_⟩FunctionˍEvidenceˍAuditˍResult : Set  Set
   A ⟩FunctionˍEvidenceˍAuditˍResult =
     A ⟩FunctionˍDevelopmentˍEvidence   A ⟩FunctionˍOperationˍLog  A

  evidenceˍinspection : {A : Set} 
     A ⟩FunctionˍEvidenceˍAuditˍResult
      A ⟩FunctionˍDevelopmentˍEvidence   A ⟩FunctionˍOperationˍLog  A
  evidenceˍinspection f p q = f p q

  module C-ProcedureˍExecution
           {TaskˍGoal : Goal}
           {ProceduralˍDocumentˍforˍTask : Set}
           {ProceduralˍDocumentˍforˍAccountabilityˍAchievement : Set}
           (let Procedure = ProceduralˍDocumentˍforˍTask
                          × ProceduralˍDocumentˍforˍAccountabilityˍAchievement)
           {Performed : Procedure  Goal} where
    Appropriate : Procedure  Goal
    Appropriate x = x is Performed  TaskˍGoal

    record AppropriateˍProcedureˍisˍPerformed : Goal where
      field
        proceduralˍdocumentˍforˍTask
          : ProceduralˍDocumentˍforˍTask
        proceduralˍdocumentˍforˍAccountabilityˍAchievement
          : ProceduralˍDocumentˍforˍAccountabilityˍAchievement
      procedure = (proceduralˍdocumentˍforˍTask
                  , proceduralˍdocumentˍforˍAccountabilityˍAchievement)
      field
        appropriatenessˍevidence : procedure is Appropriate
        executionˍevidence       : procedure is Performed

    procedureˍexecution : AppropriateˍProcedureˍisˍPerformed  TaskˍGoal
    procedureˍexecution p = appropriatenessˍevidence executionˍevidence
      where open AppropriateˍProcedureˍisˍPerformed p

open C-Global

module C-TopˍLevel where
  module atTime(t : Time) where
    postulate
      OrganizationalˍPolicy      : Set
      ServiceˍObjectives         : Set
      Stakeholders′ˍRequirements : Set
      Environement               : Set
      RegulationsˍandˍStandards  : Set
      AdvancementˍofˍTechnology  : Set

    record ExternalˍFactors : Set where
      field
        organizationalˍpolicy      : OrganizationalˍPolicy
        serviceˍobjectives         : ServiceˍObjectives
        stakeholders′ˍrequirements : Stakeholders′ˍRequirements
        enviroment                 : Environement
        regulationˍandˍstandard    : RegulationsˍandˍStandards
        advancementˍofˍtechnology  : AdvancementˍofˍTechnology

    postulate
      OrdinaryˍOperationˍstateˍcanˍbeˍachieved   : Goal
      ChangeˍAccommodationˍCycleˍcanˍbeˍachieved : Goal
      FailureˍResponseˍCycleˍcanˍbeˍachieved     : Goal
      externalˍfactors                           : ExternalˍFactors

  open atTime public

  Serviceˍcontinuityˍandˍaccountabilityˍinˍanˍever-changingˍsystemˍcanˍbeˍachieved
    = Always (OrdinaryˍOperationˍstateˍcanˍbeˍachieved   And
              ChangeˍAccommodationˍCycleˍcanˍbeˍachieved And
              FailureˍResponseˍCycleˍcanˍbeˍachieved)

  decompositionˍtoˍtheˍthreeˍelementsˍofˍDEOSˍProcess :
    Always OrdinaryˍOperationˍstateˍcanˍbeˍachieved
     Always ChangeˍAccommodationˍCycleˍcanˍbeˍachieved
     Always FailureˍResponseˍCycleˍcanˍbeˍachieved
     Serviceˍcontinuityˍandˍaccountabilityˍinˍanˍever-changingˍsystemˍcanˍbeˍachieved
  decompositionˍtoˍtheˍthreeˍelementsˍofˍDEOSˍProcess p q r t = (p t , q t , r t)
    
module C-System where
  data ChangeˍAccommodation-Stage : Set where
    RequirementˍElicitation/RiskˍAnalysis
      Stakeholders′ˍAgreement
      Development/Test
      AccountabilityˍAchievement
        : ChangeˍAccommodation-Stage

  data FailureˍResponse-Stage : Set where
     FailureˍPrevention
       ResponsiveˍAction
       CauseˍAnalysis
       AccountabilityˍAchievement
         : FailureˍResponse-Stage

  data ActivityˍClass : Set where
    OrdinaryˍOperation    : ActivityˍClass
    ChangeˍAccommodation  : ChangeˍAccommodation-Stage  ActivityˍClass
    FailureˍResponse      : FailureˍResponse-Stage      ActivityˍClass

  module atTime(t : Time) where
    postulate 
      SystemˍState  : Set
      ServiceˍLevel : Set

    record MonitoringˍResult : Set where
      field
        systemˍstate  : SystemˍState
        serviceˍlevel : ServiceˍLevel
    postulate
      monitoringˍresult : MonitoringˍResult

    postulate 
      InˍAction : ActivityˍClass  SystemˍState  Proposition

    open MonitoringˍResult monitoringˍresult
    ChangeˍAccommodationˍActivated =
      InˍAction (ChangeˍAccommodation RequirementˍElicitation/RiskˍAnalysis)
                systemˍstate
    FailureˍResponseˍActivated =
      InˍAction (FailureˍResponse FailureˍPrevention) systemˍstate or
      InˍAction (FailureˍResponse ResponsiveˍAction)  systemˍstate
    InˍaˍFailureˍResponse-Stage =
      Σ[ stage  _ ] InˍAction (FailureˍResponse     stage) systemˍstate
    InˍaˍChangeˍAccommodation-Stage =
      Σ[ stage  _ ] InˍAction (ChangeˍAccommodation stage) systemˍstate
    stage = proj₁
  open atTime public

module C-OrdinaryˍOperation(t : Time) where
  module C-RoutineˍOperation where
    open C-System.atTime t
    postulate
      OperationˍRules
        DailyˍInspectionˍGuide
        TrainingˍPlans
        OperationˍSheets
        DailyˍInspectionˍReports
        TrainingˍReports          : Set

    record RoutineˍOperation : Set where
      field
        operationˍrules        : OperationˍRules
        dailyˍinspectionˍguide : DailyˍInspectionˍGuide
        trainingˍplans         : TrainingˍPlans

    postulate
      routineˍoperation  : RoutineˍOperation

    record Performed(x : RoutineˍOperation) : Proposition where
      field
        operationˍsheets         : OperationˍSheets
        dailyˍinspectionˍreports : DailyˍInspectionˍReports
        trainingˍreports         : TrainingˍReports

  module C-ChangeˍMonitoring where
    open C-TopˍLevel.atTime
    open C-System.atTime
    postulate
      Purpose/EnviromentˍChanged₂ :
        ExternalˍFactors (prev t)  ExternalˍFactors t  Proposition

    Purpose/EnviromentˍChanged : Proposition
    Purpose/EnviromentˍChanged =
      Purpose/EnviromentˍChanged₂ (externalˍfactors (prev t))
                                  (externalˍfactors       t )

    Purpose/EnviromentˍChangeˍisˍDetectable : Goal
    Purpose/EnviromentˍChangeˍisˍDetectable =
      Purpose/EnviromentˍChanged₂ is R2.Decidable

    Purpose/EnviromentˍChangeˍDetection =
      Purpose/EnviromentˍChangeˍisˍDetectable

    ChangeˍAccommodationˍisˍReady : Goal
    ChangeˍAccommodationˍisˍReady =
      Purpose/EnviromentˍChanged
       C-System.ChangeˍAccommodationˍActivated (next t)

    ChangeˍAccommodationˍActivation = ChangeˍAccommodationˍisˍReady

    Monitoringˍforˍchangesˍcanˍbeˍachieved : Goal
    Monitoringˍforˍchangesˍcanˍbeˍachieved =
      Purpose/EnviromentˍChangeˍisˍDetectable and ChangeˍAccommodationˍisˍReady

  module C-FailureˍMonitoring where
    open C-System.atTime t
    postulate
      InˍOperationˍRange     : Pred₀ ServiceˍLevel
      _Hasˍfailure-precursor : Pred₀ SystemˍState

    Failed/Failure-Predicted : Pred₀ MonitoringˍResult
    Failed/Failure-Predicted s = let open MonitoringˍResult in
       (serviceˍlevel of s is Not InˍOperationˍRange)
       or (systemˍstate of s) Hasˍfailure-precursor

    Failure/Failure-PrecursorˍisˍDetectable : Goal
    Failure/Failure-PrecursorˍisˍDetectable =
      Failed/Failure-Predicted is R1.Decidable 
    Failure/Failure-PrecursorˍDetection =
      Failure/Failure-PrecursorˍisˍDetectable

    Failure/Failure-PrecursorˍDetected : Proposition
    Failure/Failure-PrecursorˍDetected =
      Failed/Failure-Predicted monitoringˍresult

    FailureˍResponseˍisˍReady : Goal
    FailureˍResponseˍisˍReady =
      Failure/Failure-PrecursorˍDetected
       C-System.FailureˍResponseˍActivated (next t)
    FailureˍResponseˍActivation = FailureˍResponseˍisˍReady

    Monitoringˍforˍfailuresˍcanˍbeˍachieved : Goal
    Monitoringˍforˍfailuresˍcanˍbeˍachieved =
      Failure/Failure-PrecursorˍisˍDetectable and FailureˍResponseˍisˍReady

  open C-RoutineˍOperation
  open C-ChangeˍMonitoring
  open C-FailureˍMonitoring
  open C-TopˍLevel.atTime t
  postulate
    decompositionˍbyˍmonitoringˍtargets :
      routineˍoperation is Performed
       Monitoringˍforˍchangesˍcanˍbeˍachieved
       Monitoringˍforˍfailuresˍcanˍbeˍachieved
       OrdinaryˍOperationˍstateˍcanˍbeˍachieved

module C-ChangeˍAccommodation(t : Time) where
  open C-System using (ChangeˍAccommodation-Stage)
  open C-System.atTime t
  open C-TopˍLevel.atTime t
  postulate
    StageˍGoal : ChangeˍAccommodation-Stage  Goal

  ChangeˍAccommodation-Stage-Goalsˍareˍachieved =
    (p : InˍaˍChangeˍAccommodation-Stage)  StageˍGoal (stage p)

  postulate
    ChangeˍAccommodationˍstage-wiseˍdecomposition :
      ChangeˍAccommodation-Stage-Goalsˍareˍachieved
       ChangeˍAccommodationˍCycleˍcanˍbeˍachieved
    ProceduralˍDocˍforˍChangeˍAccommodation             : Set
    ProceduralˍDocˍforˍAAˍinˍCA : Set
    Performed :
      ProceduralˍDocˍforˍChangeˍAccommodation
      × ProceduralˍDocˍforˍAAˍinˍCA
       Goal

  open C-ProcedureˍExecution
       {TaskˍGoal = ChangeˍAccommodation-Stage-Goalsˍareˍachieved}
       {ProceduralˍDocumentˍforˍTask = ProceduralˍDocˍforˍChangeˍAccommodation}
       {ProceduralˍDocumentˍforˍAccountabilityˍAchievement =
         ProceduralˍDocˍforˍAAˍinˍCA}
       {Performed = Performed}
     public

module C-FailureˍResponse(t : Time) where
  module C-Unforeseeable where
    postulate
      UnforeseeableˍFailure : Set
      Respondedᵘᶠ            : UnforeseeableˍFailure  Goal

    Responseˍtoˍunforeseeableˍfailuresˍcanˍbeˍachieved : Goal
    Responseˍtoˍunforeseeableˍfailuresˍcanˍbeˍachieved =
      Every UnforeseeableˍFailure is Respondedᵘᶠ

    postulate
      ProceduralˍDocˍforˍFailureˍResponse⟨Unforeseeable⟩                 : Set
      ProceduralˍDocˍforˍAAˍinˍFR⟨Unforeseeable⟩ : Set
      Performed :
        ProceduralˍDocˍforˍFailureˍResponse⟨Unforeseeable⟩
        × ProceduralˍDocˍforˍAAˍinˍFR⟨Unforeseeable⟩
         Goal
    open C-ProcedureˍExecution
         {TaskˍGoal = Responseˍtoˍunforeseeableˍfailuresˍcanˍbeˍachieved}
         {ProceduralˍDocumentˍforˍTask =
            ProceduralˍDocˍforˍFailureˍResponse⟨Unforeseeable⟩}
         {ProceduralˍDocumentˍforˍAccountabilityˍAchievement =
            ProceduralˍDocˍforˍAAˍinˍFR⟨Unforeseeable⟩}
         {Performed = Performed}
       public

  module C-NotˍPlannedˍfor where
    postulate
      FailureˍNotˍPlannedˍfor : Set
      ReasonsˍforˍExclusion  : FailureˍNotˍPlannedˍfor  Proposition
      Respondedⁿᵖ : FailureˍNotˍPlannedˍfor  Goal
    Responseˍtoˍfailuresˍnotˍplannedˍforˍinˍdesignˍcanˍbeˍachieved : Goal
    Responseˍtoˍfailuresˍnotˍplannedˍforˍinˍdesignˍcanˍbeˍachieved =
       failureˍnotˍplannedˍfor  failureˍnotˍplannedˍfor is Respondedⁿᵖ
    postulate
      ProceduralˍDocˍforˍFailureˍResponse⟨NotˍPlannedˍfor⟩ : Set
      ProceduralˍDocˍforˍAAˍinˍFR⟨NotˍPlannedˍfor⟩ : Set
      Performed :
        ProceduralˍDocˍforˍFailureˍResponse⟨NotˍPlannedˍfor⟩
        × ProceduralˍDocˍforˍAAˍinˍFR⟨NotˍPlannedˍfor⟩
                    Goal
    open C-ProcedureˍExecution
           {TaskˍGoal =
            Responseˍtoˍfailuresˍnotˍplannedˍforˍinˍdesignˍcanˍbeˍachieved}
           {ProceduralˍDocumentˍforˍTask  =
            ProceduralˍDocˍforˍFailureˍResponse⟨NotˍPlannedˍfor⟩}
           {ProceduralˍDocumentˍforˍAccountabilityˍAchievement =
              ProceduralˍDocˍforˍAAˍinˍFR⟨NotˍPlannedˍfor⟩}
           {Performed = Performed}
         public

  module C-Plannedˍfor where
    postulate
      FailureˍPlannedˍfor : Set
      Respondedᵖ : FailureˍPlannedˍfor  Goal

    Responseˍtoˍfailuresˍplannedˍforˍinˍdesignˍcanˍbeˍachieved : Goal
    Responseˍtoˍfailuresˍplannedˍforˍinˍdesignˍcanˍbeˍachieved =
      Every FailureˍPlannedˍfor is Respondedᵖ

    postulate
      FailureˍSpecificˍResponseˍPlans : Set
      ProceduralˍDocˍforˍAAˍinˍFRᴾ : Set
      Performed : FailureˍSpecificˍResponseˍPlans
                  × ProceduralˍDocˍforˍAAˍinˍFRᴾ
                   Goal
    open C-ProcedureˍExecution
           {TaskˍGoal =
             Responseˍtoˍfailuresˍplannedˍforˍinˍdesignˍcanˍbeˍachieved}
           {ProceduralˍDocumentˍforˍTask =
             FailureˍSpecificˍResponseˍPlans}
           {ProceduralˍDocumentˍforˍAccountabilityˍAchievement =
             ProceduralˍDocˍforˍAAˍinˍFRᴾ}
           {Performed = Performed}
         public

  module C-Foreseeable where
    open C-NotˍPlannedˍfor
    open C-Plannedˍfor

    data ForeseeableˍFailure : Set where
      _plannedˍfor : FailureˍPlannedˍfor  ForeseeableˍFailure
      _notˍplannedˍfor : FailureˍNotˍPlannedˍfor  ForeseeableˍFailure

    Respondedᶠ : ForeseeableˍFailure  Goal
    Respondedᶠ (failure plannedˍfor)     = failure is Respondedᵖ
    Respondedᶠ (failure notˍplannedˍfor) = failure is Respondedⁿᵖ

    Responseˍtoˍforeseeableˍfailuresˍcanˍbeˍachieved : Goal
    Responseˍtoˍforeseeableˍfailuresˍcanˍbeˍachieved =
      Every ForeseeableˍFailure is Respondedᶠ

    decompositionˍbyˍwhetherˍplannedˍforˍinˍdesignˍorˍnot :
      Responseˍtoˍfailuresˍplannedˍforˍinˍdesignˍcanˍbeˍachieved
       Responseˍtoˍfailuresˍnotˍplannedˍforˍinˍdesignˍcanˍbeˍachieved
       Responseˍtoˍforeseeableˍfailuresˍcanˍbeˍachieved
    decompositionˍbyˍwhetherˍplannedˍforˍinˍdesignˍorˍnot
      p q (x plannedˍfor    ) = p x
    decompositionˍbyˍwhetherˍplannedˍforˍinˍdesignˍorˍnot
      p q (x notˍplannedˍfor) = q x

  open C-Unforeseeable
  open C-Foreseeable

  data Failure : Set where
    foreseeable   : ForeseeableˍFailure  Failure
    unforeseeable : UnforeseeableˍFailure  Failure

  Responded : Failure  Goal
  Responded (foreseeable   failure) = failure is Respondedᶠ
  Responded (unforeseeable failure) = failure is Respondedᵘᶠ

  decompositionˍbyˍforeseeablity :
    Responseˍtoˍforeseeableˍfailuresˍcanˍbeˍachieved
     Responseˍtoˍunforeseeableˍfailuresˍcanˍbeˍachieved
     Every Failure is Responded
  decompositionˍbyˍforeseeablity p q (foreseeable x) = p x
  decompositionˍbyˍforeseeablity p q (unforeseeable x) = q x
                           
  open C-System.atTime t
  open C-TopˍLevel.atTime t

  postulate
    failureˍhandledˍin : InˍaˍFailureˍResponse-Stage  Failure

  FailureˍResponseˍStage-Goals =
    (p : InˍaˍFailureˍResponse-Stage)  (failureˍhandledˍin p) is Responded 

  postulate
    stage-wiseˍdecomposition :
      FailureˍResponseˍStage-Goals
       FailureˍResponseˍCycleˍcanˍbeˍachieved