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

*From*: "hengx...@xxxxxxxxx" <hengxin0912@xxxxxxxxx>*Date*: Tue, 6 Apr 2021 02:20:55 -0700 (PDT)

Hi All,

The following TLA+ code can be found at https://github.com/hengxin/tla-causal-consistency/blob/main/RelationUtils.tla.

-- I am able to generate an arbitrary linear extension of a partial order as follows (I use this algorithm: https://en.wikipedia.org/wiki/Topological_sorting#Kahn's_algorithm):

where Minimal(R, S) returns the set of minimal elements of S given relation R,

and LeftRestriction(R, m) returns the set of pairs whose first element is m.

However, I failed to generate all possible linear extensions of a partial order:

TLC reports an error: Unknown operator 'm'.

So how to generate all possible linear extensions of a partial order?

Best regards,

Hengfeng Wei (hengxin)

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/52111fcc-e8df-469e-8894-c113ae398056n%40googlegroups.com.

**Follow-Ups**:

- Prev by Date:
**Re: [tlaplus] How to express this set comprehension in TLA+?** - Next by Date:
**Re: [tlaplus] How to generate all possible linear extensions (i.e., topological sortings) of a partial order?** - Previous by thread:
**Re: [tlaplus] How to express this set comprehension in TLA+?** - Next by thread:
**Re: [tlaplus] How to generate all possible linear extensions (i.e., topological sortings) of a partial order?** - Index(es):