1

本当に不可解な質問があります。この述語のインスタンスが見つからないようです。以下はコードです。

module keyless
open util/ordering[state] as trace

abstract sig ownerpostype{}

//owner is out and far away from the car
//this set should be mapped to person
one sig far extends ownerpostype{} //{(far)}
one sig near extends ownerpostype{} //{(near)}
one sig insidecar extends ownerpostype{} //{(insidecar)}

//engine status
abstract sig enginetype{}
one sig on extends enginetype{} //engine is on
one sig off extends enginetype{}

//car door status
abstract sig dooroptype{}
one sig unlock extends dooroptype{}
one sig lock extends dooroptype{}
one sig opened extends dooroptype{}

//car status
abstract sig motortype{}
one sig moving extends motortype{}
one sig still extends motortype{}

//key fob position
abstract sig keypostype{}
one sig incar extends keypostype{} //key fob in car
one sig faralone extends keypostype{}
one sig pocket extends keypostype{}

sig state{
  owner: ownerpostype,  //(s, far) or (s,near) or (s, insideCar)
  //engine: enginetype,  
  door: dooroptype,
  //motor: motortype,
  //key: keypostype
}

//initial state
pred init (s: state){
  //engine intially off
  s.door in lock and s.owner in far
}

//operations on the owners position
pred towards (s, s' : state){
 s.owner in far and s'.owner in near and s.door = s'.door
}

//operations on key position
pred getin (s, s' : state){
 s.owner in near 
 s.door in opened
 s'.door = s.door
 s'.owner in insidecar
}

//operations on door status
pred unlockopen (s, s' : state){
  s.owner in near and s.door in lock
  s'.door in opened 
  s'.owner = s.owner
}

pred close (s, s' : state){
  s.door in opened and s'.door in unlock
  s'.owner = s.owner
}

fact {
  first.init
  all t : state - last | let t' = t.next |
     towards[t, t'] or getin[t, t'] or unlockopen[t, t'] 
}

run getin

インスタンスを取得できないのはなぜですか? コードをトレースしたところ、基本的なトレースは次のようになります: init -> together -> unlockopen -> getin.

これらの先行する各述語は、後続の述語の制約を満たす必要があります。では、getin を除く残りの述語のインスタンスを取得できるのはなぜでしょうか。

これについてのガイダンスを本当に感謝します。

4

1 に答える 1

7

デフォルトのスコープは 3 です。3 つの状態で 3 つのアクションを実行することはできません。4 つ必要です。

不整合のデバッグに関する一般的なヒントを次に示します。

  1. コマンドにインスタンスがない場合は、緩めて何が起こるかを確認してください。この場合、 に変更できrun getinますrun {}。

  2. 「コア」リンクをクリックして、unsat コアを表示します。この場合、すべてのアクション述語が表示されており、問題が発生しただけではないことが示唆されます。

  3. 範囲を広げてみてください。ただし、util/orderingこれを使用している場合は、順序付けられた型のスコープが正確になるため、少し注意が必要です (たとえば、署名 Action があり、署名 State を注文していた場合、State のスコープを設定し、アクションの値が小さい場合、トレースを埋めるのに十分なアクションがない可能性があります)。

于 2012-11-25T03:41:25.607 に答える