メインコンテンツまでスキップ

5. 言語仕様

5.1 全体構造​

CADL記述は，以下のトップレベル要素で構成される。1つのCADLファイルは1つのSoS定義を含む。CADLファイルはYAML文書であり，CADLの式（述語，ステップ）はYAML文字列の中に書く。

sos:
  name: <文字列>                # SoS名
  type: <Directed|Acknowledged|Collaborative|Virtual>  # SoS分類
  version: <セマンティックバージョン>

  context:                      # 環境・前提条件
    environment: { ... }
    assumptions: [ ... ]

  actors:                       # 構成システム（アクター）定義
    - id: <識別子>
      role: <文字列>
      autonomy: <low|medium|high>
      capabilities: [ ... ]

  contracts:                    # 契約定義（中核要素）
    - id: <識別子>
      parties: [ ... ]
      assume: [ ... ]           # 前提条件（assume-guarantee）
      guarantee: [ ... ]        # 保証条件
      authority: { ... }        # 権限構造
      information: { ... }      # 情報共有構造
      responsibilities: { ... } # 責任分担
      incentives: { ... }       # インセンティブ構造

  protocols:                    # プロトコル定義
    - id: <識別子>
      trigger: <イベント式>
      steps: [ ... ]
      timing: { ... }
      fallback: { ... }

  algorithms:                   # アルゴリズム参照
    <機能名>:
      central: <アルゴリズム名>
      local: <アルゴリズム名>

  transitions:                  # 制度遷移定義
    - from: <モードID>
      to: <モードID>
      condition: <述語式>
      protocol: <遷移プロトコルID>
      safety_invariant: <安全条件>

  metrics:                      # 評価指標定義
    - id: <識別子>
      formula: <式>
      target: <目標値>

この骨格は主要なブロックだけを示しており，description，verification，codegen，extensions，motivation は省略している。キーの完全な一覧は付録AのA.11節にある。

v0.2では，運用モード（regime）は名前である。transitions: の from: / to: に現れることで導入され，別個の宣言はない。また，契約やパラメータ値をモードに結び付ける構文は言語にない。

5.1.1 段階的記述レベル​

CADLは，利用者の専門性と記述の目的に応じた3段階の記述レベルを提供する。概要レベルは非形式的な記述であり，文法の対象外である（付録Aは，そのような記述は文法に適合しなくてよいとしている）。概要レベルのキーは自由形式であり，記述者は任意のキーを任意の言語で選んでよい（下の概要レベルの例は，付録Aが定義しない 内容: と 紛争解決: を用いている）。設計レベルへ進むには，下の設計レベルの例に示す構造へ書き直す。設計レベルのファイルは，ブロックを追加することで検証レベルへ拡張する。

記述レベル対象利用者記述内容構文の特徴
概要レベル (Overview)市民・自治体職員・企業実務者・学生SoS名，アクターの役割，契約の概要（自然言語），基本的なルール自然言語に近い記述を許容 / パラメータ・制約は省略可 / AI生成の入口となる
設計レベル (Design)設計者・研究者・上級学生制度パラメータ(α,β,λ)，プロトコル手順，遷移条件，メトリクスパラメータ値の明示 / 型注釈の付与 / 制約式の記述
検証レベル (Verification)SoSアーキテクト・検証エンジニアassume-guarantee契約，安全不変条件，形式的性質（時相論理）形式的述語・量化子 / SMT/モデル検査用注釈 / codegen/synthesis指定

v0.2には，型注釈，時相論理の性質，synthesisを書く構文はない。したがって，表のうち次の3つは目指す方向を述べたものである。設計レベルの行の「型注釈の付与」と，検証レベルの行の「形式的性質（時相論理）」，および「codegen/synthesis指定」のうちsynthesisの部分である。検証レベルの行の残りは，v0.2に存在する。assume-guarantee契約，安全不変条件，形式的述語・量化子，SMT・モデル検査を指定する verification: 項目の method:（A.8節），codegen: ブロック（A.9節）である。v0.2の検証レベルのファイルに書ける内容は，下の断片に示す。

以下に，家庭内ルールの「家事分担」を題材に，同一の制度が，概要レベル，設計レベル，および設計レベルのファイルに追加する断片としての検証レベルで，どのように記述されるかの例を示す。

