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

Re: [tlaplus] TLA+ logic

> Now my question is whether the requirement to limit the domain ever makes a difference in practice so that it actually
> reduces expressivity.

Use TLAPLUS it is a good system. All what you need to work about an algorithm is here.