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

On Tuesday, January 30, 2024 at 11:46:05 PM UTC-8 Stephan Merz wrote:

That means that the state predicate that I guessed does not characterize states following ActionA. Since you know the specification, you can perhaps identify a predicate that does. It may however be the case that no such predicate can be defined using the state variables used in the specification. In that case you’d need to add an auxiliary variable that records when ActionA has been performed, i.e. something along the lines of

Init == … /\ postActionA = FALSE

ActionA == … /\ postActionA’ = TRUE

ActionX == … /\ postActionA’ = FALSE. \* for all other actions

Stephan

On Jan 30, 2024, at 20:43, Chris Ortiz <zitro...@xxxxxxxxx> wrote:

Thank you very much Stephan. I tried your suggestion but it immediately violated the initial state.

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.

--
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/54356fbb-e93c-4df9-b00a-50e256275c30n%40googlegroups.com.