{-# OPTIONS --cubical #-}
module SemanticExplanation.Industry.LogicMore where
open import Agda.Builtin.Equality using (_≡_ ; refl)
open import Agda.Builtin.List using ([] ; _∷_)
open import Agda.Builtin.Nat using (Nat)
open import Agda.Builtin.Reflection using (Name)
open import Agda.Primitive using (Set)
open import SemanticExplanation
import SM.Basic.Properties as MachineProperties
import SMLogic.Temporal.PredicateTransformers as Temporal
data CrossingMovement : Set where sampleFreightMovement : CrossingMovement
data TrainApproachDetected : CrossingMovement → Set where approachEvidence : ∀ {x} → TrainApproachDetected x
data BarrierClosureCommanded : CrossingMovement → Set where closureCommand : ∀ {x} → BarrierClosureCommanded x
data BothBarriersProvedDown : CrossingMovement → Set where barriersDown : ∀ {x} → BothBarriersProvedDown x
data RoadConflictZoneClear : CrossingMovement → Set where roadClear : ∀ {x} → RoadConflictZoneClear x
data ProtectedRailMovementAuthorized : CrossingMovement → Set where protectedMovement : ∀ {x} → ProtectedRailMovementAuthorized x
data TrainOccupiesCrossing : CrossingMovement → Set where trainOccupancy : ∀ {x} → TrainOccupiesCrossing x
data BarrierReleaseInhibited : CrossingMovement → Set where releaseInhibited : ∀ {x} → BarrierReleaseInhibited x
data RearOfTrainClear : CrossingMovement → Set where rearClear : ∀ {x} → RearOfTrainClear x
data RoadReopeningAuthorized : CrossingMovement → Set where reopeningAuthorized : ∀ {x} → RoadReopeningAuthorized x
approachDetectionCommandsBarrierClosure
: (movement : CrossingMovement)
→ TrainApproachDetected movement
→ BarrierClosureCommanded movement
approachDetectionCommandsBarrierClosure movement approach = closureCommand
provedBarriersProtectRailMovement
: (movement : CrossingMovement)
→ BothBarriersProvedDown movement
→ RoadConflictZoneClear movement
→ ProtectedRailMovementAuthorized movement
provedBarriersProtectRailMovement movement down clear = protectedMovement
occupiedCrossingInhibitsBarrierRelease
: (movement : CrossingMovement)
→ TrainOccupiesCrossing movement
→ BothBarriersProvedDown movement
→ BarrierReleaseInhibited movement
occupiedCrossingInhibitsBarrierRelease movement occupied down = releaseInhibited
clearTrainAuthorizesRoadReopening
: (movement : CrossingMovement)
→ RearOfTrainClear movement
→ RoadConflictZoneClear movement
→ RoadReopeningAuthorized movement
clearTrainAuthorizesRoadReopening movement train-clear road-clear = reopeningAuthorized
data ColdChainShipment : Set where sampleVaccineConsignment : ColdChainShipment
data CalibratedLoggerSampleAvailable : ColdChainShipment → Set where calibratedSample : ∀ {x} → CalibratedLoggerSampleAvailable x
data TemperatureOutsideQualifiedRange : ColdChainShipment → Set where excursionSample : ∀ {x} → TemperatureOutsideQualifiedRange x
data ShipmentQuarantineRequired : ColdChainShipment → Set where quarantineRequired : ∀ {x} → ShipmentQuarantineRequired x
data ExcursionAssessmentPending : ColdChainShipment → Set where assessmentPending : ∀ {x} → ExcursionAssessmentPending x
data DistributionReleaseBlocked : ColdChainShipment → Set where releaseBlocked : ∀ {x} → DistributionReleaseBlocked x
data StabilityImpactAcceptable : ColdChainShipment → Set where acceptableImpact : ∀ {x} → StabilityImpactAcceptable x
data QualityUnitReviewComplete : ColdChainShipment → Set where qualityReview : ∀ {x} → QualityUnitReviewComplete x
data EligibleForDistributionRelease : ColdChainShipment → Set where distributionEligible : ∀ {x} → EligibleForDistributionRelease x
data OriginLoggerTracePresent : ColdChainShipment → Set where originTrace : ∀ {x} → OriginLoggerTracePresent x
data DestinationLoggerTracePresent : ColdChainShipment → Set where destinationTrace : ∀ {x} → DestinationLoggerTracePresent x
data EndToEndTemperatureTraceAvailable : ColdChainShipment → Set where completeTrace : ∀ {x} → EndToEndTemperatureTraceAvailable x
confirmedExcursionRequiresQuarantine
: (consignment : ColdChainShipment)
→ CalibratedLoggerSampleAvailable consignment
→ TemperatureOutsideQualifiedRange consignment
→ ShipmentQuarantineRequired consignment
confirmedExcursionRequiresQuarantine consignment calibrated excursion = quarantineRequired
pendingAssessmentBlocksDistribution
: (consignment : ColdChainShipment)
→ ShipmentQuarantineRequired consignment
→ ExcursionAssessmentPending consignment
→ DistributionReleaseBlocked consignment
pendingAssessmentBlocksDistribution consignment quarantine pending = releaseBlocked
reviewedStabilityEvidenceAllowsRelease
: (consignment : ColdChainShipment)
→ ShipmentQuarantineRequired consignment
→ StabilityImpactAcceptable consignment
→ QualityUnitReviewComplete consignment
→ EligibleForDistributionRelease consignment
reviewedStabilityEvidenceAllowsRelease consignment quarantine impact review = distributionEligible
pairedLoggerRecordsEstablishTemperatureTrace
: (consignment : ColdChainShipment)
→ OriginLoggerTracePresent consignment
→ DestinationLoggerTracePresent consignment
→ EndToEndTemperatureTraceAvailable consignment
pairedLoggerRecordsEstablishTemperatureTrace consignment origin destination = completeTrace
logicMoreFuel : Nat
logicMoreFuel = 512
logicMoreDomain : DomainSpec
logicMoreDomain =
domain-spec "industry-logic-rail-cold-chain-v1"
( entity-rule "rail.entity.movement" (quote CrossingMovement) [] "recorded level-crossing movement"
∷ entity-rule "cold.entity.shipment" (quote ColdChainShipment) [] "temperature-controlled shipment"
∷ [] )
( predicate-rule "rail.approach.detected" (quote TrainApproachDetected) (semanticExpression ∷ []) (unarySuffix "has a proved train-approach detection")
∷ predicate-rule "rail.barrier.commanded" (quote BarrierClosureCommanded) (semanticExpression ∷ []) (unarySuffix "requires the barrier-closing command")
∷ predicate-rule "rail.barriers.down" (quote BothBarriersProvedDown) (semanticExpression ∷ []) (unarySuffix "has both road barriers proved down")
∷ predicate-rule "rail.road.clear" (quote RoadConflictZoneClear) (semanticExpression ∷ []) (unarySuffix "has the road conflict zone proved clear")
∷ predicate-rule "rail.movement.authorized" (quote ProtectedRailMovementAuthorized) (semanticExpression ∷ []) (unarySuffix "authorizes the protected rail movement")
∷ predicate-rule "rail.crossing.occupied" (quote TrainOccupiesCrossing) (semanticExpression ∷ []) (unarySuffix "still records train occupancy in the crossing")
∷ predicate-rule "rail.release.inhibited" (quote BarrierReleaseInhibited) (semanticExpression ∷ []) (unarySuffix "keeps barrier release inhibited")
∷ predicate-rule "rail.train.clear" (quote RearOfTrainClear) (semanticExpression ∷ []) (unarySuffix "has a proved rear-of-train clear indication")
∷ predicate-rule "rail.road.reopen" (quote RoadReopeningAuthorized) (semanticExpression ∷ []) (unarySuffix "authorizes reopening the road crossing")
∷ predicate-rule "cold.logger.calibrated" (quote CalibratedLoggerSampleAvailable) (semanticExpression ∷ []) (unarySuffix "has a calibrated logger sample available")
∷ predicate-rule "cold.temperature.excursion" (quote TemperatureOutsideQualifiedRange) (semanticExpression ∷ []) (unarySuffix "has a recorded temperature outside its qualified range")
∷ predicate-rule "cold.quarantine" (quote ShipmentQuarantineRequired) (semanticExpression ∷ []) (unarySuffix "must enter quality quarantine")
∷ predicate-rule "cold.assessment.pending" (quote ExcursionAssessmentPending) (semanticExpression ∷ []) (unarySuffix "still has its excursion assessment pending")
∷ predicate-rule "cold.release.blocked" (quote DistributionReleaseBlocked) (semanticExpression ∷ []) (unarySuffix "remains blocked from distribution release")
∷ predicate-rule "cold.stability.acceptable" (quote StabilityImpactAcceptable) (semanticExpression ∷ []) (unarySuffix "has reviewed stability evidence showing acceptable impact")
∷ predicate-rule "cold.quality.review" (quote QualityUnitReviewComplete) (semanticExpression ∷ []) (unarySuffix "has completed quality-unit review")
∷ predicate-rule "cold.release.eligible" (quote EligibleForDistributionRelease) (semanticExpression ∷ []) (unarySuffix "is eligible for distribution release")
∷ predicate-rule "cold.trace.origin" (quote OriginLoggerTracePresent) (semanticExpression ∷ []) (unarySuffix "has its origin logger record")
∷ predicate-rule "cold.trace.destination" (quote DestinationLoggerTracePresent) (semanticExpression ∷ []) (unarySuffix "has its destination logger record")
∷ predicate-rule "cold.trace.complete" (quote EndToEndTemperatureTraceAvailable) (semanticExpression ∷ []) (unarySuffix "has an end-to-end temperature trace available for review")
∷ [] ) [] [] [] logicMoreFuel
railApproachExplanation = explainNameCompact logicMoreDomain approachDetectionCommandsBarrierClosure
railProtectionExplanation = explainNameCompact logicMoreDomain provedBarriersProtectRailMovement
railOccupancyExplanation = explainNameCompact logicMoreDomain occupiedCrossingInhibitsBarrierRelease
railReopeningExplanation = explainNameCompact logicMoreDomain clearTrainAuthorizesRoadReopening
coldQuarantineExplanation = explainNameCompact logicMoreDomain confirmedExcursionRequiresQuarantine
coldHoldExplanation = explainNameCompact logicMoreDomain pendingAssessmentBlocksDistribution
coldReleaseExplanation = explainNameCompact logicMoreDomain reviewedStabilityEvidenceAllowsRelease
coldTraceExplanation = explainNameCompact logicMoreDomain pairedLoggerRecordsEstablishTemperatureTrace
railApproachText : Explanation.text railApproachExplanation ≡ "For every recorded level-crossing movement movement, if movement has a proved train-approach detection, then movement requires the barrier-closing command."
railApproachText = refl
railProtectionText : Explanation.text railProtectionExplanation ≡ "For every recorded level-crossing movement movement, if movement has both road barriers proved down and movement has the road conflict zone proved clear, then movement authorizes the protected rail movement."
railProtectionText = refl
railOccupancyText : Explanation.text railOccupancyExplanation ≡ "For every recorded level-crossing movement movement, if movement still records train occupancy in the crossing and movement has both road barriers proved down, then movement keeps barrier release inhibited."
railOccupancyText = refl
railReopeningText : Explanation.text railReopeningExplanation ≡ "For every recorded level-crossing movement movement, if movement has a proved rear-of-train clear indication and movement has the road conflict zone proved clear, then movement authorizes reopening the road crossing."
railReopeningText = refl
coldQuarantineText : Explanation.text coldQuarantineExplanation ≡ "For every temperature-controlled shipment consignment, if consignment has a calibrated logger sample available and consignment has a recorded temperature outside its qualified range, then consignment must enter quality quarantine."
coldQuarantineText = refl
coldHoldText : Explanation.text coldHoldExplanation ≡ "For every temperature-controlled shipment consignment, if consignment must enter quality quarantine and consignment still has its excursion assessment pending, then consignment remains blocked from distribution release."
coldHoldText = refl
coldReleaseText : Explanation.text coldReleaseExplanation ≡ "For every temperature-controlled shipment consignment, if consignment must enter quality quarantine, consignment has reviewed stability evidence showing acceptable impact, and consignment has completed quality-unit review, then consignment is eligible for distribution release."
coldReleaseText = refl
coldTraceText : Explanation.text coldTraceExplanation ≡ "For every temperature-controlled shipment consignment, if consignment has its origin logger record and consignment has its destination logger record, then consignment has an end-to-end temperature trace available for review."
coldTraceText = refl
liveReachabilityRule : Name
liveReachabilityRule = quote MachineProperties.reachableInvariant
liveTemporalMonotonicityRule : Name
liveTemporalMonotonicityRule = quote Temporal.AXᵀ-monotone