付録A. 構文リファレンス（EBNF）

CADLファイルはYAML 1.2文書 [Ben-Kiki+, 2021] である。本付録は CADL v0.2 のリファレンス文法を 2つの部分に分けて示す。文書の構造（A.2〜A.9）は，YAMLのマッピングとシーケンスの上のEBNFとして記述する。式の部分言語（A.1，A.10）は，個々のYAML文字列スカラーの中に書かれる。

第5章と本付録は同じ構文を記述する。具象構文については本付録が規範的であり，第5章は説明のための記述である。リファレンス実装（cadl）は，この構文をそのまま受理することが期待される。cadl 0.3における既知の相違は A.12に示す。

この文法を試すには，リファレンス実装をインストールし（pip install cadl-lang）， cadl parse または cadl check を実行する。実行できるファイルは， cadlリポジトリの examples/ ディレクトリにある。

記法。 文法にはISO/IEC 14977のEBNF [ISO/IEC 14977:1996] を用い，次の規約を置く。

"name:" のようにコロンで終わる終端記号は，YAMLマッピングのキーであり，その後に値が続く。1つのマッピングの中の項目は任意の順序で書いてよく，各項目は高々1回だけ現れる。
{ "-" , x } は，x を要素とするYAMLシーケンスである。ブロック形式とフロー形式（[a, b]）は等価である。
非終端記号 k を用いた k , ":" , v は，キーを記述者が選ぶマッピングである。
text は任意のYAML文字列スカラー，number は任意のYAML整数または浮動小数点数，scalar は任意のYAMLスカラーである。これらの内容はそれ以上解釈しない。
any_char は任意の1文字である。string の規則（A.1）はここから二重引用符を除くので，文字列は次の " で終わる。
(* string *) と注記した生成規則は，1つのYAML文字列スカラーの内容を記述する。

インデント，コメント，引用符，ブロック形式とフロー形式の選択はYAMLの規定に従い，文法には示さない。[，]，*，->，": " を含むスカラー（たとえば "TAXI[*]" のようなアクター参照や "A -> B : msg" のようなステップ）は，引用符で囲むことが望ましい。フローシーケンスの中では，YAMLが別の意味に解釈するため，必ず引用符で囲まなければならない。sharing_entry（A.4）は，どこに書く場合も，引用符で囲んだ文字列でなければならない。

本付録が定義しないキーは CADL v0.2 の一部ではない。処理系は，そのようなキーを理由にファイルを拒否してはならない。リファレンス実装はそれらを無視する。

本文法は5.1.1節の設計レベルと検証レベルを対象とする。概要レベルの記述は， AIによる精緻化のための非形式的な入力であり，本文法に従う必要はない。

A.1 字句規則

これらの規則はスカラーの内部に適用する。

letter          = "A" | … | "Z" | "a" | … | "z" ;
digit           = "0" | … | "9" ;
identifier      = ( letter | "_" ) , { letter | digit | "_" } ;
hyphen_name     = identifier , { "-" , name_part } ;
name_part       = ( letter | digit | "_" ) , { letter | digit | "_" } ;
actor_ref       = identifier , [ "[" , index , "]" ] ;   (* string *)
index           = "*" | range_expr | int_literal | identifier ;
range_expr      = int_literal , ".." , ( int_literal | identifier ) ;
string          = '"' , { any_char - '"' } , '"' ;
int_literal     = digit , { digit } ;
float_literal   = int_literal , "." , [ int_literal ] , [ exponent ]
                | "." , int_literal , [ exponent ]
                | int_literal , exponent ;
exponent        = ( "e" | "E" ) , [ "+" | "-" ] , int_literal ;
bool_literal    = "true" | "false" ;
duration_lit    = int_literal , ( "ms" | "s" | "min" | "h" ) ;
literal         = string | int_literal | float_literal
                | bool_literal | duration_lit ;

