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

[Stephan Merz <stephan.merz@xxxxxxxxx>]

Hello,

your formula asserts that whenever ActionA occurs then ActionB occurs as well, which is not what you are after. In your example, DPS2Entry requires fphy_vdd = 1, whereas DPS2Exit has fphy_vdd = 0, so the implication must be false (unless DPS2Entry never occurs).

You can express your property by something like

Spec => [](postActionA => ~ ENABLED (Next /\ ~ ActionB))

where postActionA is a state predicate that characterizes states following an occurrence of ActionA. Without looking too closely at your example, this could be something like

    /\ pcie_vp = 0
    /\ vddq_nand = 0
    /\ core_vdd = 0
    /\ fphy_vdd = 0

I once suggested an extension of TLA+ [1] that would have allowed you to write

Spec => [][ActionA => X ~ ENABLED (Next /\ ~ ActionB)]_vars

where X is the next-time operator of LTL. But the TLA+ tools do not handle that extension of the logic.

Regards,

Stephan

[1] https://members.loria.fr/SMerz/papers/gtla.html

On Jan 30, 2024, at 16:43, Chris Ortiz <zitroomega@xxxxxxxxx> wrote:

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.

--
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/3C103EB7-E22F-4657-82FB-254EA7A36761%40gmail.com.