例示と充足可能性

例示とは、仕様を満たすトレースの例を生成するプロセスです。

充足可能性は例示と密接に関連する概念で、仕様を真にするトレースが少なくとも1つ存在する場合、その仕様は充足可能です。SpecForgeの静的解析は、仕様が充足可能かどうかを自動的にチェックし、充足不可能な場合は警告を表示します。

例示と充足可能性チェックはどちらも、ソルバーが考慮する追加の制約である仮定の影響を受けます。

仮定

仮定とは、仕様を解析する際に所与のものとして扱われるプロパティです。検証したいものではなく、物理法則、環境の制約、または成立することが期待される動作条件など、システムに関する背景知識を表します。

assumptionキーワード

Liloでは、assumptionキーワードを使って仮定を宣言できます：

signal temperature: Float
signal heater_on: Bool

assumption physics = always (heater_on => next temperature >= temperature)

spec eventually_warm = eventually (temperature > 30.0)

assumptionは構文的にはspec（パラメータを持たず、戻り値の型は常にBool）と同様ですが、ツールによる扱いが異なります：

• 例示：同じシステム内のすべての仕様のトレース例を生成する際、すべての仮定は自動的に制約として含まれます。ソルバーは仕様とすべての仮定の両方を満たすトレースを生成する必要があります。
• 充足可能性：仕様が充足可能かどうかをチェックする際、仮定が制約セットに含まれます。単独では充足可能な仕様も、仮定のもとでは充足不可能になる場合があります。
• 冗長性：仮定は冗長性チェックの際に他の仕様と並べて含まれます。仮定（および他の仕様）から導出される仕様は冗長として警告されます。

仮定に#[rigidity = "soft"]属性を付けることで、その仮定を例示器に対するソフト制約にすることができます。詳細は下記の厳格度レベルのセクションを参照してください。デフォルトでは、仮定はハードとして扱われます。

したがって、解析を実行する際に仮定を手動で渡す必要はありません。Liloソースで宣言するだけで十分です。

アドホック仮定

assumptionキーワードに加えて、Python SDKやVSCode拡張機能を通じて例示を実行する際にアドホック仮定を渡すこともできます。これらは、システム定義の一部ではなく、特定の解析実行にのみ適用される一時的な制約です。

アドホック仮定は、Liloソースを変更せずに「もし〜だったら」というシナリオを探索したい場合に便利です。例えば、「温度が20度を超えた状態から始まるトレースを生成する」といった場合に使用します。

厳格度レベル

ソース中でassumptionキーワードを使って宣言されたもの、例示クエリにアドホックに渡されたものの別にかかわらず、各仮定にはソルバーがどのように扱うかを制御する厳格度レベルがあります：

• Hard（ハード）：仮定は絶対的な制約として扱われます。生成されたトレースは仮定を必ず満たさなければなりません。仕様とすべてのハード仮定の両方を満たすトレースを見つけられない場合、例示は失敗します。
• Soft（ソフト）：仮定は優先条件として扱われます。ソルバーはまず仕様とすべてのハード仮定を満たすトレースを見つけようとし、次にソフト仮定も満たすように試みます。ソフト仮定がハード制約と共に満たせない場合、それは緩和され、ソルバーはそれでも結果を生成します。

実際には、必須の制約（物理法則、安全境界など）にはHardを使用し、必須ではないが望ましい制約（「温度はある時点で上昇すべき」など）にはSoftを使用してください。

注意： assumptionキーワードで宣言された仮定は、デフォルトでハード厳格度になります。キーワードで宣言された仮定をソフトにするには、#[rigidity = "soft"]で注釈を付けてください。

パラメータをデフォルト値に固定する

例示タスクを実行する際、ソースファイルにデフォルト値が指定されているパラメータは自動的にその値に固定されます。そのため、例示器は、パラメータがそれらの指定された値をとるモデルのみを見つけることになります。

場合によっては、デフォルト値が仕様や仮定と互換性がない場合、充足不可能になることがあります。VSCode拡張機能の easy analysis モードでは、「Fix Params to Defaults」オプションのチェックを外すことでこの動作を無効にできます。この場合、例示器はパラメータにデフォルト値がないかのように動作します。Python SDKでは、exemplifyメソッドにfix_defaults = Falseを渡すことで同じ効果を得られます。

特定のパラメータは自由に変動させつつ、他のパラメータをデフォルト値に固定したい場合は、例示を実行する際にそれらのパラメータにnullというJSON値を渡すことで実現できます。

具体的な例として、次のシステムを考えてみましょう：

system VendingMachine

#[default = 1]
param cansMax : Int

signal cans : Int

assumption cansPositive = cans >= 0

spec reasonableCans = 0 < cans < cansMax

この仕様はcansMaxが1（デフォルト値）の場合、0 < cans < 1を満たす整数cansが存在しないため、充足不可能です。したがって、「Fix Params to Defaults」オプションがチェックされている場合、充足不可能と判定されます。しかし、オプションのチェックが外れている場合、例示器はcansMaxに別の値（例：5）を自由に選択でき、仕様が充足可能になります。同じ効果を得るもう一つの方法は{ cansMax: null }を渡すことで、これにより、例示器はcansMaxを自由変数として扱うようになります。

例

温度センサーシステムにalways_in_boundsという仕様があるとします。混合した厳格度レベルで例示を実行することができます：

• ハード仮定"always_in_bounds"は、生成されたトレースが境界を守ることを保証します。これが不可能な場合、ソルバーは失敗します。
• ソフト仮定"eventually (temperature > 30)"は、トレースに高温度の読み取りを含めることが望ましいという優先条件を表しますが、これがハード制約と矛盾する場合でも、ソルバーは結果を生成します。