# === 概要レベル: 市民・学生向け ===
sos:
  name: "家庭の家事分担"
  type: Collaborative
  description: "家族4人で家事を公平に分担するルール"

  actors:
    - 親（2人）: 家事の割り当てを決める
    - 子ども（2人）: 割り当てられた家事を担当する

  contracts:
    - name: "家事の分担ルール"
      内容: >
        毎週，親が家事を割り当てる。
        子どもは夕食前までに完了する。
        完了したら100円のお小遣いをもらえる。
      紛争解決: "話し合いで決める。まとまらなければ親が最終決定。"
# === 設計レベル: パラメータ・プロトコルの追加 ===
sos:
  name: "FamilyHousehold"
  type: Collaborative
  version: "1.0.0"

  actors:
    - id: PARENT[1..2]
      role: "parent"
      autonomy: high
    - id: CHILD[1..2]
      role: "child"
      autonomy: medium
    - id: AI_ASSISTANT
      role: "mediator"
      autonomy: low

  contracts:
    - id: CHORE_SHARING
      parties: ["PARENT[*]", "CHILD[*]"]
      authority:
        decision_holder: PARENT[1]
        beta: 0.7                    # やや集中的
      incentives:
        lambda: 0.6
        rules:
          - "reward(CHILD[i], 100yen) when chore_completed_on_time"

  protocols:
    - id: CONFLICT_RESOLUTION
      trigger: "resource_conflict_detected"
      steps:
        - AI_ASSISTANT : propose_alternatives(all_parties)
        - PARENT[*] : vote(preferred_alternative)
        - CHILD[*] : vote(preferred_alternative)
        - if consensus_reached:
            - AI_ASSISTANT : update_schedule
          else:
            - PARENT[1] : make_final_decision

検証レベルの記述は，設計レベルのファイルに verification: ブロックを追加したものであり，その構文は付録AのA.8節に示す。下の断片は，設計レベルの例の sos: の下に，protocols: と同じインデントで追加する。

  # === 検証レベル: 設計レベルのファイルに追加するブロック ===
  verification:
    - id: CHORE_CONSISTENCY        # 対象だけを指定
      type: consistency
      target: CHORE_SHARING
      method: smt
    - id: REWARD_BOUND             # 述語を指定（付録A，A.10）
      type: safety
      target: CHORE_SHARING
      property: "週ごとの報酬が予算内に収まる"
      method: smt
      expr: "weekly_reward >= 0 AND weekly_reward <= 400"

このブロックを追加したファイルを，cadl verify（cadl 0.3.13）は受理し，2つの項目をどちらも合格と報告する。expr: を持つ項目については，述語が充足可能であることだけを検査し，モデルに対して証明することはしない（付録AのA.12節）。

7.1節は，検証レベルが目指す矛盾検出を例示する（1.2節の目的2）。7.1節の記述例は概念的なものであり，A.8節のキーとは異なるキーを用いている（第7章冒頭の注記を参照）。このように，同一の制度が利用者のニーズに応じて異なる粒度で記述でき，AIが概要レベルから設計・検証レベルへの精緻化を支援する。

5.2 データモデル​

5.2.1 型システム​

以下の表にCADLの組み込み型を示す。これらは言語設計の一部であり，リファレンス実装（cadl 0.3）はこれらを検査しない（付録A，A.12）。

型名説明記述例
Int整数型latency_ms: 100
Float浮動小数点型failure_rate: 0.002
Bool真偽値型is_active: true
String文字列型role: "vehicle"
Duration時間長型timeout: 100ms, 5s, 1min
Range区間型latency: Range(0, 200)
Dist確率分布型demand: Normal(15, 3)
Enum列挙型autonomy: low | medium | high
Set集合型parties: [CENTRAL, "TAXI[*]"]
Mapマップ型views: { CENTRAL: "global", TAXI: "local" }
Actorアクター参照型decision_holder: CENTRAL
ActorSetアクター集合型（ワイルドカード対応）TAXI[*], SENSOR[1..N]

5.2.2 アクターモデル​

