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

Re: [tlaplus] TLA+ logic

From: fl <freder...@xxxxxxxxxxx>
Date: Fri, 4 Dec 2015 09:04:46 -0800 (PST)
References: <dbc52c84-b6ce-4326-aeec-a7c17dd257c0@googlegroups.com> <33ED3621-4D95-4167-9232-9404968DD8E7@gmail.com> <02b4212f-9e09-4759-96a6-d73e7ae0881f@googlegroups.com> <f77ca825-b389-47df-9470-c2caf60b6eb1@googlegroups.com> <f22db1b8-fc80-4f82-85a6-3abfcb0cdfb3@googlegroups.com> <7fad13e8-71b5-4a59-9539-43bc0c530d78@googlegroups.com>

> 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.

--

FL

References:
- TLA+ logic
  - From: Ron Pressler
- Re: [tlaplus] TLA+ logic
  - From: Stephan Merz
- Re: [tlaplus] TLA+ logic
  - From: Ron Pressler
- Re: [tlaplus] TLA+ logic
  - From: fl
- Re: [tlaplus] TLA+ logic
  - From: fl
- Re: [tlaplus] TLA+ logic
  - From: Ron Pressler

Prev by Date: Re: [tlaplus] TLA+ logic
Next by Date: Re: [tlaplus] TLA+ logic
Previous by thread: Re: [tlaplus] TLA+ logic
Next by thread: Re: [tlaplus] TLA+ logic
Index(es):
- Date
- Thread