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

*From*: "c.burge...@xxxxxxxxx" <c.burge.glasgow@xxxxxxxxx>*Date*: Fri, 30 Apr 2021 05:46:19 -0700 (PDT)*References*: <f06df008-8efa-4942-bb93-a2ebbbfe7984n@googlegroups.com>

Also tried stating it as :

y ~0 -> y'= y-1, same error

On Friday, April 30, 2021 at 1:39:23 PM UTC+1 c.burge...@xxxxxxxxx wrote:

Hi again!

I have the following temporal formula:

y'= 0 \/ y ~0 -> y-1

Which I hope says that the next value of y is zero or y-1 if y is not zero.

However, when I put this as a property in TLC, I get the error:

Was expecting ===== or more module body, encountered '~' in Properties at line 1 and token 'y'.

Obviously it's not happy with the ~ (equally unhappy with \lnot), but I'm not sure how to proceed from here!

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/0371344f-7fd7-463e-855e-a6a1195583e6n%40googlegroups.com.

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

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