アクターはSoSの構成システムを表す基本単位である。各アクターは一意の識別子を持ち，役割・自律性レベル・能力を宣言する。アクターの集合はワイルドカード記法（[*]）またはインデックス範囲（[1..N]）で参照できる。範囲の上限は整数または名前である。N のような名前は記号的な大きさであり，v0.2にはこれに値を与える構文がないので，その記述は任意の数のアクターについてのものになる。リファレンス実装は，このような範囲を書かれたとおりに保持する。N を context.environment から引くことはなく，cadl sim-gen がアクターの数を出力するのは，両端が整数の範囲のときだけである（[1..3] は count: 3 になる）。[1..N] の場合，生成される設定に数は含まれない（付録AのA.12節）。

actors:
  - id: CENTRAL
    role: "global_planner"
    autonomy: low
    capabilities:
      - compute_routes
      - monitor_all
    interface:
      input: [taxi_positions, failure_reports]
      output: [route_assignments]

  - id: TAXI[1..N]       # N台のタクシーをパラメトリックに定義
    role: "vehicle"
    autonomy: high
    capabilities:
      - local_navigation
      - obstacle_detection
    interface:
      input: [assigned_route, road_status]
      output: [position, sensor_data]

autonomy:（low / medium / high，既定値は medium）と，ファイルレベルの type:（Directed / Acknowledged / Collaborative / Virtual）は，説明のためのラベルである。リファレンス実装はこれらを記録し，レポートや生成する設定に渡すが，βやその他の値と照合する検査は行わない。

5.2.3 契約モデル​

契約はCADLの中核要素であり，assume-guaranteeセマンティクスに基づく。各契約は以下のサブ要素を持つ。

サブ要素説明
assume前提条件。契約が有効であるために環境・他アクターが満たすべき条件。
guarantee保証条件。前提条件が満たされた場合に契約当事者が保証する性質。
authority意思決定のスコープと決定権者。集中度パラメータβを含む。
informationalpha（共有度パラメータα），各当事者が持つ views，および sharing のフロー（送信元 -> 受信先 : 項目）を保持する。push/pull/broadcastといった共有モードはv0.2では表現できない（下の例の sharing: の要素に付けたコメントは，フローが周期的かイベント駆動かを注記しているが，コメントにすぎない）。
responsibilities各当事者の義務・タスクの列挙。
incentives報酬・ペナルティ・評判メカニズムの定義。強度パラメータλを含む。
duration契約の有効期間。無期限・期限付き・イベント駆動の3種。
violation契約違反時の検出条件と対応動作。
contracts:
  - id: CENTRALIZED_ROUTING
    parties: [CENTRAL, "TAXI[*]"]

    assume:
      - "CENTRAL.is_operational == true"
      - "network_latency <= 200ms"
      - "for all t in TAXI[*]: has_capability(t, local_navigation)"

    guarantee:
      - "all_routes_conflict_free()"
      - "route_update_delay <= 100ms"

    authority:
      decision_scope: "route_assignment"
      decision_holder: CENTRAL
      beta: 0.9          # 意思決定の集中度（0=完全分散，1=完全集中）

    information:
      alpha: 0.9          # 情報共有度
      views:
        CENTRAL: "global_road_graph + all_taxi_positions"
        TAXI[*]: "assigned_route + local_sensors"
      sharing:
        - "TAXI[*] -> CENTRAL : position"       # 定期的（1秒周期）
        - "CENTRAL -> TAXI[*] : route"          # イベント駆動

    responsibilities:
      CENTRAL:
        - compute_conflict_free_routes(all_taxis)
        - update_routes_on_failure
      TAXI[*]:
        - follow_route
        - "report_position(period: 1s)"
        - report_detected_failures

    incentives:
      type: reputation
      lambda: 0.5
      rules:
        - "reward(TAXI[i], 10) when on_time_delivery"
        - "penalty(TAXI[i], -5) when route_deviation"

    violation:
      detect: "route_deviation > threshold OR position_report_delay > 5s"
      action: "notify(CENTRAL) AND log_violation"
      escalation: "after 3 violations: suspend_contract"

    duration: indefinite

5.2.4 プロトコルモデル​

