{-# OPTIONS --safe --cubical #-}
module SemanticExplanation.Industry.SpartanMore where
open import Agda.Builtin.Reflection using (Name)
open import Agda.Builtin.List renaming ([] to []L ; _∷_ to _∷L_)
open import SemanticExplanation
open import Spartan6.Prelude
import Spartan6.Semantics.Invariant as Invariant
import Spartan6.Semantics.Design as Design
record BurnerManagementSample : Type₀ where
constructor burner-sample
field
purgeCompleteBit : Bit
furnaceClearBit : Bit
fuelValvesClosedBit : Bit
flamePresentBit : Bit
burnerSafetyLoopHealthyBit : Bit
open BurnerManagementSample public
ignitionPermit : Bit → Bit → Bit → Bit
ignitionPermit purge clear valves = (purge and clear) and valves
fuelTrainPermit : Bit → Bit → Bit
fuelTrainPermit flame safety = flame and safety
PurgeCycleComplete : BurnerManagementSample → Type₀
PurgeCycleComplete sample = purgeCompleteBit sample ≡ high
PurgeCycleIncomplete : BurnerManagementSample → Type₀
PurgeCycleIncomplete sample = purgeCompleteBit sample ≡ low
FurnaceProvedClear : BurnerManagementSample → Type₀
FurnaceProvedClear sample = furnaceClearBit sample ≡ high
FuelValvesProvedClosed : BurnerManagementSample → Type₀
FuelValvesProvedClosed sample = fuelValvesClosedBit sample ≡ high
IgnitionSequenceEnabled : BurnerManagementSample → Type₀
IgnitionSequenceEnabled sample = ignitionPermit (purgeCompleteBit sample) (furnaceClearBit sample) (fuelValvesClosedBit sample) ≡ high
IgnitionSequenceBlocked : BurnerManagementSample → Type₀
IgnitionSequenceBlocked sample = ignitionPermit (purgeCompleteBit sample) (furnaceClearBit sample) (fuelValvesClosedBit sample) ≡ low
MainFlameEstablished : BurnerManagementSample → Type₀
MainFlameEstablished sample = flamePresentBit sample ≡ high
MainFlameLost : BurnerManagementSample → Type₀
MainFlameLost sample = flamePresentBit sample ≡ low
BurnerSafetyLoopHealthy : BurnerManagementSample → Type₀
BurnerSafetyLoopHealthy sample = burnerSafetyLoopHealthyBit sample ≡ high
FuelTrainEnabled : BurnerManagementSample → Type₀
FuelTrainEnabled sample = fuelTrainPermit (flamePresentBit sample) (burnerSafetyLoopHealthyBit sample) ≡ high
FuelTrainDisabled : BurnerManagementSample → Type₀
FuelTrainDisabled sample = fuelTrainPermit (flamePresentBit sample) (burnerSafetyLoopHealthyBit sample) ≡ low
verifiedPurgeAllowsIgnition
: (cycle : BurnerManagementSample)
→ PurgeCycleComplete cycle → FurnaceProvedClear cycle → FuelValvesProvedClosed cycle
→ IgnitionSequenceEnabled cycle
verifiedPurgeAllowsIgnition (burner-sample purge clear valves flame safety) pp pc pv =
cong (λ x → ignitionPermit x clear valves) pp
∙ cong (λ x → ignitionPermit high x valves) pc
∙ cong (ignitionPermit high high) pv
incompletePurgeBlocksIgnition
: (cycle : BurnerManagementSample)
→ PurgeCycleIncomplete cycle → IgnitionSequenceBlocked cycle
incompletePurgeBlocksIgnition (burner-sample purge clear valves flame safety) pp =
cong (λ x → ignitionPermit x clear valves) pp
establishedFlameEnablesFuelTrain
: (cycle : BurnerManagementSample)
→ MainFlameEstablished cycle → BurnerSafetyLoopHealthy cycle
→ FuelTrainEnabled cycle
establishedFlameEnablesFuelTrain (burner-sample purge clear valves flame safety) pf ps =
cong (λ x → fuelTrainPermit x safety) pf
∙ cong (fuelTrainPermit high) ps
flameLossDropsFuelTrain
: (cycle : BurnerManagementSample)
→ MainFlameLost cycle → FuelTrainDisabled cycle
flameLossDropsFuelTrain (burner-sample purge clear valves flame safety) pf =
cong (λ x → fuelTrainPermit x safety) pf
record PumpDemandSample : Type₀ where
constructor pump-sample
field
levelChannelA : Bit
levelChannelB : Bit
levelChannelC : Bit
pumpDriveAvailable : Bit
open PumpDemandSample public
majorityDemand : Bit → Bit → Bit → Bit
majorityDemand a b c = ((a and b) or (a and c)) or (b and c)
ChannelAReportsHighWater : PumpDemandSample → Type₀
ChannelAReportsHighWater sample = levelChannelA sample ≡ high
ChannelBReportsHighWater : PumpDemandSample → Type₀
ChannelBReportsHighWater sample = levelChannelB sample ≡ high
ChannelCReportsHighWater : PumpDemandSample → Type₀
ChannelCReportsHighWater sample = levelChannelC sample ≡ high
TwoOfThreeHighWaterDemand : PumpDemandSample → Type₀
TwoOfThreeHighWaterDemand sample = majorityDemand (levelChannelA sample) (levelChannelB sample) (levelChannelC sample) ≡ high
PumpDriveAvailable : PumpDemandSample → Type₀
PumpDriveAvailable sample = pumpDriveAvailable sample ≡ high
DrainagePumpStartPermitted : PumpDemandSample → Type₀
DrainagePumpStartPermitted sample = majorityDemand (levelChannelA sample) (levelChannelB sample) (levelChannelC sample) and pumpDriveAvailable sample ≡ high
data ChannelDisagreementRecorded : PumpDemandSample → Type₀ where disagreementEvidence : ∀ {x} → ChannelDisagreementRecorded x
data InstrumentDiagnosticRequired : PumpDemandSample → Type₀ where diagnosticRequired : ∀ {x} → InstrumentDiagnosticRequired x
channelsABConfirmHighWater
: (sample : PumpDemandSample)
→ ChannelAReportsHighWater sample → ChannelBReportsHighWater sample
→ TwoOfThreeHighWaterDemand sample
channelsABConfirmHighWater (pump-sample a b c drive) pa pb =
cong (λ x → majorityDemand x b c) pa
∙ cong (λ x → majorityDemand high x c) pb
channelsACConfirmHighWater
: (sample : PumpDemandSample)
→ ChannelAReportsHighWater sample → ChannelCReportsHighWater sample
→ TwoOfThreeHighWaterDemand sample
channelsACConfirmHighWater (pump-sample a false c drive) pa pc =
cong (λ x → majorityDemand x false c) pa
∙ cong (majorityDemand high false) pc
channelsACConfirmHighWater (pump-sample a true c drive) pa pc =
cong (λ x → majorityDemand x true c) pa
∙ cong (majorityDemand high true) pc
channelsBCConfirmHighWater
: (sample : PumpDemandSample)
→ ChannelBReportsHighWater sample → ChannelCReportsHighWater sample
→ TwoOfThreeHighWaterDemand sample
channelsBCConfirmHighWater (pump-sample false b c drive) pb pc =
cong (λ x → majorityDemand false x c) pb
∙ cong (majorityDemand false high) pc
channelsBCConfirmHighWater (pump-sample true b c drive) pb pc =
cong (λ x → majorityDemand true x c) pb
∙ cong (majorityDemand true high) pc
confirmedDemandPermitsPumpStart
: (sample : PumpDemandSample)
→ TwoOfThreeHighWaterDemand sample → PumpDriveAvailable sample
→ DrainagePumpStartPermitted sample
confirmedDemandPermitsPumpStart (pump-sample a b c drive) demand available =
cong (λ x → x and drive) demand ∙ cong (high and_) available
channelDisagreementRequiresDiagnostic
: (sample : PumpDemandSample)
→ ChannelDisagreementRecorded sample
→ InstrumentDiagnosticRequired sample
channelDisagreementRequiresDiagnostic sample disagreement = diagnosticRequired
spartanMoreDomain : DomainSpec
spartanMoreDomain =
domain-spec "industry-spartan-burner-pump-v1"
( entity-rule "burner.entity.sample" (quote BurnerManagementSample) []L "recorded burner-management sample"
∷L entity-rule "pump.entity.sample" (quote PumpDemandSample) []L "recorded three-channel pump-demand sample"
∷L []L )
( predicate-rule "burner.purge.complete" (quote PurgeCycleComplete) (semanticExpression ∷L []L) (unarySuffix "records the purge cycle complete")
∷L predicate-rule "burner.purge.incomplete" (quote PurgeCycleIncomplete) (semanticExpression ∷L []L) (unarySuffix "records the purge cycle incomplete")
∷L predicate-rule "burner.furnace.clear" (quote FurnaceProvedClear) (semanticExpression ∷L []L) (unarySuffix "records the furnace proved clear")
∷L predicate-rule "burner.valves.closed" (quote FuelValvesProvedClosed) (semanticExpression ∷L []L) (unarySuffix "records both automatic fuel valves proved closed")
∷L predicate-rule "burner.ignition.enabled" (quote IgnitionSequenceEnabled) (semanticExpression ∷L []L) (unarySuffix "enables the ignition sequence")
∷L predicate-rule "burner.ignition.blocked" (quote IgnitionSequenceBlocked) (semanticExpression ∷L []L) (unarySuffix "keeps the ignition sequence blocked")
∷L predicate-rule "burner.flame.established" (quote MainFlameEstablished) (semanticExpression ∷L []L) (unarySuffix "records the main flame established")
∷L predicate-rule "burner.flame.lost" (quote MainFlameLost) (semanticExpression ∷L []L) (unarySuffix "records loss of the main flame signal")
∷L predicate-rule "burner.safety.healthy" (quote BurnerSafetyLoopHealthy) (semanticExpression ∷L []L) (unarySuffix "records the burner safety loop healthy")
∷L predicate-rule "burner.fuel.enabled" (quote FuelTrainEnabled) (semanticExpression ∷L []L) (unarySuffix "leaves the modeled fuel-train permit high")
∷L predicate-rule "burner.fuel.disabled" (quote FuelTrainDisabled) (semanticExpression ∷L []L) (unarySuffix "forces the modeled fuel-train permit low")
∷L predicate-rule "pump.channel.a" (quote ChannelAReportsHighWater) (semanticExpression ∷L []L) (unarySuffix "has level channel A reporting high water")
∷L predicate-rule "pump.channel.b" (quote ChannelBReportsHighWater) (semanticExpression ∷L []L) (unarySuffix "has level channel B reporting high water")
∷L predicate-rule "pump.channel.c" (quote ChannelCReportsHighWater) (semanticExpression ∷L []L) (unarySuffix "has level channel C reporting high water")
∷L predicate-rule "pump.vote.confirmed" (quote TwoOfThreeHighWaterDemand) (semanticExpression ∷L []L) (unarySuffix "asserts the two-out-of-three high-water demand")
∷L predicate-rule "pump.drive.available" (quote PumpDriveAvailable) (semanticExpression ∷L []L) (unarySuffix "records the drainage-pump drive available")
∷L predicate-rule "pump.start.permitted" (quote DrainagePumpStartPermitted) (semanticExpression ∷L []L) (unarySuffix "permits the drainage pump start output")
∷L predicate-rule "pump.channel.disagreement" (quote ChannelDisagreementRecorded) (semanticExpression ∷L []L) (unarySuffix "records a disagreement between level channels")
∷L predicate-rule "pump.diagnostic.required" (quote InstrumentDiagnosticRequired) (semanticExpression ∷L []L) (unarySuffix "requires an instrument-channel diagnostic review")
∷L []L ) []L []L []L 512
burnerIgnitionExplanation = explainNameCompact spartanMoreDomain verifiedPurgeAllowsIgnition
burnerPurgeBlockExplanation = explainNameCompact spartanMoreDomain incompletePurgeBlocksIgnition
burnerFlamePermitExplanation = explainNameCompact spartanMoreDomain establishedFlameEnablesFuelTrain
burnerFlameTripExplanation = explainNameCompact spartanMoreDomain flameLossDropsFuelTrain
pumpABVoteExplanation = explainNameCompact spartanMoreDomain channelsABConfirmHighWater
pumpACVoteExplanation = explainNameCompact spartanMoreDomain channelsACConfirmHighWater
pumpBCVoteExplanation = explainNameCompact spartanMoreDomain channelsBCConfirmHighWater
pumpStartExplanation = explainNameCompact spartanMoreDomain confirmedDemandPermitsPumpStart
pumpDiagnosticExplanation = explainNameCompact spartanMoreDomain channelDisagreementRequiresDiagnostic
burnerIgnitionText : Explanation.text burnerIgnitionExplanation ≡ "For every recorded burner-management sample cycle, if cycle records the purge cycle complete, cycle records the furnace proved clear, and cycle records both automatic fuel valves proved closed, then cycle enables the ignition sequence."
burnerIgnitionText = refl
burnerPurgeBlockText : Explanation.text burnerPurgeBlockExplanation ≡ "For every recorded burner-management sample cycle, if cycle records the purge cycle incomplete, then cycle keeps the ignition sequence blocked."
burnerPurgeBlockText = refl
burnerFlamePermitText : Explanation.text burnerFlamePermitExplanation ≡ "For every recorded burner-management sample cycle, if cycle records the main flame established and cycle records the burner safety loop healthy, then cycle leaves the modeled fuel-train permit high."
burnerFlamePermitText = refl
burnerFlameTripText : Explanation.text burnerFlameTripExplanation ≡ "For every recorded burner-management sample cycle, if cycle records loss of the main flame signal, then cycle forces the modeled fuel-train permit low."
burnerFlameTripText = refl
pumpABVoteText : Explanation.text pumpABVoteExplanation ≡ "For every recorded three-channel pump-demand sample sample, if sample has level channel A reporting high water and sample has level channel B reporting high water, then sample asserts the two-out-of-three high-water demand."
pumpABVoteText = refl
pumpACVoteText : Explanation.text pumpACVoteExplanation ≡ "For every recorded three-channel pump-demand sample sample, if sample has level channel A reporting high water and sample has level channel C reporting high water, then sample asserts the two-out-of-three high-water demand."
pumpACVoteText = refl
pumpBCVoteText : Explanation.text pumpBCVoteExplanation ≡ "For every recorded three-channel pump-demand sample sample, if sample has level channel B reporting high water and sample has level channel C reporting high water, then sample asserts the two-out-of-three high-water demand."
pumpBCVoteText = refl
pumpStartText : Explanation.text pumpStartExplanation ≡ "For every recorded three-channel pump-demand sample sample, if sample asserts the two-out-of-three high-water demand and sample records the drainage-pump drive available, then sample permits the drainage pump start output."
pumpStartText = refl
pumpDiagnosticText : Explanation.text pumpDiagnosticExplanation ≡ "For every recorded three-channel pump-demand sample sample, if sample records a disagreement between level channels, then sample requires an instrument-channel diagnostic review."
pumpDiagnosticText = refl
liveInvariantRun : Name
liveInvariantRun = quote Invariant.initial-run-preserves
liveDesignTransition : Name
liveDesignTransition = quote Design.Transition