2473:------------------------------ MODULE Elevator ------------------------------ (***************************************************************************) (* This spec describes a simple multi-car elevator system. The actions in *) (* this spec are unsurprising and common to all such systems except for *) (* DispatchElevator, which contains the logic to determine which elevator *) (* ought to service which call. The algorithm used is very simple and does *) (* not optimize for global throughput or average wait time. The *) (* TemporalInvariant definition ensures this specification provides *) (* capabilities expected of any elevator system, such as people eventually *) (* reaching their destination floor. *) (***************************************************************************) EXTENDS Integers CONSTANTS Person,
422:
305:
1497:
1578:. TLAPS proofs are hierarchically structured, easing refactoring and enabling non-linear development: work can begin on later steps before all prior steps are verified, and difficult steps are decomposed into smaller sub-steps. TLAPS works well with TLC, as the model checker quickly finds small errors before verification is begun. In turn, TLAPS can prove system properties which are beyond the capabilities of finite model checking.
3110:
already moving toward the call floor in the same direction as the call. *) (* The system keeps no record of assigning an elevator to service a call. *) (* It is possible no elevator is able to service a call, but we are *) (* guaranteed an elevator will eventually become available. *) (***************************************************************************) DispatchElevator(c) == LET stationary ==
5523:
414:. According to Lamport, "I was sure that temporal logic was some kind of abstract nonsense that would never have any practical application, but it seemed like fun, so I attended." In 1980 he published "'Sometime' is Sometimes 'Not Never'", which became one of the most frequently-cited papers in the temporal logic literature. Lamport worked on writing temporal logic specifications during his time at
1241:
474:
was introduced in 2009, and the TLA proof system (TLAPS) in 2012. TLA was announced in 2014, adding some additional language constructs as well as greatly increasing in-language support for the proof system. Lamport is engaged in creating an updated TLA reference, "The TLA Hyperbook". The incomplete
1532:
As an alternative to exhaustive breadth-first search, TLC can use depth-first search or generate random behaviours. TLC operates on a subset of TLA; the model must be finite and enumerable, and some temporal operators are not supported. In distributed mode TLC cannot check liveness properties, nor
454:
TLA specifications mostly consisted of ordinary non-temporal mathematics, which
Lamport found less cumbersome than a purely temporal specification. TLA provided a mathematical foundation to the specification language TLA, introduced with the paper "Specifying Concurrent Systems with TLA" in 1999.
442:
His search for a practical method of specification resulted in the 1983 paper "Specifying
Concurrent Programming Modules", which introduced the idea of describing state transitions as boolean-valued functions of primed and unprimed variables. Work continued throughout the 1980s, and Lamport began
3109:
UNCHANGED <<PersonState, ActiveElevatorCalls>> (***************************************************************************) (* This action chooses an elevator to service the call. The simple *) (* algorithm picks the closest elevator which is either stationary or *) (*
1520:
over all defined state transitions. Execution stops when all state transitions lead to states which have already been discovered. If TLC discovers a state which violates a system invariant, it halts and provides a state trace path to the offending state. TLC provides a method of declaring model
1557:
Joint Centre to prove correctness of concurrent and distributed algorithms. The proof language is designed to be independent of any particular theorem prover; proofs are written in a declarative style, and transformed into individual obligations which are sent to back-end provers. The primary
339:
The usefulness of systems of this sort does not depend on any serious metaphysical assumption that time is discrete; they are applicable in limited fields of discourse in which we are concerned only with what happens next in a sequence of discrete states, e.g. in the working of a digital
636:
A clock which does not tick is not useful, so these behaviours should be disallowed. One solution is to disable stuttering, but TLA requires stuttering always be enabled; a stuttering step represents a change to some part of the system not described in the spec, and is useful for
2400:
The set of all firewall rules [remoteAddress : AddressRange, remotePort : PortRange, localAddress : AddressRange, localPort : PortRange, protocol : SUBSET Protocol, allow : BOOLEAN] Ruleset ==
1636:, and an internal distributed lock manager; some bugs required state traces of 35 steps. Model checking was also used to verify aggressive optimizations. In addition, TLA specifications were found to hold value as documentation and design aids.
272:
and mathematical theorems. The proofs are written in a declarative, hierarchical style independent of any single theorem prover backend. Both formal and informal structured mathematical proofs can be written in TLA; the language is similar to
1581:
TLAPS does not currently support reasoning with real numbers, nor most temporal operators. Isabelle and Zenon generally cannot prove arithmetic proof obligations, requiring use of the SMT solvers. TLAPS has been used to prove correctness of
3015:
Move the elevator to the next floor unless we have to open the doors here. LET eState == ElevatorState IN LET nextFloor == IF eState.direction = "Up" THEN eState.floor + 1 ELSE eState.floor - 1 IN
3084:
Stops the elevator if it's moved as far as it can in one direction LET eState == ElevatorState IN LET nextFloor == IF eState.direction = "Up" THEN eState.floor + 1 ELSE eState.floor - 1 IN
438: – arguing over whether the properties they listed were sufficient. I realized that, despite its aesthetic appeal, writing a specification as a conjunction of temporal properties just didn't work in practice.
491:
TLA specifications are organized into modules. Modules can extend (import) other modules to use their functionality. Although the TLA standard is specified in typeset mathematical symbols, existing TLA tools use
2890:
All people on this floor who are waiting for the elevator and travelling the same direction enter the elevator. LET eState == ElevatorState IN LET gettingOn == PeopleWaiting IN LET destinations ==
483:, described therein as "a work in progress that consists of the beginning of a series of video lectures to teach programmers and software engineers how to write their own TLA specifications".
1095:
TLA has a set of standard modules containing common operators. They are distributed with the syntactic analyzer. The TLC model checker uses Java implementations for improved performance.
2392:
The set of all packets [sourceAddress : Address, sourcePort : Port, destAddress : Address, destPort : Port, protocol : Protocol] Firewall ==
628:
The above spec disallows strange states for the one-bit clock, but does not say the clock will ever tick. For example, the following perpetually-stuttering behaviours are accepted:
882:
852:
280:
TLA was introduced in 1999, following several decades of research into a verification method for concurrent systems. Ever since, a toolchain has been developed, including an
2544:
Direction of travel required to move between current and destination floors IF destination > current THEN "Up" ELSE "Down" CanServiceCall ==
2304:<<store, tx, snapshotStore, written, missed>> ---------------------------------------------------------------------------- THEOREM Spec => (TypeInvariant /
564:
TLA concerns itself with defining the set of all correct system behaviours. For example, a one-bit clock ticking endlessly between 0 and 1 could be specified as follows:
822:
795:
292:
to TLA and is useful for specifying sequential algorithms. TLA was announced in 2014, expanding language support for proof constructs. The current TLA reference is
451:
in temporal formulas, which according to
Lamport "provides an elegant way to formalize and systematize all the reasoning used in concurrent system verification."
672:
Most specifications do not require assertion of liveness properties. Safety properties suffice both for model checking and guidance in system implementation.
234:
and mathematics, and the precision of specifications written in this language is intended to uncover design flaws before system implementation is underway.
434:
However, I became disillusioned with temporal logic when I saw how
Schwartz, Melliar-Smith, and Fritz Vogt were spending days trying to specify a simple
4613:
5570:
5565:
5555:
38:
954:
The foundational data structure of TLA is the set. Sets are either explicitly enumerated or constructed from other sets using operators or with
4437:
4237:
4198:
4147:
4087:
4040:
3999:
3822:
3722:
3548:
1590:, and the Spire consensus algorithm. It is distributed separately from the rest of the TLA tools and is free software, distributed under the
396:
568:
VARIABLE clock Init == clock \in {0, 1} Tick == IF clock = 0 THEN clock' = 1 ELSE clock' = 0 Spec == Init /\ _<<clock>>
5495:
5204:
4454:
2838:
Open the elevator doors if there is a call on this floor or the button for this floor was pressed. LET eState == ElevatorState IN /
241:. The model checker finds all possible system behaviours up to some number of execution steps, and examines them for violations of desired
4244:
Indeed, can get along quite well with specifications of the form (8.38) that express only safety properties and don't hide any variables.
1712:
The set of writes invisible to each transaction. ---------------------------------------------------------------------------- NoVal ==
281:
5229:
3473:
1441:
1390:
2991:
Close the elevator doors once all people have entered and exited the elevator on this floor. LET eState == ElevatorState IN /
447:
in 1990; however, it was not formally introduced until "The
Temporal Logic of Actions" was published in 1994. TLA enabled the use of
4944:
4525:
2787:
Person calls the elevator to go in a certain direction from their floor LET pState == PersonState IN LET call == ] IN /
5029:
620:
The safety properties of the one-bit clock – the set of reachable system states – are adequately described by the spec.
470:
Lamport published a full textbook on TLA in 2002, titled "Specifying
Systems: The TLA Language and Tools for Software Engineers".
5560:
5526:
5414:
5249:
5024:
3729:
Having to describe a design precisely often reveals problems - subtle interactions and "corner cases" that are easily overlooked.
435:
681:
5505:
5276:
5019:
657:
Weak fairness over an action means if that action is continuously enabled, it must eventually be taken. With weak fairness on
5159:
5119:
4776:
4766:
3478:
1563:
1145:
380:
246:
2320:------------------------------ MODULE Firewall ------------------------------ EXTENDS Integers CONSTANTS Address,
1610:
memory module during the process of writing a specification in TLA. TLA was used to write formal proofs of correctness for
5550:
5343:
4989:
4919:
4761:
4625:
392:
5446:
5259:
5139:
5124:
5049:
4606:
4538:
4273:
1513:
1347:
372:
242:
4287:
3974:
3945:
3535:
2983:
gettingOff THEN EXCEPT !.location = eState.floor, !.waiting = FALSE] ELSE PersonState] /
2943:
All people whose destination is this floor exit the elevator. LET eState == ElevatorState IN LET gettingOff ==
1529:
the state exploration step, and can run in distributed mode to spread the workload across a large number of computers.
5490:
5224:
5099:
5034:
3645:
1370:
1321:
1299:
353:
120:
91:
2501:
Tuple of all specification variables <<PersonState, ActiveElevatorCalls, ElevatorState>> Floor ==
5264:
4949:
4557:
4421:
4131:
4071:
1633:
1559:
741:
3543:. NATO Science Series, III: Computer and Systems Sciences. Vol. 173. Amsterdam: IOS Press. pp. 183–247.
5374:
5254:
5164:
4781:
4639:
4529:
3644:
Newcombe, Chris; Rath, Tim; Zhang, Fan; Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael (29 September 2014).
3503:
1546:
1040:
693:
444:
289:
265:
220:
3892:
923:
Temporal existential and universal quantification are included in TLA, although without support from the tools.
348:
in 1977. LTL became an important tool for analysis of concurrent programs, easily expressing properties such as
5500:
5441:
5348:
5281:
4979:
4806:
4644:
4205:
We seldom want to write a specification that isn't machine closed. If we do write one, it's usually by mistake.
3867:
3842:
1611:
1583:
927:
759:
is provided as the CHOOSE operator, which uniquely selects an arbitrary set element. Arithmetic operators over
737:
642:
227:
1245:
TLA IDE in typical use showing spec explorer on the left, editor in the middle, and parse errors on the right.
344:
Pnueli researched the use of temporal logic in specifying and reasoning about computer programs, introducing
5545:
5039:
4743:
4717:
4599:
3920:
1522:
661:
only a finite number of stuttering steps are permitted between ticks. This temporal logical statement about
379:'s method in his 1977 paper "Proving Correctness of Multiprocess Programs". Lamport's paper also introduced
4519:
3578:
476:
293:
4801:
4687:
4267:
3488:
989:
638:
4060:
3677:
2628:
An elevator has a floor button pressed only if a person in that elevator is going to that floor /
1680:--------------------------- MODULE KeyValueStore --------------------------- CONSTANTS Key,
1485:
1413:
5510:
5179:
5144:
5064:
4831:
4573:
2461:
matches : rule.allow =============================================================================
931:
685:
345:
4122:
3745:
4221:
4182:
4026:
3706:
4999:
4879:
4513:
4338:
3806:
2747:
PersonState.waiting ~> PersonState.location = PersonState.destination PickNewDestination(p) ==
2313:
1534:
1517:
1004:
943:
861:
831:
188:
45:
2548:
Whether elevator is in position to immediately service call LET eState == ElevatorState IN /
5433:
4974:
4722:
4697:
3652:
1621:
1449:
1385:
697:
388:
200:
2664:
A person is in an elevator only if the elevator is moving toward their destination floor /
5286:
5199:
5169:
4811:
4707:
4672:
4591:
4547:
4356:
4295:
4153:
3776:
3463:
TemporalInvariant) =============================================================================
1673:
1550:
1526:
1445:
689:
375:
in his 1975 paper "Proving
Assertions About Parallel Programs", which Lamport used to generalize
196:
151:
1079:
or constructed with operators from the standard
Sequences module. Sets of tuples are defined by
888:
will always be true. Other temporal operators include weak and strong fairness. Weak fairness WF
804:
4389:
195:. It is used for designing, modelling, documentation, and verification of programs, especially
5389:
5321:
5174:
5129:
5044:
4914:
4841:
4433:
4233:
4194:
4143:
4083:
4036:
3995:
3818:
3768:
3718:
3544:
1647:
1575:
1208:: Provides utility functions for model-checked specifications, such as logging and assertions.
1080:
709:
415:
208:
5456:
4994:
4702:
4692:
4425:
4346:
4135:
4075:
3987:
3810:
3760:
2743:
If a person waits for their elevator, they'll eventually arrive at their floor /
2540:
The distance between two floors IF f1 > f2 THEN f1 - f2 ELSE f2 - f1 GetDirection ==
1397:
1199:
935:
777:
753:
349:
332:
139:
127:
3868:"The Writings of Leslie Lamport: On-the-fly Garbage Collection: an Exercise in Cooperation"
2308:
TxLifecycle) =============================================================================
930:. Operators differ from functions in that their domain need not be a set: for example, the
669:: it shouldn't constrain the set of reachable states, only the set of possible behaviours.
5485:
5306:
5244:
5154:
5079:
5004:
4984:
4712:
4489:
3983:
2815:
ElevatorState.doorsOpen THEN ActiveElevatorCalls ELSE ActiveElevatorCalls
2751:
Person decides they need to go to a different floor LET pState == PersonState IN /
1669:
1639:
1496:
1266:
1165:
939:
768:
460:
448:
400:
376:
57:
50:
37:
4373:
3440:
Initialize state with Init and transition with Next, subject to
TemporalAssumptions /
2987:
UNCHANGED <<ActiveElevatorCalls, ElevatorState>> CloseElevatorDoors(e) ==
2485:
The number of floors serviced by the elevator system VARIABLES PersonState,
4342:
2525:
Elevator movement state; it is either moving in a direction or stationary
Direction
632:
0 -> 0 -> 0 -> 0 -> 0 -> ... 1 -> 1 -> 1 -> 1 -> 1 -> ...
616:
0 -> 1 -> 0 -> 1 -> 0 -> ... 1 -> 0 -> 1 -> 0 -> 1 -> ...
5311:
5054:
4869:
4864:
4821:
4667:
4479:
4385:
4229:
4217:
4190:
4178:
4118:
4056:
4032:
4022:
3970:
3941:
3916:
3888:
3863:
3838:
3741:
3714:
3702:
3673:
3574:
3531:
3498:
1654:
604:
is a temporal formula asserting all behaviours of one-bit clock must initially satisfy
426:
364:
320:
258:
238:
237:
Since TLA specifications are written in a formal language, they are amenable to finite
192:
132:
62:
5539:
5271:
5239:
5209:
4909:
4677:
4360:
3780:
1505:
1141:
480:
456:
4121:; Merz, Stephan; Ricketts, Daniel; Vanzetto, Hernán (1 January 2012). "TLA Proofs".
3197:
GetDistance.floor, c.floor] <= GetDistance.floor, c.floor] IN IF closest
2140:
Merge snapshotStore writes into store. THEN snapshotStore ELSE store] /
537:– an expression containing variables and constants that is not a next-state relation
5134:
4954:
4899:
4894:
4581:
4534:
4157:
2931:
gettingOn THEN EXCEPT !.location = e] ELSE PersonState] /
1615:
1587:
1509:
1185:
411:
371:
found an error in a paper he submitted on mutual exclusion. Ed Ashcroft introduced
324:
312:
4586:
4226:
Specifying Systems: The TLA Language and Tools for Hardware and Software Engineers
4187:
Specifying Systems: The TLA Language and Tools for Hardware and Software Engineers
4028:
Specifying Systems: The TLA Language and Tools for Hardware and Software Engineers
3843:"The Writings of Leslie Lamport: Proving the Correctness of Multiprocess Programs"
3711:
Specifying Systems: The TLA Language and Tools for Hardware and Software Engineers
2588:
Statements about the variables which we expect to hold in every system state /
1240:
4939:
4139:
2783:
UNCHANGED <<ActiveElevatorCalls, ElevatorState>> CallElevator(p) ==
684:, so operations on variables involve set manipulation. The language includes set
165:
5353:
5084:
4904:
4727:
4682:
4577:
4429:
4351:
4322:
4079:
1657:
1591:
1468:
1460:
The SANY syntactic analyzer, which parses and checks the spec for syntax errors.
1402:
1103:
760:
368:
360:
328:
308:
144:
3801:Øhrstrøm, Peter; Hasle, Per (1995). "3.7 Temporal Logic and Computer Science".
3011:
UNCHANGED <<PersonState, ActiveElevatorCalls>> MoveElevator(e) ==
1708:
A log of writes performed within each transaction. missed
5419:
5394:
5369:
4924:
4836:
4816:
4791:
4563:
4553:
4543:
4483:
4458:
3814:
3764:
3508:
3080:
UNCHANGED <<PersonState, ActiveElevatorCalls>> StopElevator(e) ==
1261:
1251:
269:
254:
204:
3772:
1516:. TLC generates a set of initial states satisfying the spec, then performs a
904:(i.e. without interruptions), it must eventually be taken. Strong fairness SF
5399:
5316:
5194:
5009:
4964:
4929:
4874:
4622:
4395:
3991:
3612:
2684:
ElevatorState.direction = GetDirection.floor, PersonState.destination] /
1716:
Choose something to represent the absence of a value. CHOOSE v : v
1643:
1629:
1603:
1270:
1155:
979:
421:
17:
3921:"The Writings of Leslie Lamport: Specifying Concurrent Programming Modules"
665:
is called a liveness assertion. In general, a liveness assertion should be
359:
Concurrent with Pnueli's work on LTL, academics were working to generalize
311:
applied temporal logic to computer science, for which he received the 1996
4262:(Recording of technical talk). TLA Community Event 2014, Toulouse, France.
920:(repeatedly, with or without interruptions), it must eventually be taken.
5464:
5379:
5189:
5149:
5074:
5059:
5014:
4796:
4786:
4567:
4323:"Spire: A Cooperative, Phase-Symmetric Solution to Distributed Consensus"
3607:
3483:
2493:
The set of all active elevator calls ElevatorState
2466:
1704:
Snapshots of the store for each transaction. written,
1625:
1607:
1189:
1175:
764:
701:
653:
Spec == Init /\ _<<clock>> /\ WF_<<clock>>(Tick)
407:
384:
250:
4455:"With Cosmos DB, Microsoft wants to build one database to rule them all"
2680:
ElevatorState.floor /= PersonState.destination) => /
2477:
The set of all people using the elevator system Elevator,
425:
TLA was developed by computer scientist and 2013 Turing award recipient
304:
226:
For design and documentation, TLA fulfills the same purpose as informal
5296:
5214:
5184:
5114:
5089:
4969:
4889:
4826:
3629:
3602:
3493:
1969:
Using transaction t, update the value associated with key k to v. /
471:
331:
was the first to seriously study the applications of temporal logic to
285:
216:
277:, and tools exist to translate TLA specifications to LaTeX documents.
5469:
5337:
5094:
5069:
4934:
4884:
3893:"The Writings of Leslie Lamport: 'Sometime' is Sometimes 'Not Never'"
3616:
1353:
1121:
1060:
946:). Recursive and anonymous user-defined operators were added in TLA.
705:
464:
1158:. Provides primitive set operation analogues and duplicate counting.
395:, respectively. This method was used to verify the first concurrent
3205:
UNCHANGED <<PersonState, ActiveElevatorCalls>> Init ==
1700:
The set of open snapshot transactions. snapshotStore,
774:
Temporal logic operators are built into TLA. Temporal formulas use
5409:
5384:
5291:
5219:
5109:
4771:
4299:
2939:
UNCHANGED <<ActiveElevatorCalls>> ExitElevator(e) ==
1571:
1554:
1495:
1464:
1083:; for example, the set of all pairs of natural numbers is defined
497:
493:
420:
303:
274:
231:
230:. However, TLA specifications are written in a formal language of
4516:, Leslie Lamport's webpage linking to the TLA tools and resources
1926:
UNCHANGED <<written, missed, store>> Add(t, k, v) ==
1696:
A data store mapping keys to values. tx,
5404:
5234:
4959:
4859:
4334:
3336:
ElevatorCall : DispatchElevator(c) TemporalAssumptions ==
3118:
Elevator : ElevatorState.direction = "Stationary"
2834:
UNCHANGED <<ElevatorState>> OpenElevatorDoors(e) ==
2054:
UNCHANGED <<tx, missed, store>> RollbackTx(t) ==
1965:
UNCHANGED <<tx, missed, store>> Update(t, k, v) ==
1930:
Using transaction t, add value v to the store under key k. /
1831:
we haven't written it, we must have missed a write.
1567:
406:
Lamport first encountered Pnueli's LTL during a 1978 seminar at
4595:
3946:"The Writings of Leslie Lamport: The Temporal Logic of Actions"
2297:
Initialize state with Init and transition with Next. Init /
2163:
Update the missed writes for other open transactions.
1500:
States and transitions discovered by TLC for the one-bit clock.
5301:
5104:
2616:
Some more comprehensive checks beyond the type invariant /
2058:
Close the transaction without merging writes into store. /
1624:
has used TLA since 2011. TLA model checking uncovered bugs in
1594:. TLA greatly expanded language support for proof constructs.
1453:
992:
in TLA assign a value to each element in their domain, a set.
284:
and a distributed model checker. The pseudocode-like language
4257:
3803:
Temporal Logic: From Ancient Ideas to Artificial Intelligence
3201:
stationary THEN = ] ELSE ElevatorState /
2489:
The state of each person ActiveElevatorCalls,
2405:
The set of all firewall rulesets SUBSET Rule Allowed ==
1755:
All snapshotStore values are initially NoVal. ] /
3340:
Assumptions about how elevators and people will behave /
2015:
UNCHANGED <<tx, missed, store>> Remove(t, k) ==
1867:
Checks transactions are cleaned up after disposal. /
1692:The set of all transaction IDs. VARIABLES store,
1022:
is a true statement in TLA. Functions are also defined with
531:– a relation describing how variables can change in any step
1771:
All missed writes are initially empty. TypeInvariant ==
459:
for TLA specifications; TLC was used to find errors in the
3209:
Initializes people and elevators to arbitrary floors /
2886:
UNCHANGED <<PersonState>> EnterElevator(e) ==
2715:
Every call is eventually serviced by an elevator /
2521:
The set of all elevator calls ElevatorDirectionState ==
2505:
The set of all floors 1 .. FloorCount Direction ==
2409:
Whether the ruleset allows the packet LET matches ==
3044:
Can move only if other elevator servicing call /
1537:
as a command line tool or bundled with the TLA toolbox.
335:, Prior speculated on its use a decade earlier in 1967:
3805:. Studies in Linguistics and Philosophy. Vol. 57.
3455:
TemporalAssumptions THEOREM Spec => (TypeInvariant /
2019:
Using transaction t, remove key k from the store. /
555:– an expression containing statements in temporal logic
4485:
Foundations of Azure Cosmos DB with Dr. Leslie Lamport
3173:
ElevatorState' = LET closest == CHOOSE e
2560:The set of all people waiting on an elevator call
1747:
The set of open transactions is initially empty. /
1646:, a globally-distributed database with five different
1586:, the Memoir security architecture, components of the
1063:
are included in TLA. They are explicitly defined with
4576:, a TLA introduction by Leslie Lamport included in a
4420:. Lecture Notes in Computer Science. Vol. 8477.
4130:. Lecture Notes in Computer Science. Vol. 7436.
4070:. Lecture Notes in Computer Science. Vol. 5684.
3982:. Lecture Notes in Computer Science. Vol. 1703.
2703:
Expectations about elevator system capabilities /
2109:
Close transaction t, merging writes into store. /
864:
834:
807:
780:
1046:
is a record with fields name and age, accessed with
828:
is eventually true. The operators are combined into
479:
from his official website. Lamport is also creating
261:
to define liveness (good things eventually happen).
5478:
5455:
5432:
5362:
5330:
4850:
4752:
4736:
4660:
4653:
4632:
4554:
Who Builds a Skyscraper without Drawing Blueprints?
3678:"Why We Should Build Software Like We Build Houses"
2580:
GetDirection.location, PersonState.destination] = d
1688:The set of all values. TxId
1408:
1396:
1384:
1376:
1366:
1346:
1320:
1298:
1276:
1260:
1250:
500:. TLA uses several terms which require definition:
160:
150:
138:
126:
116:
90:
68:
56:
44:
4418:Abstract State Machines, Alloy, B, TLA, VDM, and Z
3526:
3524:
2856:ActiveElevatorCalls : CanServiceCall
876:
846:
816:
789:
2636:ElevatorState.buttonsPressed : /
2556:c.direction = eState.direction PeopleWaiting ==
2509:Directions available to this elevator system
2481:The set of all elevators FloorCount
2324:The set of all addresses Port,
1684:The set of all keys. Val,
641:. To ensure the clock must eventually tick, weak
612:or be stuttering steps. Two such behaviours are:
4416:Chris, Newcombe (2014). "Why Amazon Chose TLA".
3976:Correct Hardware Design and Verification Methods
3020:eState.direction /= "Stationary" /
2911:eState.direction /= "Stationary" /
549:– a state predicate true in all reachable states
203:. TLA is considered to be exhaustively-testable
4112:
4110:
4108:
4106:
3911:
3909:
3134:ElevatorState.direction = c.direction /
2872:ActiveElevatorCalls' = ActiveElevatorCalls
1549:proofs written in TLA. It was developed at the
1533:check random or depth-first behaviours. TLC is
1256:Simon Zambrovski, Markus Kuppe, Daniel Ricketts
1168:along with inequality and arithmetic operators.
432:
337:
257:to define safety (bad things won't happen) and
4394:(Recording of technical talk). San Francisco:
3964:
3962:
3753:Journal of Fixed Point Theory and Applications
3646:"Use of Formal Methods at Amazon Web Services"
4607:
4068:Theoretical Aspects of Computing - ICTAC 2009
3973:(1999). "Model Checking TLA Specifications".
2328:The set of all ports Protocol
525:– a step during which variables are unchanged
8:
2692:ActiveElevatorCalls : PeopleWaiting /=
1233:
455:Later that same year, Yuan Yu wrote the TLC
418:, but found the approach to be impractical:
30:
4526:How Amazon Web Services Uses Formal Methods
4222:"8.9.6 Temporal Logic Considered Confusing"
3569:
3567:
3145:GetDirection.floor, c.floor] = c.direction
2795:pState.location /= pState.destination /
1736:All store values are initially NoVal. /
519:– a pair of successive states in a behavior
363:for verification of multiprocess programs.
327:in 1957, then called tense logic. Although
4657:
4614:
4600:
4592:
3303:Elevator : CloseElevatorDoors(e)
3141:ElevatorState.floor = c.floor
2648:PersonState.location = e /
1875:Key : snapshotStore = NoVal /
1239:
1232:
1043:are a type of function in TLA. The record
29:
4350:
3639:
3637:
3270:Elevator : OpenElevatorDoors(e)
2332:The set of all protocols AddressRange ==
2132:Detection of write-write conflicts. /
1763:All write logs are initially empty. /
1724:The set of all key-value stores. Init ==
1512:model of TLA specifications for checking
863:
833:
806:
779:
771:are available from the standard modules.
3248:Person : PickNewDestination(p)
2951:Person : PersonState.location = e /
4574:Euclid Writes an Algorithm: A Fairytale
4546:, a talk by Leslie Lamport at the 2014
3520:
1606:, a critical bug was discovered in the
1448:. It includes an editor with error and
1327:1.8.0 Clarke / December 6, 2020
1305:1.7.2 Theano / February 2, 2022
1212:Standard modules are imported with the
1029:, or by modifying an existing function
367:became interested in the problem after
4564:Programming Should Be More than Coding
4265:
3537:Specifying Concurrent Systems with TLA
2955:PersonState.destination = eState.floor
2799:ActiveElevatorCalls' = IF
1456:front-end to several other TLA tools:
1054:, and belonging to the set of records
995:is the set of all functions with f in
926:User-defined operators are similar to
507:– an assignment of values to variables
3281:Elevator : EnterElevator(e)
2699:No ghost calls TemporalInvariant ==
2136:store' =
1751:snapshotStore =
942:in ZFC (since its existence leads to
266:machine-checked proofs of correctness
7:
5496:Microsoft Open Specification Promise
5205:Text Template Transformation Toolkit
4626:free and open-source software (FOSS)
4391:Thinking for Programmers (at 21m46s)
3630:https://tlaplus.codeplex.com/license
3325:Elevator : StopElevator(e)
3314:Elevator : MoveElevator(e)
3292:Elevator : ExitElevator(e)
3193:approaching : /
2731:Elevator : CanServiceCall /
2035:snapshotStore' = = NoVal] /
1922:snapshotStore' = = store] /
1839:Key : (store /= snapshotStore /
4453:Lardinois, Frederic (10 May 2017).
4117:Cousineau, Denis; Doligez, Damien;
3746:"How to Write a 21st Century Proof"
3089:~ENABLED OpenElevatorDoors(e) /
2497:The state of each elevator Vars ==
4522:, a TLA textbook by Leslie Lamport
3474:Communicating sequential processes
3436:Vars(DispatchElevator(c)) Spec ==
3259:Person : CallElevator(p)
3048:CanServiceCall => /
2572:PersonState.location = f /
2336:The set of all address ranges
1442:integrated development environment
1391:Integrated development environment
25:
3400:Vars(CloseElevatorDoors(e)) /
3056:Elevator : /
2895:PersonState.destination : p
2652:PersonState.destination = f /
2396:The set of all firewalls Rule ==
1198:: Provides definitions useful in
543:– a Boolean-valued state function
5522:
5521:
5415:TPM 2.0 Reference Implementation
5250:Windows Communication Foundation
5025:Microsoft Automatic Graph Layout
4061:"The PlusCal Algorithm Language"
3969:Yu, Yuan; Manolios, Panagiotis;
3364:Vars(OpenElevatorDoors(e)) /
3181:approaching : /
2513:"Up", "Down"
2105:UNCHANGED store CloseTx(t) ==
1996:snapshotStore' = = v] /
1946:snapshotStore' = = v] /
1545:The TLA Proof System, or TLAPS,
1011:. For example, the TLA function
608:and have all steps either match
36:
5506:Open Source Security Foundation
5277:Windows Presentation Foundation
5020:Managed Extensibility Framework
4528:, an article in the April 2015
4321:Koutanov, Emil (12 July 2021).
4256:Markus A. Kuppe (3 June 2014).
3105:ElevatorState' = = ] /
3076:ElevatorState' = = ] /
3007:ElevatorState' = = ] /
2995:~ENABLED EnterElevator(e) /
2935:ElevatorState' = = ] /
2868:ElevatorState' = = ] /
2644:Person : /
2364:The set of all port ranges
2252:Val : Update(t, k, v)
2175:snapshotStore' = = ] /
2085:snapshotStore' = = ] /
877:{\displaystyle \Diamond \Box P}
847:{\displaystyle \Box \Diamond P}
399:algorithm in a 1978 paper with
253:. TLA specifications use basic
133:Cross-platform (multi-platform)
5571:Concurrency (computer science)
5566:Formal specification languages
5556:Software using the BSD license
5160:Python Tools for Visual Studio
5120:Open Management Infrastructure
5030:Microsoft C++ Standard Library
4556:, a talk by Leslie Lamport at
4537:, a talk by Leslie Lamport at
3479:Alloy (specification language)
2999:~ENABLED ExitElevator(e) /
2775:f /= pState.location /
736:are also included, as well as
97:TLA / January 15, 2014
1:
2830:PersonState' = = ] /
2807:Elevator : /
2779:PersonState' = = ] /
2672:Elevator : /
2576:PersonState.waiting /
2293:tx : CloseTx(t) Spec ==
2187:The next-state relation.
1895:Open a new transaction. /
1616:Pastry distributed hash table
1588:Pastry distributed hash table
1521:symmetries to defend against
858:is true infinitely often, or
27:Formal specification language
5447:Microsoft Reciprocal License
5125:Open Neural Network Exchange
5050:Microsoft Enterprise Library
4288:"Unsupported TLAPS features"
4140:10.1007/978-3-642-32759-9_14
3376:Vars(EnterElevator(e)) /
3237:The next-state relation
2811:CanServiceCall /
2552:c.floor = eState.floor /
2282:tx : RollbackTx(t)
2271:Key : Remove(t, k)
2225:Val : Add(t, k, v)
2031:snapshotStore /= NoVal /
1728:The initial predicate. /
1562:and Zenon, with fallback to
496:-like symbol definitions in
5225:Virtual File System for Git
5100:Neural Network Intelligence
5035:Microsoft Cognitive Toolkit
4430:10.1007/978-3-662-43652-3_3
4352:10.1109/ACCESS.2021.3096326
4080:10.1007/978-3-642-03466-4_2
3424:Vars(StopElevator(e)) /
3412:Vars(MoveElevator(e)) /
3388:Vars(ExitElevator(e)) /
3352:Vars(CallElevator(p)) /
3040:ActiveElevatorCalls :
3032:eState.buttonsPressed /
2979:Person |-> IF p
2927:Person |-> IF p
2864:eState.buttonsPressed /
2676:(PersonState.location = e /
1942:snapshotStore = NoVal /
584:in the next state) to 1 if
5587:
4488:(Recording of interview).
4422:Springer Berlin Heidelberg
4132:Springer Berlin Heidelberg
4072:Springer Berlin Heidelberg
3579:"TLA: A Preliminary Guide"
3122:IN LET approaching ==
2723:ActiveElevatorCalls ~>
2360:a <= r PortRange ==
2198:TxId : OpenTx(t)
1827:If store != snapshot
1484:The IDE is distributed in
1154:: Module for working with
1102:: Module for working with
817:{\displaystyle \Diamond P}
592:is 1. The state predicate
264:TLA is also used to write
5519:
5375:Extensible Storage Engine
5255:Windows Driver Frameworks
5165:R Tools for Visual Studio
5040:Microsoft Design Language
4640:Microsoft and open source
4530:Communications of the ACM
3815:10.1007/978-0-585-37463-5
3765:10.1007/s11784-012-0071-6
3603:"Tlaplus Tools - License"
3504:Temporal logic of actions
3157:ActiveElevatorCalls /
3130:Elevator : /
3060:e /= e2 /
1775:The type invariant. /
1653:Altreonic NV used TLA to
1444:is implemented on top of
1342:
1294:
1238:
1015:is an element of the set
445:temporal logic of actions
443:publishing papers on the
221:Temporal Logic of Actions
207:, and its use likened to
112:
86:
35:
5501:Open Letter to Hobbyists
5442:Microsoft Public License
5340:(v1.25, v2.0 & v4.0)
5282:Windows Template Library
4980:Dynamic Language Runtime
4645:Shared Source Initiative
4535:Thinking for Programmers
4272:: CS1 maint: location (
2471:
2429:InAddressRange /
2421:InAddressRange /
2348:Address : r <= r
2318:
1678:
1467:translator, to generate
1188:along with division and
938:as its domain, which is
651:
630:
614:
596:is true if the value of
572:The next-state relation
566:
288:was created in 2009; it
228:technical specifications
5561:Specification languages
4718:Windows Package Manager
4544:Thinking Above the Code
4183:"8.9.2 Machine Closure"
4124:FM 2012: Formal Methods
3992:10.1007/3-540-48153-2_6
3093:~eState.doorsOpen /
3024:~eState.doorsOpen /
2842:~eState.doorsOpen /
2612:] SafetyInvariant ==
2568:Person : /
2352:InAddressRange == /
1523:combinatorial explosion
1480:The TLAPS proof system.
1474:The PlusCal translator.
1120:: Defines operators on
117:Implementation language
5491:F# Software Foundation
3489:Computation tree logic
3432:ElevatorCall : SF
3221:ActiveElevatorCalls =
3003:eState.doorsOpen /
2975:PersonState' = [p
2963:eState.doorsOpen /
2923:PersonState' = [p
2907:eState.doorsOpen /
2771:Floor : /
2532:"Stationary"
2388:p <= r Packet ==
1614:and components of the
1501:
1477:The TLC model checker.
1282:; 14 years ago
878:
848:
818:
791:
790:{\displaystyle \Box P}
513:– a sequence of states
440:
430:
387:as generalizations of
342:
316:
211:for software systems;
191:language developed by
99:; 10 years ago
74:; 25 years ago
5511:Outercurve Foundation
5065:Mixed Reality Toolkit
2791:~pState.waiting /
2755:~pState.waiting /
2711:ElevatorCall :
2433:InPortRange /
2425:InPortRange /
2417:rset : /
2376:Port : r <= r
1558:back-end provers are
1514:invariance properties
1499:
1329:; 3 years ago
1307:; 2 years ago
1280:February 4, 2010
962:is some condition on
879:
849:
819:
792:
424:
346:linear temporal logic
307:
5551:Formal methods tools
5000:Fluent Design System
4880:.NET Micro Framework
4587:The TLA Google Group
4134:. pp. 147–154.
3809:. pp. 344–365.
3807:Springer Netherlands
3064:CanServiceCall /
2600:ActiveElevatorCalls
2584:TypeInvariant ==
2380:InPortRange == /
2039:written' = = @
2000:written' = = @
1950:written' = = @
1815:TxLifecycle == /
1518:breadth-first search
1025:for some expression
974:is some function of
862:
832:
805:
801:is always true, and
778:
481:The TLA Video Course
189:formal specification
4723:WorldWide Telescope
4698:Microsoft PowerToys
4343:2021IEEEA...9j1702K
3676:(25 January 2013).
3577:(15 January 2014).
1642:used TLA to design
1622:Amazon Web Services
1547:mechanically checks
1450:syntax highlighting
1235:
884:to mean eventually
529:Next-state relation
389:partial correctness
296:by Leslie Lamport.
245:properties such as
201:distributed systems
152:Filename extensions
72:April 23, 1999
69:First appeared
32:
5287:Windows UI Library
5200:T2 Temporal Prover
5170:RecursiveExtractor
4832:Small Basic Online
4708:Windows Calculator
4560:San Francisco 2014
4548:Microsoft Research
4424:. pp. 25–39.
4296:Microsoft Research
4074:. pp. 36–60.
4059:(2 January 2009).
3986:. pp. 54–66.
3420:Elevator : WF
3408:Elevator : SF
3396:Elevator : SF
3384:Elevator : WF
3372:Elevator : WF
3360:Elevator : WF
2604:ElevatorCall /
2536:GetDistance ==
2179:written' = =
2089:written' = =
1767:missed =
1759:written =
1674:snapshot isolation
1648:consistency models
1551:Microsoft Research
1502:
1252:Original author(s)
982:is represented as
968:{e : x \in S}
956:{x \in S : p}
912:) means if action
896:) means if action
874:
844:
814:
787:
712:operators such as
600:is either 0 or 1.
431:
397:garbage collection
317:
209:drawing blueprints
197:concurrent systems
5533:
5532:
5428:
5427:
5331:Operating systems
5322:Z3 Theorem Prover
5130:Open Service Mesh
5045:Microsoft Detours
4915:ASP.NET Web Forms
4853:development tools
4570:by Leslie Lamport
4566:, a 2015 talk at
4520:The TLA Hyperbook
4514:The TLA Home Page
4439:978-3-662-43651-6
4337:: 101702–101717.
4239:978-0-321-14306-8
4200:978-0-321-14306-8
4149:978-3-642-32758-2
4089:978-3-642-03465-7
4042:978-0-321-14306-8
4001:978-3-540-66559-5
3824:978-0-7923-3586-3
3724:978-0-321-14306-8
3707:"7.1 Why Specify"
3550:978-90-5199-459-9
3459:SafetyInvariant /
2739:Person :
2660:Person :
2624:Elevator :
2159:missed' =
2097:missed' = =
1847:written) => k
1438:
1437:
1081:Cartesian product
944:Russell's paradox
934:operator has the
710:First-order logic
352:and freedom from
323:was developed by
294:The TLA Hyperbook
182:
181:
16:(Redirected from
5578:
5525:
5524:
4995:Entity Framework
4693:Open Live Writer
4658:
4616:
4609:
4602:
4593:
4501:
4500:
4498:
4496:
4476:
4470:
4469:
4467:
4465:
4450:
4444:
4443:
4413:
4407:
4406:
4404:
4402:
4388:(3 April 2014).
4382:
4376:
4374:TLA Proof System
4371:
4365:
4364:
4354:
4318:
4312:
4311:
4309:
4307:
4292:TLA Proof System
4284:
4278:
4277:
4271:
4263:
4253:
4247:
4246:
4220:(18 June 2002).
4214:
4208:
4207:
4181:(18 June 2002).
4175:
4169:
4168:
4166:
4164:
4129:
4114:
4101:
4100:
4098:
4096:
4065:
4053:
4047:
4046:
4025:(18 June 2002).
4019:
4013:
4012:
4010:
4008:
3981:
3966:
3957:
3956:
3954:
3952:
3938:
3932:
3931:
3929:
3927:
3913:
3904:
3903:
3901:
3899:
3885:
3879:
3878:
3876:
3874:
3860:
3854:
3853:
3851:
3849:
3835:
3829:
3828:
3798:
3792:
3791:
3789:
3787:
3750:
3738:
3732:
3731:
3705:(18 June 2002).
3699:
3693:
3692:
3690:
3688:
3670:
3664:
3663:
3661:
3659:
3650:
3641:
3632:
3628:
3626:
3624:
3599:
3593:
3592:
3590:
3588:
3583:
3571:
3562:
3561:
3559:
3557:
3542:
3534:(January 2000).
3528:
3462:
3458:
3454:
3450:
3447:
3443:
3439:
3435:
3431:
3427:
3423:
3419:
3415:
3411:
3407:
3403:
3399:
3395:
3391:
3387:
3383:
3379:
3375:
3371:
3367:
3363:
3359:
3355:
3351:
3348:Person : WF
3347:
3343:
3339:
3335:
3331:
3328:
3324:
3320:
3317:
3313:
3309:
3306:
3302:
3298:
3295:
3291:
3287:
3284:
3280:
3276:
3273:
3269:
3265:
3262:
3258:
3254:
3251:
3247:
3243:
3240:
3236:
3232:
3228:
3224:
3220:
3216:
3212:
3208:
3204:
3200:
3196:
3192:
3188:
3184:
3180:
3176:
3172:
3168:
3164:
3160:
3156:
3152:
3148:
3144:
3140:
3137:
3133:
3129:
3125:
3121:
3117:
3113:
3108:
3104:
3100:
3096:
3092:
3088:
3083:
3079:
3075:
3071:
3067:
3063:
3059:
3055:
3051:
3047:
3043:
3039:
3035:
3031:
3027:
3023:
3019:
3014:
3010:
3006:
3002:
2998:
2994:
2990:
2986:
2982:
2978:
2974:
2970:
2966:
2962:
2958:
2954:
2950:
2946:
2942:
2938:
2934:
2930:
2926:
2922:
2918:
2914:
2910:
2906:
2902:
2898:
2894:
2889:
2885:
2881:
2878:
2875:
2871:
2867:
2863:
2859:
2855:
2851:
2848:
2845:
2841:
2837:
2833:
2829:
2825:
2821:
2818:
2814:
2810:
2806:
2802:
2798:
2794:
2790:
2786:
2782:
2778:
2774:
2770:
2766:
2762:
2759:pState.location
2758:
2754:
2750:
2746:
2742:
2738:
2734:
2730:
2726:
2722:
2718:
2714:
2710:
2706:
2702:
2698:
2695:
2691:
2687:
2683:
2679:
2675:
2671:
2667:
2663:
2659:
2655:
2651:
2647:
2643:
2639:
2635:
2631:
2627:
2623:
2619:
2615:
2611:
2607:
2603:
2599:
2595:
2591:
2587:
2583:
2579:
2575:
2571:
2567:
2563:
2559:
2555:
2551:
2547:
2543:
2539:
2535:
2531:
2528:
2524:
2520:
2517:ElevatorCall ==
2516:
2512:
2508:
2504:
2500:
2496:
2492:
2488:
2484:
2480:
2476:
2460:
2456:
2452:
2448:
2444:
2440:
2436:
2432:
2428:
2424:
2420:
2416:
2412:
2408:
2404:
2399:
2395:
2391:
2387:
2383:
2379:
2375:
2371:
2367:
2363:
2359:
2355:
2351:
2347:
2343:
2339:
2335:
2331:
2327:
2323:
2307:
2303:
2300:
2296:
2292:
2288:
2285:
2281:
2277:
2274:
2270:
2266:
2262:
2258:
2255:
2251:
2247:
2243:
2239:
2235:
2231:
2228:
2224:
2220:
2216:
2212:
2208:
2204:
2201:
2197:
2193:
2190:
2186:
2182:
2178:
2174:
2170:
2166:
2162:
2158:
2154:
2150:
2147:
2143:
2139:
2135:
2131:
2128:
2124:
2120:
2116:
2112:
2108:
2104:
2100:
2096:
2092:
2088:
2084:
2080:
2076:
2073:
2069:
2065:
2061:
2057:
2053:
2049:
2045:
2042:
2038:
2034:
2030:
2026:
2022:
2018:
2014:
2010:
2006:
2003:
1999:
1995:
1991:
1987:
1984:
1980:
1976:
1972:
1968:
1964:
1960:
1956:
1953:
1949:
1945:
1941:
1937:
1933:
1929:
1925:
1921:
1917:
1913:
1910:
1906:
1902:
1898:
1894:
1891:OpenTx(t) ==
1890:
1886:
1882:
1878:
1874:
1870:
1866:
1862:
1858:
1854:
1850:
1846:
1842:
1838:
1834:
1830:
1826:
1822:
1818:
1814:
1810:
1806:
1802:
1798:
1794:
1790:
1786:
1782:
1778:
1774:
1770:
1766:
1762:
1758:
1754:
1750:
1746:
1743:
1739:
1735:
1732:store =
1731:
1727:
1723:
1720:Val Store ==
1719:
1715:
1711:
1707:
1703:
1699:
1695:
1691:
1687:
1683:
1434:
1431:
1429:
1427:
1425:
1423:
1421:
1419:
1417:
1415:
1362:
1359:
1357:
1355:
1337:
1335:
1330:
1315:
1313:
1308:
1290:
1288:
1283:
1243:
1236:
1219:
1215:
1200:real-time system
1091:Standard modules
1086:
1078:
1056:
1053:
1049:
1045:
1036:
1024:
1021:
1017:
1014:
994:
985:
969:
957:
936:category of sets
883:
881:
880:
875:
853:
851:
850:
845:
823:
821:
820:
815:
796:
794:
793:
788:
757:
751:
747:
735:
731:
727:
723:
719:
715:
680:TLA is based on
645:is asserted for
580:′ (the value of
553:Temporal formula
467:multiprocessor.
350:mutual exclusion
333:computer science
178:
175:
173:
171:
169:
167:
107:
105:
100:
82:
80:
75:
58:Designed by
40:
33:
21:
5586:
5585:
5581:
5580:
5579:
5577:
5576:
5575:
5536:
5535:
5534:
5529:
5515:
5486:.NET Foundation
5474:
5451:
5424:
5358:
5326:
5307:XDP for Windows
5245:Windows App SDK
5005:Fluid Framework
4985:eBPF on Windows
4852:
4846:
4754:
4748:
4732:
4713:Windows Console
4649:
4628:
4620:
4510:
4505:
4504:
4494:
4492:
4490:Microsoft Azure
4482:(10 May 2017).
4478:
4477:
4473:
4463:
4461:
4452:
4451:
4447:
4440:
4415:
4414:
4410:
4400:
4398:
4384:
4383:
4379:
4372:
4368:
4320:
4319:
4315:
4305:
4303:
4286:
4285:
4281:
4264:
4259:Distributed TLC
4255:
4254:
4250:
4240:
4232:. p. 116.
4218:Lamport, Leslie
4216:
4215:
4211:
4201:
4193:. p. 112.
4179:Lamport, Leslie
4177:
4176:
4172:
4162:
4160:
4150:
4127:
4119:Lamport, Leslie
4116:
4115:
4104:
4094:
4092:
4090:
4063:
4057:Lamport, Leslie
4055:
4054:
4050:
4043:
4023:Lamport, Leslie
4021:
4020:
4016:
4006:
4004:
4002:
3984:Springer-Verlag
3979:
3971:Lamport, Leslie
3968:
3967:
3960:
3950:
3948:
3942:Lamport, Leslie
3940:
3939:
3935:
3925:
3923:
3917:Lamport, Leslie
3915:
3914:
3907:
3897:
3895:
3889:Lamport, Leslie
3887:
3886:
3882:
3872:
3870:
3864:Lamport, Leslie
3862:
3861:
3857:
3847:
3845:
3839:Lamport, Leslie
3837:
3836:
3832:
3825:
3800:
3799:
3795:
3785:
3783:
3748:
3742:Lamport, Leslie
3740:
3739:
3735:
3725:
3703:Lamport, Leslie
3701:
3700:
3696:
3686:
3684:
3674:Lamport, Leslie
3672:
3671:
3667:
3657:
3655:
3648:
3643:
3642:
3635:
3622:
3620:
3601:
3600:
3596:
3586:
3584:
3581:
3575:Lamport, Leslie
3573:
3572:
3565:
3555:
3553:
3551:
3540:
3532:Lamport, Leslie
3530:
3529:
3522:
3517:
3470:
3465:
3464:
3460:
3456:
3452:
3448:
3445:
3441:
3437:
3433:
3429:
3425:
3421:
3417:
3413:
3409:
3405:
3401:
3397:
3393:
3389:
3385:
3381:
3377:
3373:
3369:
3365:
3361:
3357:
3353:
3349:
3345:
3341:
3337:
3333:
3329:
3326:
3322:
3318:
3315:
3311:
3307:
3304:
3300:
3296:
3293:
3289:
3285:
3282:
3278:
3274:
3271:
3267:
3263:
3260:
3256:
3252:
3249:
3245:
3241:
3238:
3234:
3230:
3226:
3222:
3218:
3214:
3210:
3206:
3202:
3198:
3194:
3190:
3186:
3182:
3178:
3174:
3170:
3166:
3165:approaching /=
3162:
3158:
3154:
3150:
3146:
3142:
3138:
3135:
3131:
3127:
3123:
3119:
3115:
3111:
3106:
3102:
3098:
3094:
3090:
3086:
3081:
3077:
3073:
3069:
3065:
3061:
3057:
3053:
3049:
3045:
3041:
3037:
3033:
3029:
3025:
3021:
3017:
3012:
3008:
3004:
3000:
2996:
2992:
2988:
2984:
2980:
2976:
2972:
2968:
2964:
2960:
2956:
2952:
2948:
2944:
2940:
2936:
2932:
2928:
2924:
2920:
2916:
2912:
2908:
2904:
2900:
2896:
2892:
2887:
2883:
2879:
2876:
2873:
2869:
2865:
2861:
2857:
2853:
2849:
2846:
2843:
2839:
2835:
2831:
2827:
2823:
2819:
2816:
2812:
2808:
2804:
2800:
2796:
2792:
2788:
2784:
2780:
2776:
2772:
2768:
2764:
2760:
2756:
2752:
2748:
2744:
2740:
2736:
2732:
2728:
2724:
2720:
2716:
2712:
2708:
2704:
2700:
2696:
2693:
2689:
2685:
2681:
2677:
2673:
2669:
2665:
2661:
2657:
2653:
2649:
2645:
2641:
2637:
2633:
2629:
2625:
2621:
2617:
2613:
2609:
2605:
2601:
2597:
2593:
2589:
2585:
2581:
2577:
2573:
2569:
2565:
2561:
2557:
2553:
2549:
2545:
2541:
2537:
2533:
2529:
2526:
2522:
2518:
2514:
2510:
2506:
2502:
2498:
2494:
2490:
2486:
2482:
2478:
2474:
2463:
2462:
2458:
2454:
2450:
2446:
2442:
2438:
2434:
2430:
2426:
2422:
2418:
2414:
2410:
2406:
2402:
2397:
2393:
2389:
2385:
2384:r <= p /
2381:
2377:
2373:
2369:
2365:
2361:
2357:
2356:r <= a /
2353:
2349:
2345:
2341:
2337:
2333:
2329:
2325:
2321:
2310:
2309:
2305:
2301:
2298:
2294:
2290:
2286:
2283:
2279:
2275:
2272:
2268:
2264:
2260:
2256:
2253:
2249:
2245:
2241:
2237:
2233:
2229:
2226:
2222:
2218:
2214:
2210:
2206:
2202:
2199:
2195:
2191:
2188:
2184:
2180:
2176:
2172:
2168:
2164:
2160:
2156:
2152:
2148:
2145:
2141:
2137:
2133:
2129:
2126:
2122:
2118:
2114:
2110:
2106:
2102:
2098:
2094:
2090:
2086:
2082:
2078:
2074:
2071:
2067:
2063:
2059:
2055:
2051:
2047:
2043:
2040:
2036:
2032:
2028:
2024:
2020:
2016:
2012:
2008:
2004:
2001:
1997:
1993:
1989:
1985:
1982:
1978:
1974:
1970:
1966:
1962:
1958:
1954:
1951:
1947:
1943:
1939:
1935:
1931:
1927:
1923:
1919:
1915:
1911:
1908:
1904:
1900:
1896:
1892:
1888:
1884:
1880:
1876:
1872:
1868:
1864:
1860:
1856:
1852:
1848:
1844:
1840:
1836:
1832:
1828:
1824:
1820:
1816:
1812:
1808:
1804:
1800:
1796:
1792:
1788:
1784:
1780:
1776:
1772:
1768:
1764:
1760:
1756:
1752:
1748:
1744:
1741:
1737:
1733:
1729:
1725:
1721:
1717:
1713:
1709:
1705:
1701:
1697:
1693:
1689:
1685:
1681:
1670:key-value store
1666:
1640:Microsoft Azure
1612:Byzantine Paxos
1600:
1584:Byzantine Paxos
1543:
1494:
1486:The TLA Toolbox
1412:
1352:
1338:
1333:
1331:
1328:
1322:Preview release
1316:
1311:
1309:
1306:
1286:
1284:
1281:
1277:Initial release
1267:Hewlett-Packard
1246:
1231:
1226:
1217:
1213:
1202:specifications.
1166:Natural numbers
1093:
1084:
1076:
1072:
1068:
1064:
1055:
1051:
1047:
1044:
1034:
1030:
1023:
1019:
1016:
1012:
993:
983:
967:
955:
952:
950:Data structures
940:not a valid set
907:
891:
860:
859:
830:
829:
803:
802:
776:
775:
769:natural numbers
755:
749:
745:
733:
729:
725:
721:
717:
713:
678:
655:
654:
634:
633:
626:
618:
617:
588:is 0, and 0 if
570:
569:
562:
541:State predicate
523:Stuttering step
489:
463:protocol for a
461:cache coherence
401:Edsger Dijkstra
302:
164:
108:
103:
101:
98:
78:
76:
73:
28:
23:
22:
15:
12:
11:
5:
5584:
5582:
5574:
5573:
5568:
5563:
5558:
5553:
5548:
5546:Formal methods
5538:
5537:
5531:
5530:
5520:
5517:
5516:
5514:
5513:
5508:
5503:
5498:
5493:
5488:
5482:
5480:
5476:
5475:
5473:
5472:
5467:
5461:
5459:
5453:
5452:
5450:
5449:
5444:
5438:
5436:
5430:
5429:
5426:
5425:
5423:
5422:
5417:
5412:
5407:
5402:
5397:
5392:
5387:
5382:
5377:
5372:
5366:
5364:
5360:
5359:
5357:
5356:
5351:
5346:
5341:
5334:
5332:
5328:
5327:
5325:
5324:
5319:
5314:
5309:
5304:
5299:
5294:
5289:
5284:
5279:
5274:
5269:
5268:
5267:
5262:
5252:
5247:
5242:
5237:
5232:
5227:
5222:
5217:
5212:
5207:
5202:
5197:
5192:
5187:
5182:
5177:
5172:
5167:
5162:
5157:
5152:
5147:
5142:
5137:
5132:
5127:
5122:
5117:
5112:
5107:
5102:
5097:
5092:
5087:
5082:
5077:
5072:
5067:
5062:
5057:
5055:Microsoft SEAL
5052:
5047:
5042:
5037:
5032:
5027:
5022:
5017:
5012:
5007:
5002:
4997:
4992:
4987:
4982:
4977:
4972:
4967:
4962:
4957:
4952:
4947:
4942:
4937:
4932:
4927:
4922:
4917:
4912:
4907:
4902:
4897:
4892:
4887:
4882:
4877:
4872:
4870:.NET Gadgeteer
4867:
4865:.NET Framework
4862:
4856:
4854:
4848:
4847:
4845:
4844:
4839:
4834:
4829:
4824:
4822:Project Verona
4819:
4814:
4809:
4804:
4799:
4794:
4789:
4784:
4779:
4774:
4769:
4764:
4758:
4756:
4750:
4749:
4747:
4746:
4740:
4738:
4734:
4733:
4731:
4730:
4725:
4720:
4715:
4710:
4705:
4700:
4695:
4690:
4685:
4680:
4675:
4670:
4668:3D Movie Maker
4664:
4662:
4655:
4651:
4650:
4648:
4647:
4642:
4636:
4634:
4630:
4629:
4621:
4619:
4618:
4611:
4604:
4596:
4590:
4589:
4584:
4571:
4561:
4551:
4550:faculty summit
4541:
4532:
4523:
4517:
4509:
4508:External links
4506:
4503:
4502:
4480:Leslie Lamport
4471:
4445:
4438:
4408:
4386:Leslie Lamport
4377:
4366:
4313:
4279:
4248:
4238:
4230:Addison-Wesley
4209:
4199:
4191:Addison-Wesley
4170:
4148:
4102:
4088:
4048:
4041:
4033:Addison-Wesley
4014:
4000:
3958:
3933:
3905:
3880:
3855:
3830:
3823:
3793:
3733:
3723:
3717:. p. 75.
3715:Addison-Wesley
3694:
3665:
3633:
3619:. 8 April 2013
3594:
3563:
3549:
3519:
3518:
3516:
3513:
3512:
3511:
3506:
3501:
3499:Temporal logic
3496:
3491:
3486:
3481:
3476:
3469:
3466:
3229:ElevatorState
2967:gettingOff /=
2608:ElevatorState
2472:
2319:
1981:snapshotStore
1795:snapshotStore
1679:
1665:
1662:
1599:
1596:
1542:
1539:
1493:
1490:
1482:
1481:
1478:
1475:
1472:
1469:pretty-printed
1461:
1436:
1435:
1410:
1406:
1405:
1400:
1394:
1393:
1388:
1382:
1381:
1378:
1374:
1373:
1368:
1364:
1363:
1350:
1344:
1343:
1340:
1339:
1326:
1324:
1318:
1317:
1304:
1302:
1300:Stable release
1296:
1295:
1292:
1291:
1278:
1274:
1273:
1264:
1258:
1257:
1254:
1248:
1247:
1244:
1230:
1227:
1225:
1222:
1210:
1209:
1203:
1193:
1184:: Defines the
1179:
1174:: Defines the
1169:
1164:: Defines the
1159:
1149:
1115:
1112:Cardinality(S)
1108:IsFiniteSet(S)
1092:
1089:
1074:
1070:
1066:
1032:
951:
948:
932:set membership
905:
889:
873:
870:
867:
843:
840:
837:
813:
810:
786:
783:
677:
674:
667:machine-closed
652:
631:
625:
622:
615:
567:
561:
558:
557:
556:
550:
544:
538:
535:State function
532:
526:
520:
514:
508:
488:
485:
427:Leslie Lamport
365:Leslie Lamport
321:temporal logic
301:
298:
259:temporal logic
239:model checking
193:Leslie Lamport
180:
179:
168:.azurewebsites
162:
158:
157:
154:
148:
147:
142:
136:
135:
130:
124:
123:
118:
114:
113:
110:
109:
96:
94:
92:Stable release
88:
87:
84:
83:
70:
66:
65:
63:Leslie Lamport
60:
54:
53:
48:
42:
41:
26:
24:
14:
13:
10:
9:
6:
4:
3:
2:
5583:
5572:
5569:
5567:
5564:
5562:
5559:
5557:
5554:
5552:
5549:
5547:
5544:
5543:
5541:
5528:
5518:
5512:
5509:
5507:
5504:
5502:
5499:
5497:
5494:
5492:
5489:
5487:
5484:
5483:
5481:
5477:
5471:
5468:
5466:
5463:
5462:
5460:
5458:
5454:
5448:
5445:
5443:
5440:
5439:
5437:
5435:
5431:
5421:
5418:
5416:
5413:
5411:
5408:
5406:
5403:
5401:
5398:
5396:
5393:
5391:
5388:
5386:
5383:
5381:
5378:
5376:
5373:
5371:
5368:
5367:
5365:
5361:
5355:
5352:
5350:
5347:
5345:
5342:
5339:
5336:
5335:
5333:
5329:
5323:
5320:
5318:
5315:
5313:
5310:
5308:
5305:
5303:
5300:
5298:
5295:
5293:
5290:
5288:
5285:
5283:
5280:
5278:
5275:
5273:
5272:Windows Forms
5270:
5266:
5263:
5261:
5258:
5257:
5256:
5253:
5251:
5248:
5246:
5243:
5241:
5240:Vowpal Wabbit
5238:
5236:
5233:
5231:
5228:
5226:
5223:
5221:
5218:
5216:
5213:
5211:
5208:
5206:
5203:
5201:
5198:
5196:
5193:
5191:
5188:
5186:
5183:
5181:
5178:
5176:
5173:
5171:
5168:
5166:
5163:
5161:
5158:
5156:
5153:
5151:
5148:
5146:
5143:
5141:
5138:
5136:
5133:
5131:
5128:
5126:
5123:
5121:
5118:
5116:
5113:
5111:
5108:
5106:
5103:
5101:
5098:
5096:
5093:
5091:
5088:
5086:
5083:
5081:
5078:
5076:
5073:
5071:
5068:
5066:
5063:
5061:
5058:
5056:
5053:
5051:
5048:
5046:
5043:
5041:
5038:
5036:
5033:
5031:
5028:
5026:
5023:
5021:
5018:
5016:
5013:
5011:
5008:
5006:
5003:
5001:
4998:
4996:
4993:
4991:
4988:
4986:
4983:
4981:
4978:
4976:
4973:
4971:
4968:
4966:
4963:
4961:
4958:
4956:
4953:
4951:
4948:
4946:
4943:
4941:
4938:
4936:
4933:
4931:
4928:
4926:
4923:
4921:
4918:
4916:
4913:
4911:
4910:ASP.NET Razor
4908:
4906:
4903:
4901:
4898:
4896:
4893:
4891:
4888:
4886:
4883:
4881:
4878:
4876:
4873:
4871:
4868:
4866:
4863:
4861:
4858:
4857:
4855:
4849:
4843:
4840:
4838:
4835:
4833:
4830:
4828:
4825:
4823:
4820:
4818:
4815:
4813:
4810:
4808:
4805:
4803:
4800:
4798:
4795:
4793:
4790:
4788:
4785:
4783:
4780:
4778:
4775:
4773:
4770:
4768:
4765:
4763:
4760:
4759:
4757:
4751:
4745:
4742:
4741:
4739:
4735:
4729:
4726:
4724:
4721:
4719:
4716:
4714:
4711:
4709:
4706:
4704:
4701:
4699:
4696:
4694:
4691:
4689:
4686:
4684:
4681:
4679:
4678:Conference XP
4676:
4674:
4671:
4669:
4666:
4665:
4663:
4659:
4656:
4652:
4646:
4643:
4641:
4638:
4637:
4635:
4631:
4627:
4624:
4617:
4612:
4610:
4605:
4603:
4598:
4597:
4594:
4588:
4585:
4583:
4579:
4575:
4572:
4569:
4565:
4562:
4559:
4555:
4552:
4549:
4545:
4542:
4540:
4536:
4533:
4531:
4527:
4524:
4521:
4518:
4515:
4512:
4511:
4507:
4491:
4487:
4486:
4481:
4475:
4472:
4460:
4456:
4449:
4446:
4441:
4435:
4431:
4427:
4423:
4419:
4412:
4409:
4397:
4393:
4392:
4387:
4381:
4378:
4375:
4370:
4367:
4362:
4358:
4353:
4348:
4344:
4340:
4336:
4332:
4328:
4324:
4317:
4314:
4301:
4297:
4293:
4289:
4283:
4280:
4275:
4269:
4268:cite AV media
4261:
4260:
4252:
4249:
4245:
4241:
4235:
4231:
4227:
4223:
4219:
4213:
4210:
4206:
4202:
4196:
4192:
4188:
4184:
4180:
4174:
4171:
4159:
4155:
4151:
4145:
4141:
4137:
4133:
4126:
4125:
4120:
4113:
4111:
4109:
4107:
4103:
4091:
4085:
4081:
4077:
4073:
4069:
4062:
4058:
4052:
4049:
4044:
4038:
4034:
4030:
4029:
4024:
4018:
4015:
4003:
3997:
3993:
3989:
3985:
3978:
3977:
3972:
3965:
3963:
3959:
3947:
3943:
3937:
3934:
3922:
3918:
3912:
3910:
3906:
3894:
3890:
3884:
3881:
3869:
3865:
3859:
3856:
3844:
3840:
3834:
3831:
3826:
3820:
3816:
3812:
3808:
3804:
3797:
3794:
3782:
3778:
3774:
3770:
3766:
3762:
3758:
3754:
3747:
3743:
3737:
3734:
3730:
3726:
3720:
3716:
3712:
3708:
3704:
3698:
3695:
3683:
3679:
3675:
3669:
3666:
3654:
3647:
3640:
3638:
3634:
3631:
3618:
3614:
3610:
3609:
3604:
3598:
3595:
3580:
3576:
3570:
3568:
3564:
3552:
3546:
3539:
3538:
3533:
3527:
3525:
3521:
3514:
3510:
3507:
3505:
3502:
3500:
3497:
3495:
3492:
3490:
3487:
3485:
3482:
3480:
3477:
3475:
3472:
3471:
3467:
3028:eState.floor
2915:gettingOn /=
2860:eState.floor
2470:
2468:
2441:rule.protocol
2317:
2315:
2312:A rule-based
2167:written ELSE
2144:tx' = tx
2070:tx' = tx
1907:tx' = tx
1823:tx :
1677:
1675:
1671:
1663:
1661:
1659:
1656:
1651:
1649:
1645:
1641:
1637:
1635:
1631:
1627:
1623:
1619:
1617:
1613:
1609:
1605:
1597:
1595:
1593:
1589:
1585:
1579:
1577:
1573:
1569:
1565:
1561:
1556:
1552:
1548:
1540:
1538:
1536:
1530:
1528:
1524:
1519:
1515:
1511:
1507:
1506:model checker
1498:
1492:Model checker
1491:
1489:
1487:
1479:
1476:
1473:
1470:
1466:
1462:
1459:
1458:
1457:
1455:
1451:
1447:
1443:
1433:
1411:
1407:
1404:
1401:
1399:
1395:
1392:
1389:
1387:
1383:
1379:
1375:
1372:
1369:
1365:
1361:
1351:
1349:
1345:
1341:
1325:
1323:
1319:
1303:
1301:
1297:
1293:
1279:
1275:
1272:
1268:
1265:
1263:
1259:
1255:
1253:
1249:
1242:
1237:
1228:
1223:
1221:
1207:
1204:
1201:
1197:
1194:
1191:
1187:
1183:
1180:
1177:
1173:
1170:
1167:
1163:
1160:
1157:
1153:
1150:
1147:
1143:
1142:concatenation
1139:
1135:
1131:
1127:
1123:
1119:
1116:
1113:
1109:
1105:
1101:
1098:
1097:
1096:
1090:
1088:
1082:
1062:
1058:
1042:
1038:
1028:
1013:Double == x*2
1010:
1006:
1002:
998:
991:
987:
981:
978:. The unique
977:
973:
965:
961:
949:
947:
945:
941:
937:
933:
929:
924:
921:
919:
915:
911:
903:
899:
895:
887:
871:
868:
865:
857:
841:
838:
835:
827:
811:
808:
800:
784:
781:
772:
770:
766:
762:
758:
743:
739:
711:
707:
703:
699:
695:
691:
687:
683:
675:
673:
670:
668:
664:
660:
650:
648:
644:
640:
629:
623:
621:
613:
611:
607:
603:
599:
595:
591:
587:
583:
579:
575:
565:
559:
554:
551:
548:
545:
542:
539:
536:
533:
530:
527:
524:
521:
518:
515:
512:
509:
506:
503:
502:
501:
499:
495:
486:
484:
482:
478:
473:
468:
466:
462:
458:
457:model checker
452:
450:
446:
439:
437:
428:
423:
419:
417:
413:
410:organized by
409:
404:
402:
398:
394:
390:
386:
382:
378:
374:
370:
366:
362:
357:
355:
351:
347:
341:
336:
334:
330:
326:
322:
314:
310:
306:
299:
297:
295:
291:
287:
283:
278:
276:
271:
267:
262:
260:
256:
252:
248:
244:
240:
235:
233:
229:
224:
222:
218:
214:
210:
206:
202:
198:
194:
190:
186:
177:
163:
159:
155:
153:
149:
146:
143:
141:
137:
134:
131:
129:
125:
122:
119:
115:
111:
95:
93:
89:
85:
71:
67:
64:
61:
59:
55:
52:
49:
47:
43:
39:
34:
19:
5210:TLA+ Toolbox
5135:Open XML SDK
4955:CLR Profiler
4900:ASP.NET Core
4895:ASP.NET AJAX
4842:Visual Basic
4688:File Manager
4661:Applications
4582:Manfred Broy
4493:. Retrieved
4484:
4474:
4462:. Retrieved
4448:
4417:
4411:
4399:. Retrieved
4390:
4380:
4369:
4330:
4326:
4316:
4304:. Retrieved
4302:Joint Centre
4291:
4282:
4258:
4251:
4243:
4225:
4212:
4204:
4186:
4173:
4161:. Retrieved
4123:
4093:. Retrieved
4067:
4051:
4027:
4017:
4005:. Retrieved
3975:
3949:. Retrieved
3936:
3924:. Retrieved
3896:. Retrieved
3883:
3871:. Retrieved
3858:
3846:. Retrieved
3833:
3802:
3796:
3784:. Retrieved
3756:
3752:
3736:
3728:
3710:
3697:
3685:. Retrieved
3681:
3668:
3656:. Retrieved
3621:. Retrieved
3606:
3597:
3585:. Retrieved
3554:. Retrieved
3536:
3213:PersonState
2592:PersonState
2465:A multi-car
2464:
2311:
1851:missed /
1667:
1652:
1638:
1620:
1601:
1598:Industry use
1580:
1544:
1541:Proof system
1531:
1527:parallelizes
1510:finite state
1503:
1483:
1439:
1377:Available in
1262:Developer(s)
1220:statements.
1211:
1205:
1195:
1186:Real numbers
1181:
1171:
1161:
1151:
1138:Append(S, E)
1137:
1133:
1129:
1125:
1117:
1111:
1107:
1099:
1094:
1059:
1039:
1026:
1008:
1000:
996:
988:
975:
971:
963:
959:
953:
925:
922:
917:
913:
909:
902:continuously
901:
897:
893:
885:
855:
825:
798:
773:
744:quantifiers
694:intersection
679:
671:
666:
662:
658:
656:
646:
635:
627:
619:
609:
605:
601:
597:
593:
589:
585:
581:
577:
573:
571:
563:
552:
546:
540:
534:
528:
522:
516:
510:
504:
490:
469:
453:
441:
433:
412:Susan Owicki
405:
358:
343:
338:
325:Arthur Prior
318:
313:Turing Award
279:
263:
236:
225:
212:
184:
183:
18:TLA+ Toolbox
5354:Azure Linux
5085:MonoDevelop
4905:ASP.NET MVC
4851:Frameworks,
4753:Programming
4737:Video games
4728:XML Notepad
4683:Family.Show
4578:festschrift
4327:IEEE Access
3189:stationary
3177:stationary
3161:stationary
3101:Floor /
3072:Floor /
2763:Floor /
2449:matches /=
2437:p.protocol
2244:Key :
2217:Key :
1783:Store /
1658:OpenComRTOS
1655:model check
1592:BSD license
1403:MIT License
1234:TLA Toolbox
1106:. Provides
1104:finite sets
1020:Double \in
999:, for each
918:continually
916:is enabled
900:is enabled
742:existential
708:operators.
393:termination
369:peer review
361:Hoare logic
329:Amir Pnueli
309:Amir Pnueli
145:MIT License
5540:Categories
5420:WikiBhasha
5395:Project Mu
5370:ChronoZoom
5344:Barrelfish
5180:Sandcastle
5145:Playwright
4950:ChakraCore
4925:Babylon.js
4837:TypeScript
4817:PowerShell
4792:IronPython
4744:Allegiance
4539:Build 2014
4459:TechCrunch
3515:References
3509:Z notation
3451:Vars /
3444:Init /
3233:] Next ==
3097:nextFloor
3068:nextFloor
2263:tx :
2236:tx :
2209:tx :
2183:] Next ==
2125:written =
1879:written =
1863:tx :
1791:TxId /
1525:. It also
1416:.microsoft
1367:Written in
1348:Repository
1334:2020-12-06
1312:2022-02-02
1287:2010-02-04
1114:operators.
1100:FiniteSets
1085:Nat \X Nat
754:Hilbert's
698:difference
686:membership
639:refinement
436:FIFO queue
373:invariance
290:transpiles
270:algorithms
255:set theory
243:invariance
205:pseudocode
104:2014-01-15
79:1999-04-23
5400:ReactiveX
5317:xUnit.net
5230:Voldemort
5195:SVNBridge
5010:Infer.NET
4965:DeepSpeed
4940:C++/WinRT
4930:BitFunnel
4875:.NET MAUI
4755:languages
4623:Microsoft
4396:Microsoft
4361:236480167
3781:121557270
3773:1661-7738
3759:: 43–63.
3613:Microsoft
2899:gettingOn
2602:\subseteq
1887:missed =
1789:\subseteq
1644:Cosmos DB
1604:Microsoft
1535:available
1508:builds a
1452:, plus a
1271:Microsoft
1156:multisets
1118:Sequences
1065:<<e
990:Functions
980:empty set
869:◻
866:◊
839:◊
836:◻
809:◊
782:◻
738:universal
676:Operators
547:Invariant
511:Behaviour
477:available
340:computer.
268:both for
5527:Category
5465:CodePlex
5434:Licenses
5380:FlexWiki
5190:StyleCop
5150:ProcDump
5075:mod_mono
5060:mimalloc
5015:LightGBM
4990:Electron
4920:Avalonia
4812:Power Fx
4797:IronRuby
4787:GW-BASIC
4703:Terminal
4654:Software
4633:Overview
4568:Stanford
3744:(2012).
3608:CodePlex
3484:B-Method
3468:See also
3149:IN /
2959:IN /
2903:IN /
2469:system:
2467:elevator
2344:Address
2314:firewall
2117:tx /
2066:tx /
2027:tx /
1988:NoVal, v
1977:tx /
1938:tx /
1903:tx /
1803:written
1664:Examples
1626:DynamoDB
1608:Xbox 360
1566:solvers
1560:Isabelle
1504:The TLC
1430:/toolbox
1426:/lamport
1414:research
1360:/tlaplus
1358:/tlaplus
1218:INSTANCE
1196:RealTime
1190:infinity
1176:Integers
1172:Integers
1162:Naturals
1124:such as
1077:>>
854:to mean
824:to mean
797:to mean
765:integers
702:powerset
643:fairness
624:Liveness
487:Language
475:work is
408:Stanford
385:liveness
354:deadlock
251:liveness
46:Paradigm
5479:Related
5297:WinObjC
5215:U-Prove
5185:SignalR
5155:ProcMon
5140:Orleans
5115:OneFuzz
5090:MSBuild
4970:DiskSpd
4890:ASP.NET
4339:Bibcode
4158:5243433
3494:PlusCal
3217:] /
2596:] /
2171:] /
2121:missed
2101:] /
2093:] /
2050:] /
2011:] /
1961:] /
1811:missed
1446:Eclipse
1424:/people
1409:Website
1398:License
1380:English
1332: (
1310: (
1285: (
1214:EXTENDS
1134:Tail(S)
1130:Head(S)
1041:Records
1003:in the
750:∃
746:∀
718:∧
714:∨
472:PlusCal
449:actions
319:Modern
300:History
286:PlusCal
217:acronym
166:lamport
161:Website
140:License
102: (
77: (
5470:GitHub
5457:Forges
5390:Gollum
5338:MS-DOS
5175:Roslyn
5095:MsQuic
5070:ML.NET
4935:Blazor
4885:AirSim
4762:Bosque
4495:10 May
4464:10 May
4436:
4401:14 May
4359:
4306:14 May
4236:
4197:
4163:14 May
4156:
4146:
4095:10 May
4086:
4039:
4007:14 May
3998:
3951:22 May
3926:22 May
3898:22 May
3873:22 May
3848:22 May
3821:
3786:23 May
3779:
3771:
3721:
3653:Amazon
3623:10 May
3617:Compaq
3556:22 May
3547:
3099:\notin
3030:\notin
1983:\notin
1901:\notin
1845:\notin
1779:store
1718:\notin
1574:, and
1471:specs.
1420:/en-us
1354:github
1146:filter
1144:, and
1126:Len(S)
1122:tuples
1061:Tuples
1048:r.name
1005:domain
970:where
958:where
928:macros
767:, and
756:ε
722:¬
706:subset
704:, and
560:Safety
465:Compaq
381:safety
247:safety
215:is an
51:Action
5410:TLAPS
5385:FourQ
5363:Other
5349:SONiC
5292:WinJS
5220:vcpkg
5110:NuGet
4975:Dryad
4772:Dafny
4558:React
4357:S2CID
4300:INRIA
4154:S2CID
4128:(PDF)
4064:(PDF)
3980:(PDF)
3777:S2CID
3749:(PDF)
3687:7 May
3682:Wired
3658:8 May
3649:(PDF)
3587:2 May
3582:(PDF)
3541:(PDF)
3036:call
2852:call
2457:rule
2445:IN /
2413:rule
2372:Port
1859:TxId
1829:&
1740:tx =
1672:with
1572:Yices
1555:INRIA
1465:LaTeX
1432:.html
1224:Tools
1182:Reals
1052:r.age
966:, or
761:reals
690:union
598:clock
590:clock
586:clock
582:clock
578:clock
576:sets
505:State
498:ASCII
494:LaTeX
377:Floyd
275:LaTeX
232:logic
187:is a
176:.html
5405:SILK
5265:UMDF
5260:KMDF
5235:VoTT
5080:Mono
4960:Dapr
4860:.NET
4802:Lean
4673:Atom
4580:for
4497:2017
4466:2017
4434:ISBN
4403:2015
4335:IEEE
4308:2015
4274:link
4234:ISBN
4195:ISBN
4165:2015
4144:ISBN
4097:2015
4084:ISBN
4037:ISBN
4009:2015
3996:ISBN
3953:2015
3928:2015
3900:2015
3875:2015
3850:2015
3819:ISBN
3788:2015
3769:ISSN
3719:ISBN
3689:2015
3660:2015
3625:2015
3589:2015
3558:2015
3545:ISBN
3426:\ \A
3414:\ \A
3402:\ \A
3390:\ \A
3378:\ \A
3366:\ \A
3354:\ \A
3342:\ \A
3191:\cup
3183:\ \A
3179:\cup
3163:\cup
3050:\ \E
3034:\ \A
2822:call
2817:\cup
2765:\ \E
2733:\ \A
2705:\ \A
2686:\ \A
2666:\ \A
2654:\ \A
2638:\ \E
2630:\ \A
2618:\ \A
2527:\cup
2455:\ \A
2165:\cup
2123:\cap
2041:\cup
2002:\cup
1952:\cup
1909:\cup
1869:\ \A
1853:\ \A
1817:\ \A
1568:CVC3
1463:The
1428:/tla
1418:.com
1386:Type
1371:Java
1356:.com
1152:Bags
1110:and
1050:and
1007:set
748:and
740:and
663:Tick
659:Tick
647:Tick
610:Tick
606:Init
602:Spec
594:Init
574:Tick
517:Step
391:and
383:and
249:and
219:for
199:and
174:/tla
172:/tla
170:.net
156:.tla
121:Java
5312:XSP
5302:WiX
5105:npm
4945:CCF
4426:doi
4347:doi
4136:doi
4076:doi
3988:doi
3811:doi
3761:doi
3430:\in
3418:\in
3406:\in
3394:\in
3382:\in
3370:\in
3358:\in
3346:\in
3334:\in
3323:\in
3312:\in
3301:\in
3290:\in
3279:\in
3268:\in
3257:\in
3246:\in
3231:\in
3215:\in
3199:\in
3187:\in
3185:e2
3175:\in
3155:\in
3128:\in
3116:\in
3070:\in
3054:\in
3052:e2
3038:\in
2981:\in
2977:\in
2949:\in
2929:\in
2925:\in
2897:\in
2862:\in
2854:\in
2805:\in
2769:\in
2761:\in
2737:\in
2729:\in
2721:\in
2709:\in
2690:\in
2670:\in
2658:\in
2642:\in
2634:\in
2622:\in
2610:\in
2594:\in
2566:\in
2459:\in
2439:\in
2415:\in
2370:\in
2342:\in
2291:\in
2280:\in
2269:\in
2261:\in
2250:\in
2242:\in
2234:\in
2223:\in
2215:\in
2207:\in
2196:\in
2115:\in
2064:\in
2025:\in
1975:\in
1936:\in
1873:\in
1857:\in
1849:\in
1837:\in
1821:\in
1813:\in
1805:\in
1797:\in
1787:tx
1781:\in
1634:EBS
1602:At
1564:SMT
1454:GUI
1440:An
1422:/um
1229:IDE
1216:or
1206:TLC
1031:= v
1018:so
416:SRI
282:IDE
213:TLA
185:TLA
31:TLA
5542::
4827:Q#
4782:F*
4777:F#
4767:C#
4457:.
4432:.
4355:.
4345:.
4333:.
4329:.
4325:.
4298:-
4294:.
4290:.
4270:}}
4266:{{
4242:.
4228:.
4224:.
4203:.
4189:.
4185:.
4152:.
4142:.
4105:^
4082:.
4066:.
4035:.
4031:.
3994:.
3961:^
3944:.
3919:.
3908:^
3891:.
3866:.
3841:.
3817:.
3775:.
3767:.
3757:11
3755:.
3751:.
3727:.
3713:.
3709:.
3680:.
3651:.
3636:^
3615:,
3611:.
3605:.
3566:^
3523:^
3461:\
3457:\
3453:\
3446:\
3442:\
3438:\*
3428:c
3416:e
3404:e
3392:e
3380:e
3368:e
3356:e
3344:p
3338:\*
3332:c
3330:\E
3327:\/
3321:e
3319:\E
3316:\/
3310:e
3308:\E
3305:\/
3299:e
3297:\E
3294:\/
3288:e
3286:\E
3283:\/
3277:e
3275:\E
3272:\/
3266:e
3264:\E
3261:\/
3255:p
3253:\E
3250:\/
3244:p
3242:\E
3239:\/
3235:\*
3227:\
3223:{}
3219:\
3211:\
3207:\*
3203:\
3195:\
3171:\
3167:{}
3159:\
3153:c
3151:\
3143:\/
3139:\/
3136:\
3132:\
3126:e
3114:e
3107:\
3103:\
3095:\
3091:\
3087:\
3082:\*
3078:\
3074:\
3066:\
3062:\
3058:\
3046:\
3042:\*
3026:\
3022:\
3018:\
3013:\*
3009:\
3005:\
3001:\
2997:\
2993:\
2989:\*
2985:\
2973:\
2969:{}
2965:\
2961:\
2953:\
2947:p
2941:\*
2937:\
2933:\
2921:\
2917:{}
2913:\
2909:\
2905:\
2888:\*
2884:\
2874:\
2870:\
2866:\
2858:\/
2850:\E
2847:\/
2844:\
2840:\
2836:\*
2832:\
2828:\
2813:\
2809:\
2803:e
2801:\E
2797:\
2793:\
2789:\
2785:\*
2781:\
2777:\
2773:\
2767:f
2757:\
2753:\
2749:\*
2745:\
2741:\*
2735:p
2727:e
2725:\E
2719:c
2717:\
2713:\*
2707:c
2701:\*
2697:\*
2694:{}
2688:c
2682:\
2678:\
2674:\
2668:e
2662:\*
2656:p
2650:\
2646:\
2640:p
2632:f
2626:\*
2620:e
2614:\*
2606:\
2598:\
2590:\
2586:\*
2578:\
2574:\
2570:\
2564:p
2558:\*
2554:\
2550:\
2546:\*
2542:\*
2538:\*
2523:\*
2519:\*
2507:\*
2503:\*
2499:\*
2495:\*
2491:\*
2487:\*
2483:\*
2479:\*
2475:\*
2451:{}
2447:\
2435:\
2431:\
2427:\
2423:\
2419:\
2407:\*
2403:\*
2398:\*
2394:\*
2390:\*
2386:\
2382:\
2374:\X
2368:r
2362:\*
2358:\
2354:\
2346:\X
2340:r
2334:\*
2330:\*
2326:\*
2322:\*
2316::
2306:\
2299:\
2295:\*
2289:t
2287:\E
2284:\/
2278:t
2276:\E
2273:\/
2267:k
2265:\E
2259:t
2257:\E
2254:\/
2248:v
2246:\E
2240:k
2238:\E
2232:t
2230:\E
2227:\/
2221:v
2219:\E
2213:k
2211:\E
2205:t
2203:\E
2200:\/
2194:t
2192:\E
2189:\/
2185:\*
2181:{}
2177:\
2173:\
2169:{}
2161:\*
2157:\
2146:\
2142:\
2138:\*
2134:\
2130:\*
2127:{}
2119:\
2113:t
2111:\
2107:\*
2103:\
2099:{}
2095:\
2091:{}
2087:\
2083:\
2072:\
2068:\
2062:t
2060:\
2056:\*
2052:\
2037:\
2033:\
2029:\
2023:t
2021:\
2017:\*
2013:\
1998:\
1994:\
1979:\
1973:t
1971:\
1967:\*
1963:\
1948:\
1944:\
1940:\
1934:t
1932:\
1928:\*
1924:\
1920:\
1905:\
1899:t
1897:\
1893:\*
1889:{}
1885:\
1881:{}
1877:\
1871:k
1865:\*
1861:\
1855:t
1843:k
1841:\
1835:k
1833:\A
1825:\*
1819:t
1809:\
1801:\
1793:\
1785:\
1777:\
1773:\*
1769:\*
1765:\
1761:\*
1757:\
1753:\*
1749:\
1745:\*
1742:{}
1738:\
1734:\*
1730:\
1726:\*
1722:\*
1714:\*
1710:\*
1706:\*
1702:\*
1698:\*
1694:\*
1690:\*
1686:\*
1682:\*
1676::
1668:A
1660:.
1650:.
1632:,
1630:S3
1628:,
1618:.
1576:Z3
1570:,
1488:.
1269:,
1140:,
1136:,
1132:,
1128:,
1087:.
1073:,e
1069:,e
1057:.
1037:.
986:.
984:{}
763:,
752:.
732:,
728:,
724:,
720:,
716:,
700:,
696:,
692:,
688:,
682:ZF
649::
403:.
356:.
223:.
128:OS
4807:P
4615:e
4608:t
4601:v
4499:.
4468:.
4442:.
4428::
4405:.
4363:.
4349::
4341::
4331:9
4310:.
4276:)
4167:.
4138::
4099:.
4078::
4045:.
4011:.
3990::
3955:.
3930:.
3902:.
3877:.
3852:.
3827:.
3813::
3790:.
3763::
3691:.
3662:.
3627:.
3591:.
3560:.
3449:_
3434:_
3422:_
3410:_
3398:_
3386:_
3374:_
3362:_
3350:_
3225:/
3169:/
3147:}
3124:{
3120:}
3112:{
3085:/
3016:/
2971:/
2957:}
2945:{
2919:/
2901:}
2893:{
2882:/
2880:}
2877:{
2826:/
2824:}
2820:{
2582:}
2562:{
2534:}
2530:{
2515:}
2511:{
2453:/
2443:}
2411:{
2378:}
2366:{
2350:}
2338:{
2302:_
2155:/
2153:}
2151:t
2149:{
2081:/
2079:}
2077:t
2075:{
2048:}
2046:k
2044:{
2009:}
2007:k
2005:{
1992:/
1990:}
1986:{
1959:}
1957:k
1955:{
1918:/
1916:}
1914:t
1912:{
1883:/
1807:/
1799:/
1553:-
1336:)
1314:)
1289:)
1192:.
1178:.
1148:.
1075:3
1071:2
1067:1
1035:]
1033:2
1027:e
1009:S
1001:x
997:T
976:x
972:e
964:x
960:p
914:A
910:A
908:(
906:e
898:A
894:A
892:(
890:e
886:P
872:P
856:P
842:P
826:P
812:P
799:P
785:P
734:≡
730:↔
726:⇒
429:.
315:.
106:)
81:)
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
