[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Action A can only be followed by Action B



Here is the Spec I am model checking with [][ActionA => ActionB]_vars

EXTENDS Naturals

\* LOGIC <- 0..1
CONSTANT LOGIC


VARIABLES vcc_1v8_aon, pcie_vph, aon_vdd, pcie_vp, vddq_nand, core_vdd, fphy_vdd, hsstp_vph, hsstp_vp, pmic_reset
vars == <<vcc_1v8_aon, pcie_vph, aon_vdd, pcie_vp, vddq_nand, core_vdd, fphy_vdd, hsstp_vph, hsstp_vp, pmic_reset>>

Init ==
    /\ vcc_1v8_aon = 0
    /\ pcie_vph = 0
    /\ aon_vdd = 0
    /\ pcie_vp = 0
    /\ vddq_nand = 0
    /\ core_vdd = 0
    /\ fphy_vdd = 0
    /\ hsstp_vph = 0
    /\ hsstp_vp = 0
    /\ pmic_reset = 0
   
FullPowerUp ==
    /\ vcc_1v8_aon = 0
    /\ pcie_vph = 0
    /\ aon_vdd = 0
    /\ pcie_vp = 0
    /\ vddq_nand = 0
    /\ core_vdd = 0
    /\ fphy_vdd = 0
    /\ hsstp_vph \in LOGIC \*HSSTP is described as independent but wrong in diagram
    /\ hsstp_vp \in LOGIC \*HSSTP is described as independent but wrong in diagram
    /\ pmic_reset = 0
    /\ vcc_1v8_aon' = 1
    /\ pcie_vph' = 1
    /\ aon_vdd' = 1
    /\ pcie_vp' = 1
    /\ vddq_nand' = 1
    /\ core_vdd' = 1
    /\ fphy_vdd' = 1
    /\ hsstp_vph' = 1
    /\ hsstp_vp' = 1
    /\ pmic_reset' = 1
   
DPS2Entry ==
    /\ pmic_reset = 1
    /\ pcie_vph = 1
    /\ aon_vdd = 1
    /\ vcc_1v8_aon = 1
    /\ pcie_vp = 1
    /\ vddq_nand = 1
    /\ core_vdd = 1
    /\ fphy_vdd = 1
    /\ pcie_vp' = 0
    /\ vddq_nand' = 0
    /\ core_vdd' = 0
    /\ fphy_vdd' = 0
    /\ \E logic \in LOGIC: /\ hsstp_vph = 1 /\ hsstp_vp = 1
                           /\ hsstp_vph' = logic /\ hsstp_vp' = logic
    /\ UNCHANGED <<pmic_reset, vcc_1v8_aon, pcie_vph, aon_vdd>>
   
DPS2Exit ==
    /\ vcc_1v8_aon = 1
    /\ pcie_vph = 1
    /\ pmic_reset = 1
    /\ pcie_vp = 0
    /\ pcie_vp' = 1
    /\ vddq_nand = 0
    /\ vddq_nand' = 1
    /\ core_vdd = 0
    /\ core_vdd' = 1
    /\ fphy_vdd = 0
    /\ fphy_vdd' = 1
    /\ hsstp_vph \in LOGIC
    /\ hsstp_vph' \in LOGIC
    /\ hsstp_vp \in LOGIC
    /\ hsstp_vp' \in LOGIC
    /\ UNCHANGED <<vcc_1v8_aon, pcie_vph, aon_vdd, pmic_reset>>
   
FullPowerDown ==
    /\ vcc_1v8_aon = 1
    /\ vcc_1v8_aon' = 0
    /\ pcie_vph = 1
    /\ pcie_vph' = 0
    /\ aon_vdd = 1
    /\ aon_vdd' = 0
    /\ pcie_vp = 1
    /\ pcie_vp' = 0
    /\ vddq_nand = 1
    /\ vddq_nand' = 0
    /\ core_vdd = 1
    /\ core_vdd' = 0
    /\ fphy_vdd = 1
    /\ fphy_vdd' = 0
    /\ pmic_reset = 1
    /\ pmic_reset' = 0
    /\ UNCHANGED <<hsstp_vph, hsstp_vp>>

Next ==
    \/ FullPowerUp
    \/ DPS2Entry
    \/ DPS2Exit
    \/ FullPowerDown

CannotDPS2ExitWithoutEntry == [][DPS2Entry => DPS2Exit]_vars
   

Spec == Init /\ [][Next]_vars

THEOREM Spec => CannotDPS2ExitWithoutEntry

On Monday, January 29, 2024 at 1:40:56 PM UTC-8 Chris Ortiz wrote:
Hello TLA+ Group,

How would you express a property that Action A can only be followed by Action B?

Thanks,
Zitro

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4e63c4e7-83d4-4f97-98bd-6dc5fbc5a73bn%40googlegroups.com.