プロトコルはアクター間の協調手順を定義する。ステップには次の5種類がある。

  • メッセージ送信（A -> B : m，矢印記法）— アクターAがアクターBにメッセージ m を送る。
  • ローカル計算（A : f(x)，コロン記法）— アクターAが自身の計算を行う。
  • 条件分岐（if / else）— 条件が成り立つときは if の下のステップを，成り立たないときは else: の下のステップを実行する。
  • parallel: — その下に並べたステップは互いの順序が定まっておらず，それらがすべて完了するとプロトコルは先へ進む。
  • barrier: — 同期点である。与えた条件が成り立つときにだけ，プロトコルは先へ進む。

cadl 0.3.10からは，リファレンス実装は else: の分岐とバリアの条件を保持する。それより前のリリースは，これらを捨てていた（付録AのA.12節）。

protocols:
  - id: FAILURE_REPLAN
    trigger: "road_failure_detected_by(TAXI[i])"
    precondition: "CENTRAL.is_operational"

    steps:
      - TAXI[i] -> CENTRAL : failure_report(road_id, severity)
      - CENTRAL : validate_failure(road_id)
      - if severity >= HIGH:
          - CENTRAL : recompute_routes(all_taxis)
          - CENTRAL -> TAXI[*] : new_route
        else:
          - CENTRAL : recompute_routes(affected_taxis)
          - CENTRAL -> TAXI[*] : new_route

    timing:
      max_response: 100ms
      max_total: 500ms

    fallback:
      on_timeout: "TAXI[*] : execute_safe_stop()"
      on_failure: "switch_to_protocol(LOCAL_REPLAN)"

    postcondition: "all_routes_conflict_free()"

  - id: REGIME_TRANSITION
    trigger: "regime_map.recommend(new_regime) != current_regime"

    steps:
      - CENTRAL -> TAXI[*] : transition_notice(new_regime, deadline)
      - parallel:
          - TAXI[*] : prepare_for_transition()
          - CENTRAL : verify_safety_invariants(new_regime)
      - barrier: all_ready(TAXI[*])
      - CENTRAL : activate_regime(new_regime)
      - CENTRAL -> TAXI[*] : regime_activated

    timing:
      max_total: 30s
      checkpoint_interval: 5s

    rollback:
      condition: "NOT all_ready(TAXI[*]) within 20s"
      action: "revert_to(current_regime)"

    safety_invariant: "no_collision AND service_continuity"

5.3 構文定義​

CADLファイルはYAML文書である。以下にCADLの主要な構文規則をEBNF（拡張バッカス・ナウア記法）で示す。記法は付録Aに従う。すなわち，コロンで終わる終端記号はYAMLマッピングのキーであり，マッピングの中の項目は任意の順序で書いてよく，{ "-" , x } は x を要素とするYAMLシーケンスである。述語の式の構文を含む完全な文法は付録Aを参照されたい。具象構文については付録Aが規範的である。以下の規則は抜粋であり，ファイルの extensions: と motivation:，契約の lifecycle: と monitors:（付録AのA.2節とA.4節），および入れ子のブロックの規則を省いている。

(* CADL EBNF - 主要規則（抜粋。付録Aが規範的である） *)

cadl_file = "sos:" , sos_definition ;
sos_definition = "name:" , text ,
    [ "type:" , sos_type ] ,
    [ "version:" , scalar ] ,
    [ "description:" , text ] ,
    [ "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 } ] ;

sos_type = "Directed" | "Acknowledged" | "Collaborative" | "Virtual" ;

actor_def = "id:" , actor_ref ,
    "role:" , text ,
    [ "autonomy:" , autonomy_level ] ,
    [ "capabilities:" , { "-" , text } ] ,
    [ "interface:" , interface_def ] ;

actor_ref = identifier , [ "[" , ( "*" | range_expr | int_literal | identifier ) , "]" ] ;
autonomy_level = "low" | "medium" | "high" ;

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 ] ;

