[
Date Prev
][
Date Next
][
Thread Prev
][
Thread Next
][
Date Index
][
Thread Index
]
Re: [tlaplus] TLA+ logic
From
: Ron Pressler <
r...@xxxxxxxxxxxxxxxxxxx
>
Date
: Thu, 10 Dec 2015 09:51:13 -0800 (PST)
References
: <
dbc52c84-b6ce-4326-aeec-a7c17dd257c0@googlegroups.com
> <
33ED3621-4D95-4167-9232-9404968DD8E7@gmail.com
> <
02b4212f-9e09-4759-96a6-d73e7ae0881f@googlegroups.com
> <
708CF982-1782-422F-8445-6C87C4E7D8D6@gmail.com
> <
57658c49-b05f-47df-9a41-df4992c873bc@googlegroups.com
> <
5f44d273-19c0-4086-973c-bbb620e7777b@googlegroups.com
> <
4ff7ce2d-b955-4953-b58b-8221b6594313@googlegroups.com
> <
60953B6B-6BF3-478F-BAA2-1EE39514B126@cs.uni-duesseldorf.de
> <
91ae46d4-9318-43b6-ac78-2f4ef819011b@googlegroups.com
> <
EDA72D76-C08E-4DAB-A62D-3066FF3D1451@cs.uni-duesseldorf.de
>
Nice! This means that we can also use TLA+ to spec
and check
all sorts of order-based algorithms.
If you're interested in algorithms to check, I would suggest a B-tree (
here's
a short implementation).
Ron
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:
Stephan Merz
Re: [tlaplus] TLA+ logic
From:
Leslie Lamport
Re: [tlaplus] TLA+ logic
From:
Chris Newcombe
Re: [tlaplus] TLA+ logic
From:
Ron Pressler
Re: [tlaplus] TLA+ logic
From:
Michael Leuschel
Re: [tlaplus] TLA+ logic
From:
Ron Pressler
Re: [tlaplus] TLA+ logic
From:
Michael Leuschel
Prev by Date:
Re: [tlaplus] TLA+ logic
Next by Date:
Re: [tlaplus] Recursive definitions of higher-order operators
Previous by thread:
Re: [tlaplus] TLA+ logic
Next by thread:
How to check if a variable increases or stays the same at each new state?
Index(es):
Date
Thread