identifier は，アクター，契約，プロトコル，運用モード（regime），メトリクスの名前に用いる。 hyphen_name は，拡張の名前とコード生成ターゲットの名前（たとえば sos-dsl， unity-csharp）にだけ用いる。数値リテラルは符号を持たない。識別子はASCIIに限る。文字列とコメントには任意のUnicode文字を使用できる。これが要求NFR-7（第4章）の求める内容である。cadl 0.3.9からは，リファレンス実装は，ASCIIの規則に違反するidや運用モードの名前をエラーとして報告する（A.12）。

A.2 トップレベル構造

cadl_file   = "sos:" , sos_body ;
sos_body    = "name:" , text ,
              [ "type:"         , sos_type ] ,
              [ "version:"      , scalar ] ,
              [ "description:"  , text ] ,
              [ "extensions:"   , { "-" , extension_decl } ] ,
              [ "context:"      , context_block ] ,
              [ "actors:"       , { "-" , actor_def } ] ,
              [ "contracts:"    , { "-" , contract_def } ] ,
              [ "protocols:"    , { "-" , protocol_def } ] ,
              [ "algorithms:"   , { algorithm_def } ] ,
              [ "transitions:"  , { "-" , transition_def } ] ,
              [ "metrics:"      , { "-" , metric_def } ] ,
              [ "verification:" , { "-" , verify_def } ] ,
              [ "codegen:"      , { "-" , codegen_def } ] ,
              [ "motivation:"   , motivation_block ] ;
sos_type    = "Directed" | "Acknowledged" | "Collaborative" | "Virtual" ;
extension_decl = hyphen_name , ":" , scalar ;

1つのファイルは1つのSoS定義を含む。version: には，慣例として "1.0.0" のようなセマンティックバージョンの文字列を書く。

拡張点。 extensions: は，ファイルが依存する言語拡張を，名前とバージョンの組（たとえば - sos-dsl: 0.1）として宣言する。次の2つの拡張を定義している。宣言できる名前を持つのは1つ目だけである。

SoS-DSL拡張（付録E）。名前 sos-dsl，バージョン 0.1 として宣言する。contract_def（A.4）にキー lifecycle: と monitors: を追加する。
動機拡張（付録C）。motivation_block を定義する。 v0.2では extensions: に書く名前を持たず，motivation: ブロックを書くだけで用いる。

A.3 コンテキスト・アクター・メトリクス

context_block  = [ "environment:" , { identifier , ":" , scalar } ] ,
                 [ "assumptions:" , { "-" , text } ] ;

actor_def      = "id:"   , actor_ref ,
                 "role:" , text ,
                 [ "autonomy:"     , autonomy_level ] ,
                 [ "capabilities:" , { "-" , text } ] ,
                 [ "interface:"    , interface_def ] ;
autonomy_level = "low" | "medium" | "high" ;
interface_def  = [ "input:"  , { "-" , text } ] ,
                 [ "output:" , { "-" , text } ] ;

metric_def     = "id:" , identifier ,
                 [ "formula:" , predicate ] ,          (* string *)
                 [ "target:"  , scalar ] ;

autonomy: の既定値は medium である。actor_def の id: の添字は，通常は範囲（"ROBOT[1..N]"）であり，パラメータ化されたアクターの集合を宣言する。 range_expr の上限は整数または識別子である。N のような識別子は記号的な大きさであり， v0.2にはこれを値に束縛する構文がない（リファレンス実装での扱いは A.12を参照）。 environment: の値が文字列でないときはリテラル（A.1）として読み，文字列のときはそのまま保持する。

A.4 コントラクト（制度層）

制度層は，ここで定義する contracts: と，actors:（A.3）および transitions:（A.7）からなる。

