[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:39:23 -0700 (PDT)*Ironport-hdrordr*: A9a23:xxt84qkDFf+1cErJflzm+hDPXz/pDfIK3DAbvn1ZSRFFG/GwvcaogfgdyFvImC8cMUtApfmsMLSNKEm2ybdb+o8UVI3JYCDDmE+FaL5v9pHjxTqIIUPD38pQz71pfaQ7KPCYNzRHpP336gW5DNosqePvmJyAv/vUzHtmUGhRBJ1I0gERMGumO3wzYAFHAJYjfaD92vZ6

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/f06df008-8efa-4942-bb93-a2ebbbfe7984n%40googlegroups.com.

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

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

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