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

Re: [tlaplus] Nondeterminism and equivalence

From: Stephan Merz <stepha...@xxxxxxxxx>
Date: Sat, 19 Nov 2016 10:20:00 +0100
References: <cde0ef35-c0a5-4180-b65b-7a3604d97380@googlegroups.com> <B1B0F433-F2EF-4987-8468-F0693CF4B338@gmail.com> <e0b40cdd-6d92-4ef0-a534-9ed086e2b081@googlegroups.com> <5C455288-1203-4D8C-BE55-7BDE4F2BF64E@gmail.com> <ec20f9c3-7ef2-4783-96a6-110c47f887c7@googlegroups.com>

The only problem is (I think) that such formulas cannot themselves be detected within the logic, correct?

Correct. The restriction to (countable) conjunctions of fairness conditions on sub-actions is just a sufficient condition.

Stephan

References:
- Nondeterminism and equivalence
  - From: Ron Pressler
- Re: [tlaplus] Nondeterminism and equivalence
  - From: Stephan Merz
- Re: [tlaplus] Nondeterminism and equivalence
  - From: Ron Pressler
- Re: [tlaplus] Nondeterminism and equivalence
  - From: Stephan Merz
- Re: [tlaplus] Nondeterminism and equivalence
  - From: Ron Pressler

Prev by Date: Re: [tlaplus] Nondeterminism and equivalence
Next by Date: Re: TLA+ Video Course
Previous by thread: Re: [tlaplus] Nondeterminism and equivalence
Next by thread: Re: Nondeterminism and equivalence
Index(es):
- Date
- Thread