contract_def      = "id:"      , identifier ,
                    "parties:" , { "-" , actor_ref } ,
                    [ "assume:"           , { "-" , predicate } ] ,
                    [ "guarantee:"        , { "-" , predicate } ] ,
                    [ "authority:"        , authority_block ] ,
                    [ "information:"      , information_block ] ,
                    [ "responsibilities:" , { actor_ref , ":" , { "-" , text } } ] ,
                    [ "incentives:"       , incentive_block ] ,
                    [ "violation:"        , violation_block ] ,
                    [ "duration:"         , scalar ] ,
                    [ "lifecycle:"        , lifecycle_block ] ,       (* 付録E *)
                    [ "monitors:"         , { "-" , monitor_def } ] ; (* 付録E *)

authority_block   = [ "decision_scope:"  , text ] ,
                    [ "decision_holder:" , actor_ref ] ,
                    [ "beta:"            , number ] ,
                    [ "mode:"            , text ] ;

information_block = [ "alpha:"   , number ] ,
                    [ "views:"   , { actor_ref , ":" , text } ] ,
                    [ "sharing:" , { "-" , sharing_entry } ] ;
sharing_entry     = actor_ref , "->" , actor_ref , ":" , identifier ;  (* string *)

incentive_block   = [ "type:"   , text ] ,
                    [ "lambda:" , number ] ,
                    [ "rules:"  , { "-" , text } ] ;

violation_block   = [ "detect:"     , text ] ,
                    [ "action:"     , text ] ,
                    [ "escalation:" , text ] ;

assume: と guarantee: の各要素は，predicate（A.10）を保持する文字列である。 alpha，beta，lambda は [0, 1] の範囲になければならない。parties: は宣言済みのアクターを少なくとも1つ挙げなければならず，契約の中のアクター参照はすべて actors: で宣言されたアクターを指さなければならない。duration: は indefinite，duration_lit，またはイベントの記述のいずれかである。 sharing_entry は，引用符で囲んだ文字列として書かなければならない（- "TAXI[*] -> CENTRAL : position"）。引用符がないと，YAMLはこれを文字列ではなく，項目が1つのマッピングとして読む。

A.5 プロトコル

protocol_def     = "id:"      , identifier ,
                   "trigger:" , text ,
                   [ "precondition:"     , text ] ,
                   "steps:"   , { "-" , step } ,
                   [ "timing:"           , { identifier , ":" , scalar } ] ,
                   [ "fallback:"         , { identifier , ":" , text } ] ,
                   [ "rollback:"         , rollback_block ] ,
                   [ "postcondition:"    , text ] ,
                   [ "safety_invariant:" , text ] ;
rollback_block   = [ "condition:" , text ] ,
                   [ "action:"    , text ] ;

step             = message_step | compute_step | conditional_step
                 | parallel_step | barrier_step ;
message_step     = actor_ref , "->" , actor_ref , ":" , step_expr ;
compute_step     = actor_ref , ":" , step_expr ;
conditional_step = "if" , predicate , ":" , { "-" , step } ,
                   [ "else:" , { "-" , step } ] ;
parallel_step    = "parallel:" , { "-" , step } ;
barrier_step     = "barrier:" , predicate ;
step_expr        = function_call | identifier ;

message_step と compute_step は，シーケンスの1要素である。引用符で囲んだ文字列（- "A -> B : msg(x)"，推奨）として書いても，引用符なしで書いてもよい。後者の場合，YAMLはこれを項目が1つのマッピングとして読むが，両者は等価である。 conditional_step，parallel_step，barrier_step は，キーが if <predicate>， parallel，barrier のマッピングである。timing: の代表的なキーは max_response，max_total，checkpoint_interval であり，fallback: の代表的なキーは on_timeout と on_failure である。

A.6 アルゴリズム

algorithm_def = identifier , ":" , algorithm_body ;
algorithm_body = [ "central:" , text ] ,
                 [ "local:"   , text ] ;

algorithms: は，機能の名前（たとえば pathfinding）から，中央側とローカル側で用いるアルゴリズムへのマッピングである。

A.7 遷移

transition_def = "from:" , identifier ,
                 "to:"   , identifier ,
                 [ "condition:"        , predicate ] ,     (* string *)
                 [ "protocol:"         , identifier ] ,
                 [ "safety_invariant:" , predicate ] ;     (* string *)

