[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*Ironport-hdrordr*: A9a23:fw/KVKoxDVdzx7P80Jxkjm4aV5t1L9V00zEX/kB9WHVpm5Oj+7HUoB1L73KE8Ar5BktL6Km90ci7MAPhHPtOjucs1NiZLXzbUQeTXfBfBM7Zskvd88OXzJ8Z6U9PG5IOSuEYTmIKw/oT2WGDYpUdKaC8geSVbVK09QYjcegVUdAo0+4JMHfpLqQsfngLOXNRLvP1jbsh1kDQBQVoUimiPAh5YwGAnay+qHuBW29KO/cJ0mmzZFiTmczH+najr2Aju/Im+8ZHzYEHqX2b2kxgiZCGIq+27R6S032boqqC9jI6Pr3FtiAZQQ+cwDpBlO9aKva/VfkO0YTfjidUrPD85y04N8A2wXLcdGO4rF/M3E3PyzAz8hbZuB6lvUc=*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. |

**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:
**[tlaplus] Understanding PlusCal 'either' translation to TLA** - Index(es):