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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Fri, 30 Apr 2021 14:47:59 +0200*References*: <f06df008-8efa-4942-bb93-a2ebbbfe7984n@googlegroups.com>

Hello, 1. "not equal" is written # in TLA+ (or /=), "~" is Boolean negation. 2. I believe "->" represents implication in your formula, but it is written "=>" in TLA+. 3. The expressions on both sides of an implication should be Boolean, but the _expression_ on the right-hand side is y-1. 4. The (action) formula corresponding to your informal statement can be written as \/ y' = 0 \/ y # 0 /\ y' = y-1 A similar formula (but with a slightly different meaning) is y' = IF y # 0 THEN y-1 ELSE 0 Stephan
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/09E12A1A-7A9E-4A1D-9B43-7048C57AE425%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] What's wrong with this temporal formula?***From:*c.burge...@xxxxxxxxx

**References**:**[tlaplus] What's wrong with this temporal formula?***From:*c.burge...@xxxxxxxxx

- Prev by Date:
**[tlaplus] Re: What's wrong with this temporal formula?** - Next by Date:
**Re: [tlaplus] What's wrong with this temporal formula?** - Previous by thread:
**[tlaplus] Re: What's wrong with this temporal formula?** - Next by thread:
**Re: [tlaplus] What's wrong with this temporal formula?** - Index(es):