2

次のモデルでverifyingUndefinedFieldsアサーションを確認しようとしています:

module Tests
open law6_withStaticSemantic

assert verifyingUndefinedFields {
    some fa:FieldAccess | fa.pExp in newCreator && fa.id_fieldInvoked !in fa.pExp.((id_cf.(*extend)).fields)
}

check verifyingUndefinedFields

次に提示されたモデルは、law6_withStaticSemantic という別のモデルを使用しています。以下は、このモデルの非常に簡略化されたバージョンです。

module TestWithStaticSemantic    
open javametamodel_withStaticSemantic    
sig Left,Right extends Class{}

one sig ARight, BRight, CRight extends Right{}

one sig ALeft, BLeft, CLeft extends Left{}

pred law6RightToLeft[] {
    twoClassesDeclarationInHierarchy[]
    mirroringOfTwoClassesDeclarationsExceptForTheFieldMoved[]
    law6[]
}

pred twoClassesDeclarationInHierarchy[] {...}    
pred mirroringOfTwoClassesDeclarationsExceptForTheFieldMoved[] {...}
... 
run law6RightToLeft for 10 but 10 Id, exactly 2 FieldAccess, exactly 11 Type, 4 Method, exactly 1 Field, 4 SequentialComposition, 8 Expression, 4 Block, exactly 1 LiteralValue

2 番目のモデル (law6_withStaticSemantic) は、定義された述語に従ってインスタンスを生成します。ただし、最初のモデルでアサーションを実行すると、生成された反例は、2 番目のモデルの述語で定義された条件に従いません。以前のモデルの述語を考慮して反例をチェックするアサーションを構築/実行するにはどうすればよいですか?

モデルについては、以前に次の質問で詳しく説明しました。

Alloy で再帰的な述語/関数を作成する方法

推移的なクロージャを介して再帰的に Alloy 関数を使用する

4

1 に答える 1

2

predicate と assertion のプロパティは、生成されたインスタンスのセットで、後者が仕様のどこかで呼び出された場合にのみ「強制」されます。

モデル 2 では、実行するコマンド ( run law6RightToLeft) に、適用したい述語への参照が含まれています。したがって、生成されたインスタンスがその述語の制約に従っていることがわかります。

さて、最初のモデルでは、このlaw6RightToLeft述語から独立したアサーションをチェックします。この述語で記述されたプロパティを生成されたインスタンスのセットに強制したい場合は、それを変換するか、ファクトで参照する必要があります。

于 2015-11-13T08:54:11.313 に答える