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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 2 Aug 2022 18:30:00 +0200*References*: <c7ad139e-5c11-4df4-883b-e49c10f71d0fn@googlegroups.com> <a111a2e7-2561-4f59-beab-1e8dd15fb3fcn@googlegroups.com> <ac722f3f-a751-459d-b8cd-0d2a0c3ba7adn@googlegroups.com> <8eb90ad3-0e00-43db-a092-5f99938491bfn@googlegroups.com> <98c48137-da4c-4973-95a9-84b22a4ccb95n@googlegroups.com> <692789fc-88b9-4d44-8251-a21dc2e93ad7n@googlegroups.com>

TLC will choke whenever you quantify over or try to enumerate an infinite set – even if the end result is finite as in { n \in Nat : 0 < n /\ n < 10 }. ProB [1] accepts TLA+, it is based on a constraint solver and can handle such cases. Apalache is mostly restricted to finite data structures, in particular any sets occurring as values have to be finite. You can (usually) get away with unbounded integers as data because SMT solvers handle them natively, so you may not need a state constraint bounding integer values in the same way as in TLC. Stephan [1] https://prob.hhu.de
--
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/70E6C0D0-61EE-4927-B98E-DAFC12A2EBB1%40gmail.com. |

**References**:**[tlaplus] Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat***From:*Brandon Barker

**[tlaplus] Re: Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat***From:*Brandon Barker

**[tlaplus] Re: Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat***From:*Brandon Barker

**[tlaplus] Re: Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat***From:*Andrew Helwer

**[tlaplus] Re: Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat***From:*Brandon Barker

**[tlaplus] Re: Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat***From:*Andrew Helwer

- Prev by Date:
**[tlaplus] Re: Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat** - Next by Date:
**Re: [tlaplus] Modeling optional values - from a newbie** - Previous by thread:
**[tlaplus] Re: Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat** - Next by thread:
**[tlaplus] Re: Issue enumerating Nat, but I don't see where I'm enumerating the entire set Nat** - Index(es):