from: と to: は運用モードの名前である。運用モードは遷移の中で使うことで導入され，別個の宣言はない。protocol: は protocols: で宣言したプロトコルを指すことが望ましい。

A.8 検証ブロック

verify_def    = "id:"   , identifier ,
                "type:" , text ,
                [ "target:"   , verify_target ] ,
                [ "property:" , text ] ,
                [ "method:"   , verify_method ] ,
                [ "expr:"     , predicate ] ,              (* string *)
                [ "bound:"    , int_literal ] ;
verify_target = identifier
              | identifier , "->" , identifier ;           (* FROM->TO *)
verify_method = "smt" | "model_check" | "simulation" | "proof" ;

type: は性質の種類を表し，たとえば consistency，deadlock，safety， liveness を書く。target: は対象の契約，プロトコル，または遷移の名前である。すなわち，契約またはプロトコルの id，運用モードの名前，または2つの運用モードの間の遷移を表す FROM->TO を書く。 method: の既定値は smt である。宣言された手法を実装していない処理系は，その項目を黙って読み飛ばすのではなく not_supported として報告しなければならず，未知の手法はエラーとして報告しなければならない。宣言されたものを何も指さない target: は，エラーとして報告することが望ましい。

A.9 コード生成ブロック

codegen_def = [ "target:"   , hyphen_name ] ,
              [ "output:"   , text ] ,
              [ "mappings:" , { identifier , ":" , text } ] ;

target: の既定値は python である。ターゲットの名前は付録Dに一覧する。output: は出力先のパスであり， mappings: はターゲットに固有の名前の対応を生成器に渡す。

A.10 式

predicate は，1つのYAML文字列スカラーの中に書く。

predicate        = or_expr ;
or_expr          = and_expr , { "OR" , and_expr } ;
and_expr         = not_expr , { "AND" , not_expr } ;
not_expr         = "NOT" , not_expr
                 | comparison ;
comparison       = arith_expr , [ comp_op , arith_expr ]
                 | quantified_expr ;
comp_op          = "==" | "!=" | "<=" | ">=" | "<" | ">" ;
quantified_expr  = ( "for all" | "exists" ) , identifier , "in" ,
                   arith_expr , ":" , predicate ;
arith_expr       = term , { ( "+" | "-" ) , term } ;
term             = factor , { ( "*" | "/" ) , factor } ;
factor           = "(" , predicate , ")"
                 | function_call
                 | member_access
                 | literal
                 | indexed_ref ;
function_call    = identifier , "(" , [ arg_list ] , ")" ;
arg_list         = arg , { "," , arg } ;
arg              = predicate | comprehension ;
comprehension    = predicate , "for" , identifier , "in" ,
                   ( range_expr | arith_expr ) ;
member_access    = indexed_ref , "." , identifier , { "." , identifier } ;
indexed_ref      = identifier ,
                   [ "[" , ( "*" | range_expr | arith_expr ) , "]" ] ;

演算子の結合の強さは，弱いものから順に OR，AND，NOT，比較，+ -， * / である。優先順位が等しい二項演算子は左結合である。比較は結合的でない（a < b < c は述語ではない）。量化子の有効範囲は，右方向へ可能な限り広くとる。トークンの間の空白は無視する。

comprehension は集約関数の引数であり，束縛された識別子の値ごとに，その predicate を 1回評価する。たとえば sum(ROBOT[i].goal_count for i in 1..N) や sum(r.load for r in ROBOT[*]) である。

assume: または guarantee: の要素がこの文法に従わなくても，構文エラーにはならない。その要素は不透明な述語として保持され，処理系はそれを変更せずに引き渡し，形式検証の対象から除く。これにより，設計レベルでは自然言語による条件を書くことができる。A.5のステップの式と条件についても同様である。

A.11 予約語

式の部分言語のキーワード。これらを識別子として用いてはならない。

AND    OR    NOT    true    false    for all    exists    in

