Why is there no instance found for this predicate?

Question

I have a really puzzling question. I can't seem to find an instance for this predicate. Below is the code.

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

Why can't getin have an instance? I have traced the code, and the basic trace should follow like this: init -> towards -> unlockopen -> getin.

Each of these preceding predicates should fulfil the constraints in the succeeding predicate. So why can I get an instance for the rest of the predicates except getin?

Would really appreciate some guidance on this.

Answer 1

The default scope is 3. You can't get an execution of 3 actions with 3 states -- you need 4!

Here are some general tips on debugging inconsistencies:

1. If your command has no instances, then loosen it and see what happens. In this case, you could change run getin to run {}.

2. Click on the "core" link to see the unsat core. In this case, it shows all the action predicates, suggesting that the problem isn't just getin itself.

3. Try increasing the scope. But note that when you're using util/ordering this is a bit tricky because it makes the scope on the ordered type exact (so, for example, if you had a signature Action and were ordering a signature State, if you set a scope for State and a smaller one for Action, you may not have enough actions to fill the trace).