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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sat, 16 Oct 2021 13:50:36 +0200*References*: <92ac2873-a0a6-415a-9c6f-fd6a8afa028cn@googlegroups.com> <68599e0d-f105-4103-97ad-3e98644274ean@googlegroups.com> <E22933E0-B6A3-4530-9D60-152A789D76F8@gmail.com> <6ffc80d4-e218-40cc-8f53-bca2c868dbb6n@googlegroups.com> <ac28683b-f55a-4916-978a-b7a5b1f5f18en@googlegroups.com>

First, you can of course ignore the deadlock by disabling deadlock checking if you are not interested in it. Second, a state is deadlocked if `ENABLED Next' is false at that state, but the actual transition relation is [Next]_vars, so a finite behavior ending in a deadlocked state can always be extended to an infinite behavior. 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/4AB111BC-F840-4085-9A25-9B39EB368CB4%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] How to model check this "real-time" spec?***From:*Earnshaw

**References**:**[tlaplus] How to model check this "real-time" spec?***From:*ns

**[tlaplus] Re: How to model check this "real-time" spec?***From:*ns

**Re: [tlaplus] How to model check this "real-time" spec?***From:*Stephan Merz

**Re: [tlaplus] How to model check this "real-time" spec?***From:*ns

**Re: [tlaplus] How to model check this "real-time" spec?***From:*ns

- Prev by Date:
**Re: [tlaplus] How to model check this "real-time" spec?** - Next by Date:
**Re: [tlaplus] Current status of TLC multi-core scaling** - Previous by thread:
**Re: [tlaplus] How to model check this "real-time" spec?** - Next by thread:
**Re: [tlaplus] How to model check this "real-time" spec?** - Index(es):