単独の for（内包表記を導入する）と all は予約語ではない。IN（大文字。モニターの rule の中での集合への所属，付録E）と in（小文字。量化子と内包表記の定義域）は，別のキーワードである。

構造のキー。認識されるブロックごとに示す。

ブロック	キー
ファイル	`sos`
`sos`	`name` `type` `version` `description` `extensions` `context` `actors` `contracts` `protocols` `algorithms` `transitions` `metrics` `verification` `codegen` `motivation`
`context`	`environment` `assumptions`
アクター	`id` `role` `autonomy` `capabilities` `interface`（`input` `output`）
契約	`id` `parties` `assume` `guarantee` `authority` `information` `responsibilities` `incentives` `violation` `duration` `lifecycle` `monitors`
`authority`	`decision_scope` `decision_holder` `beta` `mode`
`information`	`alpha` `views` `sharing`
`incentives`	`type` `lambda` `rules`
`violation`	`detect` `action` `escalation`
プロトコル	`id` `trigger` `precondition` `steps` `timing` `fallback` `rollback`（`condition` `action`） `postcondition` `safety_invariant`
ステップ	`if` `else` `parallel` `barrier`
アルゴリズム	`central` `local`
遷移	`from` `to` `condition` `protocol` `safety_invariant`
メトリクス	`id` `formula` `target`
検証	`id` `type` `target` `property` `method` `expr` `bound`
コード生成	`target` `output` `mappings`

列挙値: Directed Acknowledged Collaborative Virtual（SoSの型）， low medium high（自律度），smt model_check simulation proof （検証手法），ms s min h（時間の単位）。拡張のキーと値は付録Cと付録Eに示す。

A.12 リファレンス実装の状況（`cadl` 0.3）

リファレンス実装は，YAML 1.1のローダーでファイルを読み，寛容に振る舞う。パーサが拒否するのは，sos: マッピングの欠落，不正なYAML，不正な type:，および数値でない alpha，beta，lambda だけである。 cadl check は，これに加えて，idの重複，未宣言のアクター，重複して挙げられた当事者，当事者のない契約，[0, 1] の範囲外のガバナンスパラメータ，Minor，Major， Critical 以外の severity:，low，medium，high 以外の autonomy:，識別子でないidや運用モードの名前，形式に合わない sharing: の要素，および付録Eの規則L-1，L-2，L-3，L-5，M-1（cadl 0.3.11から），M-3への違反，および（cadl 0.3.12から）読み取れない deadline: と sampling: の値をエラーとして報告する。assume: または guarantee: の項目の中では，名前が添字付きである（ROBOT[i]）か，メンバーアクセスの対象である（ROBOT.battery）とき，添字の中に現れる場合も含めて，その名前はアクターへの参照とみなされ，宣言されていなければならない。単独で現れる名前は状態変数とみなされ，検査されない。condition:，safety_invariant:，formula:，expr:，モニターの rule:，ライフサイクルの when:，およびメッセージイベントでない on: の述語については，未宣言のアクターの検査を行わない。それ以外の必須キーが欠けている場合は，空の値で置き換える。cadl 0.3では，次の点で本付録と相違する（cadl 0.3.13で確認）。

