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

On Tuesday, January 30, 2024 at 7:59:17 AM UTC-8 Stephan Merz wrote:

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 <zitro...@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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4e63c4e7-83d4-4f97-98bd-6dc5fbc5a73bn%40googlegroups.com.