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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Fri, 30 Apr 2021 15:17:40 +0200*References*: <f06df008-8efa-4942-bb93-a2ebbbfe7984n@googlegroups.com> <09E12A1A-7A9E-4A1D-9B43-7048C57AE425@gmail.com> <80bd4635-9dcb-4604-a8fa-30fecd75baedn@googlegroups.com>

As I wrote, this is an action formula, not a temporal formula expected for properties. If you want to check that this action formula holds at all transitions, you can write [][(y=0 /\ y' = 0) \/ (y # 0 /\ y' = y-1)]_y (you may also use the tuple "vars" as the subscript if it includes y). 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/7E9E767C-4AA9-4068-8353-64B525E2F886%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] What's wrong with this temporal formula?***From:*Stephan Merz

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

**Re: [tlaplus] What's wrong with this temporal formula?***From:*Stephan Merz

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

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