式。 cadl 0.3.13では，式はA.10とA.11に従う。既知の相違はない。
識別子。 cadl 0.3.9からは，cadl check は，アクター，契約，プロトコル，メトリクスのid，および運用モードの名前が，A.1の識別子でない場合（たとえば非ASCII文字やハイフンを含む場合），またはA.11の予約語か付録Eの IN である場合に，エラーとして報告する。 cadl 0.3.10からは，ライフサイクルの状態の名前，ライフサイクルの遷移とモニターのid，およびモニターの違反ラベルにも同じ検査が適用される。検証項目のidは検査されない。 cadl 0.3.12までは，これらの名前や運用モードの名前に引用符なしで書いた true / false は YAMLが真偽値として読み，True / False という名前として受理されていた。
範囲。 上限が記号である範囲（"TAXI[1..N]"）は，書かれたとおりに保持される。 N を environment: から引くことはなく，添字が宣言された範囲に収まるかどうかも検査されない。cadl sim-gen が count を出力するのは，両端が整数のときだけである。
型。 5.2.1節の型は検査されない。型構成子を用いて書いた値（たとえば Range(1, 4)）は，テキストのまま保持される。
寛容な形式。 パーサは，1つの文字列として書いた parties:（"[A, B]"），負でない数値の deadline:（小数でもよく，秒として読まれる），単位の前に空白を含む期間（5 s，periodic( 500ms )），マッピング {kind: periodic, period_ms: <負でない整数>} または {kind: event} として書いた sampling:，および大文字と小文字を問わない method: も受理する。これらの形式は本付録の一部ではない。
ステップ。 cadl 0.3.10からは，conditional_step の else: の分岐と，barrier_step の条件が保持される。したがって，else: の分岐に現れるアクターは検査され，どちらもシミュレータIRに出力される。それより前のリリースは，これらを捨てていた。
契約。 cadl 0.3.9からは，"SOURCE -> TARGET : item" の形式の文字列でない sharing: の要素，および項目が識別子で始まらない要素は，cadl check でエラーとなる。それより前のリリースは，引用符なしの要素を診断なしに捨てていた。"A -> B : report(period: 5s)" の引数のように，項目が識別子で始まり，その後ろに別の文字列が続く要素は，警告を出したうえで受理され，先頭の名前だけが保持される。この形式は本付録の一部ではない。 cadl 0.3.10からは，low，medium，high 以外の autonomy: の値は，cadl check でエラーとなる。それより前のリリースは，診断なしに medium として読んでいた。
検証。 method:，expr:，bound: は読み込まれる。smt 以外の手法は not_supported として報告され（テキスト出力では [SKIP] と表示される），未知の手法はエラーとなる。宣言されたものを何も指さない target: は，どの手法についてもエラーとなる。 smt の項目については，充足不能な expr: はエラーとなり，A.10に適合しない expr: は unknown として報告され，検査されない。expr をモデルに対して証明することはしない。 6.3節の契約と遷移の検査は，項目の有無にかかわらず実行される。
コード生成。 codegen: の項目は構文解析されるが，それに基づく処理は行われない。ターゲットはコマンドラインで選択する（付録D）。 cadl 0.3.9からは，実装が出力できない target: を持つ項目（たとえば target: ros2）について， cadl check，cadl verify，cadl codegen が警告を出す。これは付録DのD.4節が求める診断であり，ファイルは有効なままである。コマンドラインの -t ros2 は拒否される。
拡張。 lifecycle: と monitors: は，extensions: が sos-dsl を宣言しているかどうかにかかわらず認識される。cadl 0.3.9からは，cadl check は，sos-dsl 以外の extensions: の名前， 0.1 以外の sos-dsl のバージョン，および motivation: ブロックについて，情報レベルの診断を出す。この診断によってファイルが無効になることはない。これは，拡張を実装していない処理系に付録Cが求めるものである。motivation: ブロックは解釈されないが， cadl sim-ir は，このブロックを書かれたとおりに motivation_block というキーで引き渡す（付録CのC.6節）。ファイルにこのブロックがなければ，このキーは出力されない。 cadl が付録Eそのものに対して満たしていない点は，E.4節に示す。

cadl の0.3.7より前のリリースは，これらの点のいくつかで異なっていた。その経緯は，cadlリポジトリの CHANGELOGにある。

A.1 字句規則​

A.2 トップレベル構造​

A.3 コンテキスト・アクター・メトリクス​

A.4 コントラクト（制度層）​

A.5 プロトコル​

A.6 アルゴリズム​

A.7 遷移​

A.8 検証ブロック​

A.9 コード生成ブロック​

A.10 式​

A.11 予約語​

A.12 リファレンス実装の状況（cadl 0.3）​