protocol_def = "id:" , identifier ,
    "trigger:" , text ,
    [ "precondition:" , text ] ,
    "steps:" , { "-" , step } ,
    [ "timing:" , { identifier , ":" , scalar } ] ,
    [ "fallback:" , { identifier , ":" , text } ] ,
    [ "rollback:" , rollback_block ] ,
    [ "postcondition:" , text ] ,
    [ "safety_invariant:" , 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 ;

契約で必須なのは id と parties だけであり，本章の例では不要なブロックを省略している。autonomy の既定値は medium である。

ファイルはYAMLであるため，一部のスカラーは引用符で囲む必要がある。プロトコルのステップは引用符なしで書いてもよい。YAMLは A -> B : m を項目が1つのマッピングとして読み，パーサはこれを受理する。ただし，引用符で囲んだ形（- "A -> B : m"）を推奨する。sharing: の要素（- "TAXI[*] -> CENTRAL : position"）と，インラインのリストの中の添字付きアクター参照（parties: [CENTRAL, "TAXI[*]"]）は，引用符で囲まなければならない（付録Aの記法の規約とA.4節）。囲まないと，YAMLが別の意味に読むか，拒否する。cadl 0.3.9からは，リファレンス実装は引用符なしの sharing: の要素をエラーとして報告する（付録AのA.12節）。

5.4 意味論​

5.4.1 契約のassume-guaranteeセマンティクス​

CADLの契約は，Benvenisteらの契約ベース設計理論およびSaoudらの連続時間assume-guarantee契約に基づく。契約C = (A, G)において，Aは前提条件（assume），Gは保証条件（guarantee）である。合成と飽和形はBenvenisteらに，弱充足と強充足の区別はSaoudらによる（付録Bを参照）。

飽和形: 契約C = (A, G)は，Aに違反するすべての振る舞いをGがすでに含んでいるとき，すなわちGをG ∨ ¬Aで置き換えたとき，飽和形（正準形）であるという。

無矛盾性: 契約は，A ∧ Gが充足可能であるとき無矛盾である。リファレンス実装の検証器が，契約ごとに，また当事者を共有する契約の対について検査するのは，この性質である。

契約の合成: 2つの契約C₁ = (A₁, G₁)とC₂ = (A₂, G₂)の並行合成は，飽和形（正準形）の契約に対して C₁ ⊗ C₂ = ((A₁ ∧ A₂) ∨ ¬(G₁ ∧ G₂), G₁ ∧ G₂) で定義される。

弱充足と強充足: 弱充足では，構成要素は，それまでAが成り立ち続けている間，Gを満たさなければならない。強充足では，Aが成り立たなくなった後も短い時間はGを満たし続けなければならない。これが，構成要素間の循環論法を断ち切る。循環依存がある場合はSaoudらに従い，各構成契約に（弱充足ではなく）強充足を要求する。

5.4.2 制度パラメータの意味論​

制度パラメータα（情報共有度），β（意思決定集中度），λ（インセンティブ強度）は，それぞれ区間[0, 1]の値を取る。これらのパラメータは制度の構造的特性を連続的に制御し，モードマップ構築の基礎となる。

パラメータ名称意味
α (alpha)情報共有度0: 情報非共有（各アクターはローカル情報のみ） / 1: 完全共有（全アクターが全情報を観測可能）
β (beta)意思決定集中度0: 完全分散（C-SoS: 各アクターが自律的に決定） / 1: 完全集中（D-SoS: 単一アクターが全決定）
λ (lambda)インセンティブ強度0: インセンティブなし（指令ベース） / 1: 強いインセンティブ（市場メカニズム）

表に示したβとSoS類型の対応は目安であり，検査される規則ではない（5.1.1節の例は type: Collaborative と beta: 0.7 を組み合わせている）。

5.4.3 プロトコルの操作的意味論​

プロトコルの各ステップはラベル付き遷移システム（LTS）として解釈される。メッセージ送信 A -> B : m は，Aの送信アクションとBの受信アクションの同期合成として定義される。タイミング制約は時間オートマトンの不変条件として符号化し，UPPAAL [Larsen+, 1997] 等のモデル検査器で検証することを設計上の意図としている。cadl 0.3ではモデル検査は統合されておらず，デッドロック検出は構造解析で行う（6.3節）。

5.5 この先の参照先​

  • 完全な文法とキーの一覧: 付録A。
  • 5.2節で詳しく扱っていないブロック（context，algorithms，transitions，metrics，verification，codegen）: 付録AのA.3節とA.6〜A.9節で規定する。
  • 契約のライフサイクルとモニター（lifecycle:，monitors:）: 付録E。
  • 動機拡張: 付録C。
  • コード生成ターゲット: 付録D。
  • ファイルの検査: cadl parse，cadl check，cadl verify（インストール方法は仕様書イントロダクションに示す）。
  • 実行できる例: cadlリポジトリのexamples/ ディレクトリ。