TLA+のソースを表示
←
TLA+
ナビゲーションに移動
検索に移動
あなたには「このページの編集」を行う権限がありません。理由は以下の通りです:
この操作は、次のグループに属する利用者のみが実行できます:
登録利用者
。
このページのソースの閲覧やコピーができます。
{{DISPLAYTITLE:TLA<sup>+</sup>}} {{Infobox プログラミング言語 | 名前 = TLA<sup>+</sup> | ロゴ = | 拡張子 = .tla | ウェブサイト ={{URL|research.microsoft.com/en-us/um/people/lamport/tla/tla.html}} | ライセンス=[[MIT License]]<ref name="toolboxlicense"> {{cite web | title = Tlaplus Tools - License | website = [[CodePlex]] | publisher = [[Microsoft]], [[Compaq]] | date = 8 April 2013 | url = https://tlaplus.codeplex.com/license | access-date = 10 May 2015}} </ref> |プラットフォーム=[[Cross-platform|Cross-platform (multi-platform)]] |最新リリース日={{Start date and age|2014|01|15}}<ref name="tla2guide"> {{cite web | url = http://research.microsoft.com/en-us/um/people/lamport/tla/tla2-guide.pdf | title = TLA<sup>+2</sup>: A Preliminary Guide | last = Lamport | first = Leslie | author-link = Leslie Lamport | date = 15 January 2014 | access-date = 2 May 2015}} </ref> | 最新リリース=TLA<sup>+2</sup> | プログラミング言語=[[Java]] | 設計者=[[Leslie Lamport]] | 登場時期={{Start date and age|1999|04|23}} <ref name="tlaplus-original"> {{cite book | last = Lamport | first = Leslie | author-link = Leslie Lamport | date = January 2000 | title = Specifying Concurrent Systems with TLA<sup>+</sup> | publisher = IOS Press, Amsterdam | journal = NATO Science Series, III: Computer and Systems Sciences | volume = 173 | issue = Calculational System Design | pages = 183–247 | url = http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-spec-tla-plus.pdf | isbn = 978-90-5199-459-9 | accessdate = 22 May 2015}} </ref> |パラダイム=[[Action language|Action]] |logo_size=248 |wikibooks=}} '''TLA<sup>+</sup>'''は、[[レスリー・ランポート|Leslie Lamport]]によって開発された[[形式仕様記述|形式仕様]]言語。[[並行性|並行システム]]と[[分散コンピューティング|分散システム]]の設計、モデル化、文書化、および検証に使用される。 TLA<sup>+</sup>は、網羅的にテスト可能な[[擬似コード]]<ref name="awsorig"> {{Cite web|author=Newcombe|first=Chris|title=Use of Formal Methods at Amazon Web Services|publisher=[[Amazon Web Services|Amazon]]|date=29 September 2014|url=http://research.microsoft.com/en-us/um/people/lamport/tla/formal-methods-amazon.pdf|accessdate=8 May 2015}}</ref>として説明されており、その使用はソフトウェアシステムの[[製図|設計図]]を描くことに喩えられる。 <ref name="wired"> {{Cite journal|last=Lamport|first=Leslie|author-link=Leslie Lamport|date=25 January 2013|title=Why We Should Build Software Like We Build Houses|url=https://www.wired.com/2013/01/code-bugs-programming-why-we-need-specs/|journal=Wired|publisher=[[Wired (magazine)|Wired]]|accessdate=7 May 2015}}</ref> TLAは''Temporal Logic of Actions''の頭字語である。 設計と文書化に関して、TLA<sup>+</sup> は非公式の技術[[仕様]]と同じ目的を果たす。ただし、TLA<sup>+</sup>の仕様は[[論理学]]と数学の[[形式言語]]で記述されており、この言語で記述された仕様の精度は、システムの実装が始まる前に設計上の欠陥を明らかにすることを目的としている。 <ref name="precise-spec"> {{Cite book|last=Lamport|first=Leslie|author-link=Leslie Lamport|title=Specifying Systems: The TLA<sup>+</sup> Language and Tools for Hardware and Software Engineers|chapter=7.1 Why Specify|page=75|quote=Having to describe a design precisely often reveals problems - subtle interactions and "corner cases" that are easily overlooked.|publisher=[[Addison-Wesley]]|date=18 June 2002|chapterurl=http://research.microsoft.com/en-us/um/people/lamport/tla/book.html|isbn=978-0-321-14306-8}}</ref> TLA<sup>+</sup>のコードは[[形式言語]]で記述するため、有限[[モデル検査]]に適する。モデルチェッカーは、いくつかの実行ステップまでのすべての可能なシステム動作を見つけ、安全性や活性などの望ましい[[不変性]]プロパティの違反を調べる。 TLA<sup>+</sup>のコードでは、基本的な[[集合論]]を使用して安全性（悪いことが起こらない事）を定義し、[[時相論理]]を使用して活性（良いことがいずれ起こる事）を定義する。 TLA<sup>+</sup>は、[[アルゴリズム]]と数学的定理の両方について、マシンでチェックされた[[自動定理証明|正確性の証明]]を作成するためにも使用される。証明は、単一の定理証明者バックエンドに依存しない宣言型の階層スタイルで記述される。公式および非公式の構造化された数学的証明は、TLA<sup>+</sup>で記述できる。言語は[[LaTeX]]に似ており、TLA<sup>+</sup>のコードをLaTeXドキュメントに翻訳するためのツールが存在する。 <ref name="lamport-proofs"> {{Cite journal|last=Lamport|first=Leslie|author-link=Leslie Lamport|date=2012|title=How to Write a 21st Century Proof|url=http://research.microsoft.com/en-us/um/people/lamport/pubs/proof.pdf|journal=Journal of Fixed Point Theory and Applications|volume=11|pages=43–63|accessdate=23 May 2015|DOI=10.1007/s11784-012-0071-6|ISSN=1661-7738}}</ref> TLA<sup>+</sup>は、並行システムの検証方法に関する数十年の研究の後、1999年に公開された。その後、[[統合開発環境|IDE]]や分散モデルチェッカーなどの[[ツールチェーン]]が開発された。擬似コードのような言語[[PlusCal]]は2009年に作成され、TLA<sup>+</sup>に[[トランスコンパイラ|トランスパイル]]され、シーケンシャルアルゴリズムを記述する際に有用とされる。 TLA<sup>+2</sup>は2014年に発表され、プルーフコンストラクトの言語サポートを拡張した。現在のTLA<sup>+</sup>リファレンスは、LeslieLamportによるTLA<sup>+</sup>Hyperbookである。 == 歴史 == [[ファイル:Amir_Pnueli.jpg|代替文=Portrait of an Israeli man in his sixties. His hair is short and balding, and he is wearing glasses with a dress shirt and jacket.|サムネイル|[[アミール・プヌーリ]]は、コンピュータサイエンスに時相論理を適用し、1996年の[[チューリング賞]]を受賞した。]] 現代の[[時相論理]]は、1957年に[[アーサー・プライアー]]によって開発され、当時は時制論理と呼ばれていた。[[アミール・プヌーリ]]が、[[コンピュータサイエンス]]への時相論理の適用を真剣に研究した最初の人物だったが、アーサー・プライアーは1967年の10年前に既にその使用について予測していた。 プヌーリは、コンピュータープログラムの指定と推論における時相論理の使用を研究し、1977年に[[線形時相論理]]を導入した。 線形時相論理は、[[排他制御]]や[[デッドロック]]の解決などの特性を簡単に表現する、並行プログラムの分析のための重要なツールとなった。 <ref name="temporal-logic-history"> {{Cite book|last=Øhrstrøm|first=Peter|last2=Hasle|first2=Per|series=Studies in Linguistics and Philosophy|volume=57|title=Temporal Logic: From Ancient Ideas to Artificial Intelligence|chapter=3.7 Temporal Logic and Computer Science|pages=344–365|publisher=[[Springer Netherlands]]|date=1995|doi=10.1007/978-0-585-37463-5|isbn=978-0-7923-3586-3}}</ref> プヌーリの線形時相論理に関する研究と同時に、学者はマルチプロセスプログラムの検証のために[[ホーア論理]]を一般化するために取り組んでいた。[[レスリー・ランポート]][[査読|は、ピアレビュー]]で相互排除について提出した論文に誤りが見つかった後、この問題に関心を持つようになった。 Ed Ashcroftは、1975年の論文「Proving Assertions About Parallel Programs」で[[不変量|不変性]]を紹介した。これは、Lamportが1977年の論文「Proving Correctness of Multiprocess Programs」で[[ロバート・フロイド|Floydの方法を一般化するために使用した。]]ランポートの論文はまた、[[正当性 (計算機科学)|部分正当性]]と終了の一般化として、それぞれ安全性と活性を紹介した。 <ref name="lamport-proving"> {{Cite web|author=Lamport|first=Leslie|authorlink=Leslie Lamport|title=The Writings of Leslie Lamport: Proving the Correctness of Multiprocess Programs|url=http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#proving|accessdate=22 May 2015}}</ref>[[エドガー・ダイクストラ|この方法は、EdsgerDijkstraによる]]1978年の論文で[[ガベージコレクション|最初の同時ガベージコレクション]]アルゴリズムを検証するために使用された。 <ref name="lamport-garbage"> {{Cite web|author=Lamport|first=Leslie|authorlink=Leslie Lamport|title=The Writings of Leslie Lamport: On-the-fly Garbage Collection: an Exercise in Cooperation|url=http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#garbage|accessdate=22 May 2015}}</ref> ランポートは、[[スーザンオウィッキ]]が主催した[[スタンフォード大学|スタンフォード]]での1978年のセミナーで、プヌーリのLTLに最初に遭遇しました。ランポートによると「時相論理は、実用化されそうもなく抽象的で無意味だと確信していたが、楽しそうだったので参加した。」 との事であったが、1980年に彼は「'Sometime' is Sometimes 'Not Never'」を出版し、時相論理の文献で最も頻繁に引用される論文の1つとなった。 <ref name="lamport-sometime"> {{Cite web|author=Lamport|first=Leslie|authorlink=Leslie Lamport|title=The Writings of Leslie Lamport: 'Sometime' is Sometimes 'Not Never'|url=http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#sometime|accessdate=22 May 2015}}</ref> ランポートは、[[SRIインターナショナル|SRI]]在籍中に時相論理仕様の作成に取り組んだが、このアプローチは実用的ではないとわかった。 [[ファイル:Leslie_Lamport.jpg|代替文=Portrait of a Caucasian man in his seventies with medium-length gray hair and a full gray beard, wearing glasses and a T-shirt.|サムネイル| TLA<sup>+</sup> は、コンピューター科学者であり、2013年チューリング賞を受賞した[[レスリー・ランポート|レスリーランポート]]によって開発された。]] 彼が実用的な仕様方法を模索した結果として1983年に論文「Specifying Concurrent Programming Modules」が生まれた。この論文では、状態遷移をプライム変数と非プライム変数のブール値関数として記述するというアイデアが導入されている。 <ref name="lamport-spec"> {{Cite web|author=Lamport|first=Leslie|authorlink=Leslie Lamport|title=The Writings of Leslie Lamport: Specifying Concurrent Programming Modules|url=http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#spec|accessdate=22 May 2015}}</ref>その模索は1980年代に継続され、ランポートは1990年にアクションの時相論理に関する論文群の発表を開始した。しかし、1994年に「アクションの時相論理」が発表されるまでは正式には導入されなかった。 TLAは、時間式での[[アクション]]の使用を可能にした。これは、ランポートによれば、「並行システム検証で使用されるすべての推論を形式化および体系化するための洗練された方法を提供する。」とされている。<ref name="lamport-actions"> {{Cite web|author=Lamport|first=Leslie|authorlink=Leslie Lamport|title=The Writings of Leslie Lamport: The Temporal Logic of Actions|url=http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#lamport-actions|accessdate=22 May 2015}}</ref> TLAの仕様は、ほとんどが通常の非時相論的数学で構成されていたが、Lamportは、純粋な時間的仕様よりも煩わしさが少ないと発見した。 TLAは、1999年に論文「Specifying Concurrent Systems with TLA<sup>+</sup>」で紹介され、TLA<sup>+</sup>の仕様記述言語としての数学的基礎を提供した。同じ年の後半に、YuanYuはTLA<sup>+</sup>仕様のTLC[[モデル検査|モデルチェッカー]]を作成した。 TLCは、[[Compaq]]マルチプロセッサの[[キャッシュコヒーレンシ|キャッシュコヒーレンス]]プロトコルのエラーを見つけるために使用された。<ref name="tlcoriginal"> {{Cite book|last=Yu|pages=54–66|series=Lecture Notes in Computer Science|accessdate=14 May 2015|url=http://research.microsoft.com/en-us/um/people/lamport/pubs/yuanyu-model-checking.pdf|doi=10.1007/3-540-48153-2_6|date=1999|publisher=[[Springer-Verlag]]|volume=1703|first=Yuan|journal=Correct Hardware Design and Verification Methods|title=Model checking TLA<sup>+</sup> specifications|author3-link=Leslie Lamport|first3=Leslie|last3=Lamport|first2=Panagiotis|last2=Manolios|isbn=978-3-540-66559-5}}</ref> ランポートは、2002年に「Specifying Systems：TLA<sup>+</sup> Language and Tools for Software Engineers」というタイトルの<sup>+</sup>に関する完全な教科書を発行した。 <ref name="specsystems"> {{Cite book|last=Lamport|first=Leslie|author-link=Leslie Lamport|title=Specifying Systems: The TLA<sup>+</sup> Language and Tools for Hardware and Software Engineers|publisher=[[Addison-Wesley]]|date=18 June 2002|url=http://research.microsoft.com/en-us/um/people/lamport/tla/book.html|isbn=978-0-321-14306-8}}</ref> [[PlusCal]]は2009年に導入され<ref name="pluscal-original"> {{Cite book|last=Lamport|first=Leslie|author-link=Leslie Lamport|title=The PlusCal Algorithm Language|journal=Lecture Notes in Computer Science|volume=5684|issue=Theoretical Aspects of Computing - ICTAC 2009|pages=36–60|publisher=[[Springer Berlin Heidelberg]]|date=2 January 2009|url=http://research.microsoft.com/en-us/um/people/lamport/pubs/pluscal.pdf|doi=10.1007/978-3-642-03466-4_2|accessdate=10 May 2015|isbn=978-3-642-03465-7}}</ref> 、TLA<sup>+</sup>プルーフシステム（TLAPS）は2012年<ref name="tlaps-survey"> {{Cite book|last=Cousineau|title=TLA<sup>+</sup> Proofs|series=Lecture Notes in Computer Science|accessdate=14 May 2015|url=http://research.microsoft.com/en-us/um/people/lamport/pubs/tlaps.pdf|doi=10.1007/978-3-642-32759-9_14|date=1 January 2012|pages=147–154|volume=7436|journal=FM 2012: Formal Methods|publisher=[[Springer Berlin Heidelberg]]|first6=Hernán|first=Denis|last6=Vanzetto|first5=Daniel|last5=Ricketts|first4=Stephan|last4=Merz|author3-link=Leslie Lamport|first3=Leslie|last3=Lamport|first2=Damien|last2=Doligez|isbn=978-3-642-32758-2}}</ref>、 TLA<sup>+2</sup>は2014年に発表され、いくつかの言語構造が追加され、プルーフシステムの言語内サポートが大幅に増加した。 ランポートは、更新されたTLA<sup>+</sup>のリファレンスである「The TLA<sup>+</sup> Hyperbook」の作成に取り組んでいる。未完成な作品は彼の公式ウェブサイトから入手できる。Lamportは、TLA+ビデオコースも作成している。このコースでは、「プログラマーとソフトウェアエンジニアにTLA+コードの記述方法を教える入門から始まる一連のビデオレクチャーを作りかけている」と説明されている。 == 言語 == TLA<sup>+</sup>コードは複数のモジュールからなる。モジュールは、他のモジュールを拡張（インポート）して、その機能を使用できる。 TLA<sup>+</sup>標準はタイプセット数学記号で指定されているが、既存のTLA<sup>+</sup>ツールは、[[ASCII]]で[[LaTeX]]のような記号定義を使用する。 TLA<sup>+</sup>では、定義が必要ないくつかの用語を使用する。 * ''State'' – 変数への値の代入 * ''Behaviour'' – 連続したState * ''Step'' – Behaviourでの連続したStateのペア * ''Shuttering step'' – 変数が変更されないStep * ''Next-state relation'' – 変数が任意のStepでどのように変化するかを説明する関係 * ''State function'' – Next-state relationではない変数と定数を含む式 * ''State predicate'' – ブール値の状態関数 * ''Invariant'' – 到達可能なすべてのStateで真とする状態述語 * ''Temporal formula'' – 時相論理のステートメントを含む式 === 安全性 === TLA<sup>+</sup>は、すべての正しいシステム動作のBehaviorを定義することを目的としている。例えば、0と1の間で際限なく刻々と変化する1ビットクロックは、次のように記述できる。<syntaxhighlight lang="text"> VARIABLE clock Init == clock \in {0, 1} Tick == IF clock = 0 THEN clock' = 1 ELSE clock' = 0 Spec == Init /\ [][Tick]_<<clock>> </syntaxhighlight>Relation '''Tick'''はクロックが1であればclock'（次のStateにおけるclockの値）は0、0であれば1を設定する。clockの値が0または1の場合、State Predicateである'''Init'''は'''true'''である。 '''Spec'''は、1ビットクロックのすべてのBehaviorが最初に'''Init'''を満たし、すべてのStepが'''Tick'''に一致するか、Shuttering stepである必要があることをアサートするTemporal formulaである。そのような2つの動作は次の通りである。<syntaxhighlight lang="text"> 0 -> 1 -> 0 -> 1 -> 0 -> ... 1 -> 0 -> 1 -> 0 -> 1 -> ... </syntaxhighlight>1ビットクロックの安全性は –到達可能なシステム状態の集合 –という仕様によって適切に説明される。 === 活性 === 上記の仕様では、1ビットクロックの奇妙な状態は許可されていないが、クロックが常に変化するとは言っていない。たとえば、次のような永続的なShuttering stepが起こりうる。<syntaxhighlight lang="text"> 0 -> 0 -> 0 -> 0 -> 0 -> ... 1 -> 1 -> 1 -> 1 -> 1 -> ... </syntaxhighlight>変化しない時計は役に立たないので、これらの振る舞いは禁止されるべきである。 1つの解決策はShuttering stepを無効にする事であるが、TLA<sup>+</sup>では常にShutteringを有効にする必要がある。Shuttering stepは、仕様に記載されていないシステムの一部への変更を表し、[[詳細化|改良]]に有用である。最終的にTickしなければならないクロックを確保するために、弱い公平性が'''Tick'''のためにアサートできる。<syntaxhighlight lang="text"> Spec == Init /\ [][Tick]_<<clock>> /\ WF_<<clock>>(Tick) </syntaxhighlight>アクションに対する公平性が弱いということは、そのアクションが継続的に有効になっている場合は、最終的に実行する必要があることを意味する。'''Tick'''の公平性が弱いため、ティック間で許可されるShuttering stepの数は限られている。 '''Tick'''に関するこの時相論理ステートメントは、活性アサーションと呼ばれる。一般に、活性アサーションはマシンで閉じる必要がある。到達可能な状態のセットを制約するのではなく、可能な動作のセットのみを制約する必要がある。 <ref name="machine-closure"> {{Cite book|last=Lamport|first=Leslie|author-link=Leslie Lamport|title=Specifying Systems: The TLA<sup>+</sup> Language and Tools for Hardware and Software Engineers|chapter=8.9.2 Machine Closure|page=112|quote=We seldom want to write a specification that isn't machine closed. If we do write one, it's usually by mistake.|publisher=[[Addison-Wesley]]|date=18 June 2002|chapterurl=http://research.microsoft.com/en-us/um/people/lamport/tla/book.html|isbn=978-0-321-14306-8}}</ref> ほとんどの仕様では、活性の表明は必要ない。安全性特性だけでモデル検査とシステム実装の両方に対して事足りる。 <ref name="temporal-logic-confusing"> {{Cite book|last=Lamport|first=Leslie|author-link=Leslie Lamport|title=Specifying Systems: The TLA<sup>+</sup> Language and Tools for Hardware and Software Engineers|chapter=8.9.6 Temporal Logic Considered Confusing|page=116|quote=Indeed, [most engineers] can get along quite well with specifications of the form (8.38) that express only safety properties and don't hide any variables.|publisher=[[Addison-Wesley]]|date=18 June 2002|chapterurl=http://research.microsoft.com/en-us/um/people/lamport/tla/book.html|isbn=978-0-321-14306-8}}</ref> === 演算子 === TLA<sup>+</sup>は[[:en:Zermelo–Fraenkel_set_theory|ZF]]に基づいているため、変数の操作にはセット操作が含まれる。言語には、集合[[元 (数学)|元]]、[[和集合]]、[[共通部分 (数学)|共通部分集合]]、[[差集合]]、[[冪集合|べき集合]]、および[[サブセット|部分集合]]演算子が含まれる。 {{Math|∨}} 、 {{Math|∧}} 、 {{Math|¬}} 、 {{Math|⇒}} 、 {{Math|↔}} 、 {{Math|≡}}などの[[一階述語論理]]演算子、および[[全称記号]]および[[存在記号]]{{Math|∀}}と{{Math|∃}}も含まれている。[[:en:Epsilon_calculus|ヒルベルトの{{Math|ε}}]]は、任意の集合要素を一意に選択するCHOOSE演算子として提供される。[[実数]]、[[整数]]、[[自然数]]の算術演算子は、標準モジュールから利用可能である。 時相論理演算子はTLA<sup>+</sup>に組み込まれている。時間式では<math>\Box P</math> を"''P''が常に真である"を意味し、 <math>\Diamond P</math>を "''P''が最終的に真となる"を意味するという使い方をする。演算子は結合され<math>\Box \Diamond P</math>''は"P''が無限に頻繁に真である"を意味する、または<math>\Diamond \Box P</math>は、"最終的に''P''は常に真になる"という意味となる。他の時相演算子には、弱い公平性と強い公平性が含まれる。弱い公平を表すWF<sub>e</sub>''（A）は、''アクションAが連続して（つまり絶え間なく）有効になっている場合、それが最終的に実施される事を意味する。強い公平を表すSF<sub>e</sub>(A)アクション''Aは、（''中断の有無にかかわらず、繰り返し）''継続的に''有効になっている場合は、それが最終的に実施される事を意味する。 ツールからのサポートはないが時相論的な存在記号と全称記号はTLA<sup>+</sup>に含まれている。 ユーザー定義の演算子は[[マクロ (コンピュータ用語)|マクロ]]に似ている。演算子は、ドメインが集合である必要がないという点において関数とは異なる。たとえば、[[元 (数学)|集合のメンバーシップ]]演算子は、そのドメインとして[[集合の圏]]を持つが、これはZFCでは有効な集合ではない（その存在は[[ラッセルのパラドックス|ラッセルのパラドックスに]]つながるため）。再帰的で匿名のユーザー定義演算子がTLA<sup>+2</sup>に追加された。 === データ構造 === TLA<sup>+</sup>の基本的なデータ構造とは集合である。集合は、明示的に列挙されるか、演算子を使用するか、 <syntaxhighlight lang="tex" inline="">{x \in S : p}</syntaxhighlight> （''pはxの''条件）または<syntaxhighlight lang="tex" inline="">{e : x \in S}</syntaxhighlight> （''eはxの''関数）を使用して他の集合から構築される。一意の[[空集合]]は<code>{}</code>として表される。 TLA<sup>+</sup>の[[関数 (数学)|関数]]は、ドメイン内の各要素集合に値を割り当てる。 <code>[S -> T]</code>は、[[定義域]]集合''Sの''各''xについて、Tにf [x]''を持つすべての関数の集合である。例えばTLA<sup>+</sup>関数<code>Double[x \in Nat] == x*2</code> とは集合 <code>[Nat -> Nat]</code>の一要素であるため、 <code>Double \in [Nat -> Nat]</code>はTLA<sup>+</sup>の真のステートメントである。関数は、一部の式''e'' <code>[x \in S |-> e]</code>を使用するか、既存の関数を変更することによっても定義される<code>[f EXCEPT ![v <sub>1</sub> ] = v <sub>2</sub> ]</code> 。 [[レコード (計算機科学)|レコード]]はTLA<sup>+</sup>の関数の一種である。レコード<code>[name |-> "John", age |-> 35]</code>は、フィールドnameとageを持つレコードであり、 <code>r.name</code>や<code>r.age</code>でアクセスされ、レコードの集合<code>[name : String, age : Nat]</code>に所属する。 [[順序組|タプル]]はTLA<sup>+</sup>に含まれている。 <code><<e <sub>1</sub> ,e <sub>2</sub> ,e <sub>3</sub> >></code>は明示的に定義されるか、標準のシーケンスモジュールの演算子で構成される。タプルの集合は、[[直積集合|デカルト積]]によって定義される。たとえば、自然数のすべてのペアの集合は、 <code>Nat \X Nat</code>として定義される。 == 標準モジュール == TLA<sup>+</sup>には、一般的な演算子を含む一連の標準モジュールがある。それらは構文アナライザーで配布される。 TLCモデルチェッカーは、パフォーマンスを向上させるためにJava実装を使用する。 * '''FiniteSets''' ：[[有限集合]]を扱うためのモジュール。 ''IsFiniteSet（S）''および''Cardinality（S）''演算子を提供する。 * '''Sequences'''： ''Len（S）''、''Head（S）''、''Tail（S）''、''Append（S、E）'' 、[[文字列結合|連結]]、[[フィルター（高階関数）|フィルター]]などの[[順序組|タプルの]]演算子を定義する。 * '''Bags'''： [[多重集合]]を扱うためのモジュール。プリミティブな集合演算の類似物と重複カウントを提供する。 * '''Naturals'''： 不等式および算術演算子とともに[[自然数]]を定義する。 * '''Integers'''：[[整数]]を定義する。 * '''Reals'''：[[実数]]と除算と[[無限|無限大]]を定義する。 * '''RealTime'''：リアルタイムの[[リアルタイムシステム|システム]]仕様で役立つ定義を提供する。 * '''TLC''' ：ロギングやアサーションなど、モデルでチェックされた仕様のユーティリティ関数を提供する。 標準モジュールは<code>EXTENDS</code>または<code>INSTANCE</code>ステートメントでインポートされる。 == ツール == === IDE === {{Infobox Software | 名称 = TLA+ Toolbox | ロゴ = | スクリーンショット = TLA IDE screenshot.png | 説明文 = TLA<sup>+</sup> IDE in typical use showing spec explorer on the left, editor in the middle, and parse errors on the right. | 開発者 = Simon Zambrovski, Markus Kuppe, Daniel Ricketts | 開発元 = [[Hewlett-Packard]], [[Microsoft]] | 初版 = {{Start date and age|2010|02|04}}<!-- {{Start date and age|YYYY|MM|DD|df=yes/no}} --> | discontinued = | 最新版 = 1.7.0 | 最新版発表日 = {{Start date and age|2020|04|25}}<!-- {{Start date and age|YYYY|MM|DD|df=yes/no}} --> | 最新評価版 = 1.7.1 | 最新評価版発表日 = {{Start date and age|2020|05|01}} | リポジトリ = {{URL|https://github.com/tlaplus/tlaplus}} | プログラミング言語 = [[Java]] | 対応OS = | 対応プラットフォーム = | サイズ = | language count = <!-- DO NOT include this parameter unless you know what it does --> | 対応言語 = | 種別 = [[Integrated development environment]] | ライセンス = [[MIT License]] | 公式サイト = {{URL|http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html}} }}[[統合開発環境]]は[[Eclipse (統合開発環境)|Eclipse]]の上に実装されている。これには、エラーと[[シンタックスハイライト]]を備えたエディターに加えて、他のいくつかのTLA<sup>+</sup>ツールへの[[グラフィカルユーザインタフェース|GUI]][[フロントエンド]]が含まれる。 * SANY構文アナライザー。仕様を解析して構文エラーをチェックする。 * pretty-printされた仕様を生成するための[[LaTeX|LaTeXトランスレータ。]] * PlusCalトランスレータ。 * TLCモデルチェッカー。 * TLAPSプルーフシステム。 IDEはTLAツールボックスで配布される。 === モデルチェッカー === [[ファイル:TLC_one-bit_clock_states.png|代替文=Finite state machine diagram of one-bit clock|サムネイル| 1ビットクロックに対してTLCによって検出された状態と遷移。]] TLC[[モデル検査|モデルチェッカー]]は、[[不変量|不変性プロパティ]]をチェックするためのTLA<sup>+</sup>コードの[[有限オートマトン|有限状態]]モデルを構築する。 TLCは、仕様を満たす初期状態のセットを生成し、定義されたすべての状態遷移に対して[[幅優先探索]]を実行する。すべての状態遷移がすでに検出された状態につながると、実行は停止する。 TLCがシステム不変条件に違反する状態を検出すると、TLCは停止し、問題のある状態への状態トレースパスを提供する。 TLCは、[[組合せ爆発|組み合わせ爆発]]を防ぐためにモデルの対称性を宣言する方法を提供する。<ref name="tlcoriginal" /><nowiki></nowiki>また[[並列計算]]状態探索ステップを[[並列計算|並列化し]]、分散モードで実行して、ワークロードを多数のコンピューターに分散させる事もできる。<ref name="tlcdistributed"> {{Cite AV media|last=Markus A. Kuppe|title=Distributed TLC|location=TLA<sup>+</sup> Community Event 2014, Toulouse, France|date=3 June 2014|url=https://vimeo.com/97961350}}</ref> 徹底的な幅優先探索の代わりに、TLCは深さ優先探索を使用するか、ランダムな動作を生成できる。 TLCはTLA<sup>+</sup>のサブセットで動作する。モデルは有限で列挙可能でなければならず、一部の時相演算子はサポートされていない。分散モードでは、TLCは活性特性をチェックすることも、ランダムまたは深さ優先の動作をチェックすることもできない。 TLCは、コマンドラインツールとして、またはTLAツールボックスにバンドルされて利用できる。 TLA<sup>+</sup>プルーフシステム（TLAPS）は、TLA<sup>+で</sup>記述されたプルーフを[[自動定理証明|機械的にチェック]]する。これは、[[Microsoft Research]] - [[フランス国立情報学自動制御研究所|INRIA]] Joint Centerで開発され、並行アルゴリズムと分散アルゴリズムの正確性を証明する。証明言語は、特定の定理証明者から独立するように設計されており、証明は宣言型で記述され、複数の個別の義務として変換されバックエンドの証明者に送信される。主なバックエンドの証明者は[[Isabelle]]とZenonであり、 [[SMT]]ソルバー[[CVC3]] 、 [[Yices]] 、および[[Z3]]定理証明者にフォールバックする。 TLAPSプルーフは階層構造になっているため、リファクタリングが容易になり、非線形開発が可能となる。前のすべてのステップが検証される前に、後のステップで作業を開始でき、難しいステップはより小さなサブステップに分解される。モデルチェッカーは検証が開始される前に小さなエラーをすばやく見つけるため、TLAPSはTLCとうまく連携する。同様にしてTLAPSは、有限モデル検査の機能を超えるシステムプロパティを証明できる。 <ref name="tlaps-survey" /> TLAPSは現在、実数による推論も、ほとんどの時間演算子もサポートしない。 IsabelleとZenonは通常、算術証明の義務を証明できないため、SMTソルバーを使用する必要がある。 <ref name="tlaps-unsupported"> {{Cite web|title=Unsupported TLAPS features|website=TLA<sup>+</sup> Proof System|publisher=[[Microsoft Research]] - [[INRIA]] Joint Centre|url=https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Unsupported_features.html|accessdate=14 May 2015}}</ref> TLAPSは、[[Paxosアルゴリズム|ビザンチンPaxos]] 、Memoirセキュリティアーキテクチャ、およびPastry[[分散ハッシュテーブル]]のコンポーネントの正当性を証明するために使用されている。<ref name="tlaps-survey" /> これは他のTLA<sup>+</sup>ツールとは別に配布され、[[BSDライセンス]]の下で配布されるフリーソフトウェアである。 <ref>[https://tla.msr-inria.inria.fr/tlaps/content/Home.html TLA+ Proof System]</ref> TLA<sup>+2は</sup>、プルーフコンストラクトの言語サポートを大幅に拡張した。 == 業界での使用 == [[Microsoft]]では、TLA<sup>+</sup>で仕様を作成する過程で、 [[Xbox 360]]メモリモジュールに重大なバグを発見した。 <ref name="lamportbuild"> {{Cite AV media|last=[[Leslie Lamport]]|title=Thinking for Programmers (at 21m46s)|publisher=[[Microsoft]]|location=San Francisco|date=3 April 2014|url=http://channel9.msdn.com/Events/Build/2014/3-642#time=21m46s|accessdate=14 May 2015}}</ref> TLA<sup>+</sup>は、[[Paxosアルゴリズム|ビザンチンPaxos]]およびPastry[[分散ハッシュテーブル]]のコンポーネントの正式な証明を作成するために使用された。 <ref name="tlaps-survey" /> [[Amazon Web Services|アマゾンウェブサービス]]は2011年からTLA<sup>+</sup>を使用している。TLA<sup>+</sup>モデル検査によって[[Amazon DynamoDB|DynamoDB]] 、 [[Amazon Simple Storage Service|S3]] 、 [[Amazon Elastic Block Store|EBS]]、および内部分散ロックマネージャーでバグを発見。一部のバグには、35ステップの状態トレースが必要であった。モデル検査は、積極的な最適化を検証するためにも使用された。さらに、TLA<sup>+</sup>仕様は、文書化および設計支援としての価値があることを確認した。 <ref name="awsorig" /> Microsoftの[[Microsoft Azure|Azure]]は、TLA<sup>+</sup>を使用して5つの異なる一貫性モデルをもち世界規模に分散したデータベースであるCosmos DBを設計した。 <ref name="cosmos"> {{Cite web|author=Lardinois|first=Frederic|title=With Cosmos DB, Microsoft wants to build one database to rule them all|publisher=[[TechCrunch]]|date=10 May 2017|url=https://techcrunch.com/2017/05/10/with-cosmos-db-microsoft-wants-to-build-one-database-to-rule-them-all/|accessdate=10 May 2017}}</ref> <ref name="lamportcosmos"> {{Cite AV media|last=[[Leslie Lamport]]|title=Foundations of Azure Cosmos DB with Dr. Leslie Lamport|publisher=[[Microsoft Azure]]|date=10 May 2017|url=https://www.youtube.com/watch?v=L_PPKyAsR3w|accessdate=10 May 2017}}</ref> == 例 == {{Hidden begin|title=A key-value store with [[snapshot isolation]]}} <syntaxhighlight lang="Haskell"> --------------------------- MODULE KeyValueStore --------------------------- CONSTANTS Key, \* The set of all keys. Val, \* The set of all values. TxId \* The set of all transaction IDs. VARIABLES store, \* A data store mapping keys to values. tx, \* The set of open snapshot transactions. snapshotStore, \* Snapshots of the store for each transaction. written, \* A log of writes performed within each transaction. missed \* The set of writes invisible to each transaction. ---------------------------------------------------------------------------- NoVal == \* Choose something to represent the absence of a value. CHOOSE v : v \notin Val Store == \* The set of all key-value stores. [Key -> Val \cup {NoVal}] Init == \* The initial predicate. /\ store = [k \in Key |-> NoVal] \* All store values are initially NoVal. /\ tx = {} \* The set of open transactions is initially empty. /\ snapshotStore = \* All snapshotStore values are initially NoVal. [t \in TxId |-> [k \in Key |-> NoVal]] /\ written = [t \in TxId |-> {}] \* All write logs are initially empty. /\ missed = [t \in TxId |-> {}] \* All missed writes are initially empty. TypeInvariant == \* The type invariant. /\ store \in Store /\ tx \subseteq TxId /\ snapshotStore \in [TxId -> Store] /\ written \in [TxId -> SUBSET Key] /\ missed \in [TxId -> SUBSET Key] TxLifecycle == /\ \A t \in tx : \* If store != snapshot & we haven't written it, we must have missed a write. \A k \in Key : (store[k] /= snapshotStore[t][k] /\ k \notin written[t]) => k \in missed[t] /\ \A t \in TxId \ tx : \* Checks transactions are cleaned up after disposal. /\ \A k \in Key : snapshotStore[t][k] = NoVal /\ written[t] = {} /\ missed[t] = {} OpenTx(t) == \* Open a new transaction. /\ t \notin tx /\ tx' = tx \cup {t} /\ snapshotStore' = [snapshotStore EXCEPT ![t] = store] /\ UNCHANGED <<written, missed, store>> Add(t, k, v) == \* Using transaction t, add value v to the store under key k. /\ t \in tx /\ snapshotStore[t][k] = NoVal /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = v] /\ written' = [written EXCEPT ![t] = @ \cup {k}] /\ UNCHANGED <<tx, missed, store>> Update(t, k, v) == \* Using transaction t, update the value associated with key k to v. /\ t \in tx /\ snapshotStore[t][k] \notin {NoVal, v} /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = v] /\ written' = [written EXCEPT ![t] = @ \cup {k}] /\ UNCHANGED <<tx, missed, store>> Remove(t, k) == \* Using transaction t, remove key k from the store. /\ t \in tx /\ snapshotStore[t][k] /= NoVal /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = NoVal] /\ written' = [written EXCEPT ![t] = @ \cup {k}] /\ UNCHANGED <<tx, missed, store>> RollbackTx(t) == \* Close the transaction without merging writes into store. /\ t \in tx /\ tx' = tx \ {t} /\ snapshotStore' = [snapshotStore EXCEPT ![t] = [k \in Key |-> NoVal]] /\ written' = [written EXCEPT ![t] = {}] /\ missed' = [missed EXCEPT ![t] = {}] /\ UNCHANGED store CloseTx(t) == \* Close transaction t, merging writes into store. /\ t \in tx /\ missed[t] \cap written[t] = {} \* Detection of write-write conflicts. /\ store' = \* Merge snapshotStore writes into store. [k \in Key |-> IF k \in written[t] THEN snapshotStore[t][k] ELSE store[k]] /\ tx' = tx \ {t} /\ missed' = \* Update the missed writes for other open transactions. [otherTx \in TxId |-> IF otherTx \in tx' THEN missed[otherTx] \cup written[t] ELSE {}] /\ snapshotStore' = [snapshotStore EXCEPT ![t] = [k \in Key |-> NoVal]] /\ written' = [written EXCEPT ![t] = {}] Next == \* The next-state relation. \/ \E t \in TxId : OpenTx(t) \/ \E t \in tx : \E k \in Key : \E v \in Val : Add(t, k, v) \/ \E t \in tx : \E k \in Key : \E v \in Val : Update(t, k, v) \/ \E t \in tx : \E k \in Key : Remove(t, k) \/ \E t \in tx : RollbackTx(t) \/ \E t \in tx : CloseTx(t) Spec == \* Initialize state with Init and transition with Next. Init /\ [][Next]_<<store, tx, snapshotStore, written, missed>> ---------------------------------------------------------------------------- THEOREM Spec => [](TypeInvariant /\ TxLifecycle) ============================================================================= </syntaxhighlight> </div> {{Hidden end}} {{Hidden begin|title=ルールベースの[[ファイアウォール]]}} <syntaxhighlight lang="Haskell"> ------------------------------ MODULE Firewall ------------------------------ EXTENDS Integers CONSTANTS Address, \* The set of all addresses Port, \* The set of all ports Protocol \* The set of all protocols AddressRange == \* The set of all address ranges {r \in Address \X Address : r[1] <= r[2]} InAddressRange[r \in AddressRange, a \in Address] == /\ r[1] <= a /\ a <= r[2] PortRange == \* The set of all port ranges {r \in Port \X Port : r[1] <= r[2]} InPortRange[r \in PortRange, p \in Port] == /\ r[1] <= p /\ p <= r[2] Packet == \* The set of all packets [sourceAddress : Address, sourcePort : Port, destAddress : Address, destPort : Port, protocol : Protocol] Firewall == \* The set of all firewalls [Packet -> BOOLEAN] Rule == \* The set of all firewall rules [remoteAddress : AddressRange, remotePort : PortRange, localAddress : AddressRange, localPort : PortRange, protocol : SUBSET Protocol, allow : BOOLEAN] Ruleset == \* The set of all firewall rulesets SUBSET Rule Allowed[rset \in Ruleset, p \in Packet] == \* Whether the ruleset allows the packet LET matches == {rule \in rset : /\ InAddressRange[rule.remoteAddress, p.sourceAddress] /\ InPortRange[rule.remotePort, p.sourcePort] /\ InAddressRange[rule.localAddress, p.destAddress] /\ InPortRange[rule.localPort, p.destPort] /\ p.protocol \in rule.protocol} IN /\ matches /= {} /\ \A rule \in matches : rule.allow ============================================================================= </syntaxhighlight> {{Hidden end}} {{Hidden begin|title=A multi-car [[エレベーター|elevator]] system}} <syntaxhighlight lang="Haskell"> ------------------------------ 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, \* The set of all people using the elevator system Elevator, \* The set of all elevators FloorCount \* The number of floors serviced by the elevator system VARIABLES PersonState, \* The state of each person ActiveElevatorCalls, \* The set of all active elevator calls ElevatorState \* The state of each elevator Vars == \* Tuple of all specification variables <<PersonState, ActiveElevatorCalls, ElevatorState>> Floor == \* The set of all floors 1 .. FloorCount Direction == \* Directions available to this elevator system {"Up", "Down"} ElevatorCall == \* The set of all elevator calls [floor : Floor, direction : Direction] ElevatorDirectionState == \* Elevator movement state; it is either moving in a direction or stationary Direction \cup {"Stationary"} GetDistance[f1, f2 \in Floor] == \* The distance between two floors IF f1 > f2 THEN f1 - f2 ELSE f2 - f1 GetDirection[current, destination \in Floor] == \* Direction of travel required to move between current and destination floors IF destination > current THEN "Up" ELSE "Down" CanServiceCall[e \in Elevator, c \in ElevatorCall] == \* Whether elevator is in position to immediately service call LET eState == ElevatorState[e] IN /\ c.floor = eState.floor /\ c.direction = eState.direction PeopleWaiting[f \in Floor, d \in Direction] == \* The set of all people waiting on an elevator call {p \in Person : /\ PersonState[p].location = f /\ PersonState[p].waiting /\ GetDirection[PersonState[p].location, PersonState[p].destination] = d} TypeInvariant == \* Statements about the variables which we expect to hold in every system state /\ PersonState \in [Person -> [location : Floor \cup Elevator, destination : Floor, waiting : BOOLEAN]] /\ ActiveElevatorCalls \subseteq ElevatorCall /\ ElevatorState \in [Elevator -> [floor : Floor, direction : ElevatorDirectionState, doorsOpen : BOOLEAN, buttonsPressed : SUBSET Floor]] SafetyInvariant == \* Some more comprehensive checks beyond the type invariant /\ \A e \in Elevator : \* An elevator has a floor button pressed only if a person in that elevator is going to that floor /\ \A f \in ElevatorState[e].buttonsPressed : /\ \E p \in Person : /\ PersonState[p].location = e /\ PersonState[p].destination = f /\ \A p \in Person : \* A person is in an elevator only if the elevator is moving toward their destination floor /\ \A e \in Elevator : /\ (PersonState[p].location = e /\ ElevatorState[e].floor /= PersonState[p].destination) => /\ ElevatorState[e].direction = GetDirection[ElevatorState[e].floor, PersonState[p].destination] /\ \A c \in ActiveElevatorCalls : PeopleWaiting[c.floor, c.direction] /= {} \* No ghost calls TemporalInvariant == \* Expectations about elevator system capabilities /\ \A c \in ElevatorCall : \* Every call is eventually serviced by an elevator /\ c \in ActiveElevatorCalls ~> \E e \in Elevator : CanServiceCall[e, c] /\ \A p \in Person : \* If a person waits for their elevator, they'll eventually arrive at their floor /\ PersonState[p].waiting ~> PersonState[p].location = PersonState[p].destination PickNewDestination(p) == \* Person decides they need to go to a different floor LET pState == PersonState[p] IN /\ ~pState.waiting /\ pState.location \in Floor /\ \E f \in Floor : /\ f /= pState.location /\ PersonState' = [PersonState EXCEPT ![p] = [@ EXCEPT !.destination = f]] /\ UNCHANGED <<ActiveElevatorCalls, ElevatorState>> CallElevator(p) == \* Person calls the elevator to go in a certain direction from their floor LET pState == PersonState[p] IN LET call == [floor |-> pState.location, direction |-> GetDirection[pState.location, pState.destination]] IN /\ ~pState.waiting /\ pState.location /= pState.destination /\ ActiveElevatorCalls' = IF \E e \in Elevator : /\ CanServiceCall[e, call] /\ ElevatorState[e].doorsOpen THEN ActiveElevatorCalls ELSE ActiveElevatorCalls \cup {call} /\ PersonState' = [PersonState EXCEPT ![p] = [@ EXCEPT !.waiting = TRUE]] /\ UNCHANGED <<ElevatorState>> OpenElevatorDoors(e) == \* Open the elevator doors if there is a call on this floor or the button for this floor was pressed. LET eState == ElevatorState[e] IN /\ ~eState.doorsOpen /\ \/ \E call \in ActiveElevatorCalls : CanServiceCall[e, call] \/ eState.floor \in eState.buttonsPressed /\ ElevatorState' = [ElevatorState EXCEPT ![e] = [@ EXCEPT !.doorsOpen = TRUE, !.buttonsPressed = @ \ {eState.floor}]] /\ ActiveElevatorCalls' = ActiveElevatorCalls \ {[floor |-> eState.floor, direction |-> eState.direction]} /\ UNCHANGED <<PersonState>> EnterElevator(e) == \* All people on this floor who are waiting for the elevator and travelling the same direction enter the elevator. LET eState == ElevatorState[e] IN LET gettingOn == PeopleWaiting[eState.floor, eState.direction] IN LET destinations == {PersonState[p].destination : p \in gettingOn} IN /\ eState.doorsOpen /\ eState.direction /= "Stationary" /\ gettingOn /= {} /\ PersonState' = [p \in Person |-> IF p \in gettingOn THEN [PersonState[p] EXCEPT !.location = e] ELSE PersonState[p]] /\ ElevatorState' = [ElevatorState EXCEPT ![e] = [@ EXCEPT !.buttonsPressed = @ \cup destinations]] /\ UNCHANGED <<ActiveElevatorCalls>> ExitElevator(e) == \* All people whose destination is this floor exit the elevator. LET eState == ElevatorState[e] IN LET gettingOff == {p \in Person : PersonState[p].location = e /\ PersonState[p].destination = eState.floor} IN /\ eState.doorsOpen /\ gettingOff /= {} /\ PersonState' = [p \in Person |-> IF p \in gettingOff THEN [PersonState[p] EXCEPT !.location = eState.floor, !.waiting = FALSE] ELSE PersonState[p]] /\ UNCHANGED <<ActiveElevatorCalls, ElevatorState>> CloseElevatorDoors(e) == \* Close the elevator doors once all people have entered and exited the elevator on this floor. LET eState == ElevatorState[e] IN /\ ~ENABLED EnterElevator(e) /\ ~ENABLED ExitElevator(e) /\ eState.doorsOpen /\ ElevatorState' = [ElevatorState EXCEPT ![e] = [@ EXCEPT !.doorsOpen = FALSE]] /\ UNCHANGED <<PersonState, ActiveElevatorCalls>> MoveElevator(e) == \* Move the elevator to the next floor unless we have to open the doors here. LET eState == ElevatorState[e] IN LET nextFloor == IF eState.direction = "Up" THEN eState.floor + 1 ELSE eState.floor - 1 IN /\ eState.direction /= "Stationary" /\ ~eState.doorsOpen /\ eState.floor \notin eState.buttonsPressed /\ \A call \in ActiveElevatorCalls : \* Can move only if other elevator servicing call /\ CanServiceCall[e, call] => /\ \E e2 \in Elevator : /\ e /= e2 /\ CanServiceCall[e2, call] /\ nextFloor \in Floor /\ ElevatorState' = [ElevatorState EXCEPT ![e] = [@ EXCEPT !.floor = nextFloor]] /\ UNCHANGED <<PersonState, ActiveElevatorCalls>> StopElevator(e) == \* Stops the elevator if it's moved as far as it can in one direction LET eState == ElevatorState[e] IN LET nextFloor == IF eState.direction = "Up" THEN eState.floor + 1 ELSE eState.floor - 1 IN /\ ~ENABLED OpenElevatorDoors(e) /\ ~eState.doorsOpen /\ nextFloor \notin Floor /\ ElevatorState' = [ElevatorState EXCEPT ![e] = [@ EXCEPT !.direction = "Stationary"]] /\ UNCHANGED <<PersonState, ActiveElevatorCalls>> (***************************************************************************) (* This action chooses an elevator to service the call. The simple *) (* algorithm picks the closest elevator which is either stationary or *) (* 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 == {e \in Elevator : ElevatorState[e].direction = "Stationary"} IN LET approaching == {e \in Elevator : /\ ElevatorState[e].direction = c.direction /\ \/ ElevatorState[e].floor = c.floor \/ GetDirection[ElevatorState[e].floor, c.floor] = c.direction } IN /\ c \in ActiveElevatorCalls /\ stationary \cup approaching /= {} /\ ElevatorState' = LET closest == CHOOSE e \in stationary \cup approaching : /\ \A e2 \in stationary \cup approaching : /\ GetDistance[ElevatorState[e].floor, c.floor] <= GetDistance[ElevatorState[e2].floor, c.floor] IN IF closest \in stationary THEN [ElevatorState EXCEPT ![closest] = [@ EXCEPT !.floor = c.floor, !.direction = c.direction]] ELSE ElevatorState /\ UNCHANGED <<PersonState, ActiveElevatorCalls>> Init == \* Initializes people and elevators to arbitrary floors /\ PersonState \in [Person -> [location : Floor, destination : Floor, waiting : {FALSE}]] /\ ActiveElevatorCalls = {} /\ ElevatorState \in [Elevator -> [floor : Floor, direction : {"Stationary"}, doorsOpen : {FALSE}, buttonsPressed : {{}}]] Next == \* The next-state relation \/ \E p \in Person : PickNewDestination(p) \/ \E p \in Person : CallElevator(p) \/ \E e \in Elevator : OpenElevatorDoors(e) \/ \E e \in Elevator : EnterElevator(e) \/ \E e \in Elevator : ExitElevator(e) \/ \E e \in Elevator : CloseElevatorDoors(e) \/ \E e \in Elevator : MoveElevator(e) \/ \E e \in Elevator : StopElevator(e) \/ \E c \in ElevatorCall : DispatchElevator(c) TemporalAssumptions == \* Assumptions about how elevators and people will behave /\ \A p \in Person : WF_Vars(CallElevator(p)) /\ \A e \in Elevator : WF_Vars(OpenElevatorDoors(e)) /\ \A e \in Elevator : WF_Vars(EnterElevator(e)) /\ \A e \in Elevator : WF_Vars(ExitElevator(e)) /\ \A e \in Elevator : SF_Vars(CloseElevatorDoors(e)) /\ \A e \in Elevator : SF_Vars(MoveElevator(e)) /\ \A e \in Elevator : WF_Vars(StopElevator(e)) /\ \A c \in ElevatorCall : SF_Vars(DispatchElevator(c)) Spec == \* Initialize state with Init and transition with Next, subject to TemporalAssumptions /\ Init /\ [][Next]_Vars /\ TemporalAssumptions THEOREM Spec => [](TypeInvariant /\ SafetyInvariant /\ TemporalInvariant) ============================================================================= </syntaxhighlight> {{Hidden end}} == 関連項目 == * [[B-Method]] * [[計算木論理]] * [[PlusCal]] * [[時相論理]] * [[Z言語]] == 脚注 == {{reflist}} == 外部リンク == * [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html The TLA Home Page], TLA<sup>+</sup>ツール群とリソースにリンクしているレスリーランポートのウェブページ * [http://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html TLA<sup>+</sup> Hyperbook], レスリー・ランポートによるTLA<sup>+</sup>の教科書 * [http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext How Amazon Web Services Uses Formal Methods], ACMの2015年4月のコミュニケーションの記事 * [http://channel9.msdn.com/Events/Build/2014/3-642 Thinking for Programmers], [[:en:Build_(developer_conference)#2014|Build 2014]]でのレスリーランポートによる講演 * [https://www.youtube.com/watch?v=-4Yp3j_jk8Q Thinking Above the Code], 2014 [[:en:Microsoft_Research|Microsoft Research]] faculty summitでのレスリーランポートによる講演 * [https://www.youtube.com/watch?v=iCRqE59VXT0 Who Builds a Skyscraper without Drawing Blueprints?], [[React]] San Francisco 2014でのレスリーランポートによる講演 * [https://www.youtube.com/watch?v=6QsTfL-uXd8 Programming Should Be More than Coding], レスリー・ランポートによる[[スタンフォード大学|スタンフォード]]での2015年の講演 * [http://research.microsoft.com/en-us/um/people/lamport/pubs/euclid.pdf Euclid Writes an Algorithm: A Fairytale], マンフレッド・ブロイの記念論文集に含まれるレスリー・ランポートによるTLA<sup>+</sup>の紹介 * [https://groups.google.com/forum/#!forum/tlaplus TLA<sup>+</sup> Googleグループ] {{DEFAULTSORT:TLA}} [[Category:並行性]] [[Category:形式仕様記述言語]] [[Category:仕様記述言語]] [[Category:形式手法ツール]] [[Category:形式手法]]
このページで使用されているテンプレート:
テンプレート:Cite AV media
(
ソースを閲覧
)
テンプレート:Cite book
(
ソースを閲覧
)
テンプレート:Cite journal
(
ソースを閲覧
)
テンプレート:Cite web
(
ソースを閲覧
)
テンプレート:Hidden begin
(
ソースを閲覧
)
テンプレート:Hidden end
(
ソースを閲覧
)
テンプレート:Infobox Software
(
ソースを閲覧
)
テンプレート:Infobox プログラミング言語
(
ソースを閲覧
)
テンプレート:Math
(
ソースを閲覧
)
テンプレート:Reflist
(
ソースを閲覧
)
TLA+
に戻る。
ナビゲーション メニュー
個人用ツール
ログイン
名前空間
ページ
議論
日本語
表示
閲覧
ソースを閲覧
履歴表示
その他
検索
案内
メインページ
最近の更新
おまかせ表示
MediaWiki についてのヘルプ
特別ページ
ツール
リンク元
関連ページの更新状況
ページ情報