No counterexample found issue

Questions
1

I have this model, basically services store a list of request.name -> request id. I created a request which isn’t in the list, so I would expect no change to the buffer that is used to store the request hits. But I tested it against s.buffer' = s.buffer + r.name -> r.id, I would expect a counterexample, but none is found.

sig Id, Name {}

abstract sig Request {
	id : Id,	
	name : Name
}

abstract sig Service { 
	var list : Name -> set Id 
}

sig Service1 extends Service      { 
	-- store hits in buffer
	var buffer : Name -> set Id 
}

sig HitMissRequest extends Request {} { 
	no a : Service1 | name -> id in a.list
}

pred Process [r : Request, s : Service] {
	isHit[r, s] and 	
       -- since it's miss s.buffer' should equal to s.buffer only								
	s.buffer' = s.buffer + r.name -> r.id
}

pred isHit [r : Request, s : Service] {
	r.name -> r.id in s.list
}

assert MissRequest {
	all r : HitMissRequest, s : Service1 |
		Process[r, s] implies
			s.buffer' = s.buffer + r.name -> r.id
}

check MissRequest

no Counterexample found, no sure why.

2

Hi,
There is no counterexample because Process[r,s] is always false when r is a HitMissRequest, hence the implication is true.
Maybe you had in mind a different specification for Process, namely one that keeps the buffer the same if the request does not satisfy isHit. Something as follows:

pred Process [r : Request, s : Service] {
	isHit[r, s] implies s.buffer' = s.buffer + r.name -> r.id
	else s.buffer' = s.buffer
}

With this specification you will get a counterexample.
Best,
Alcino

1 Like
3

Thank you so much Alcino! I looked up implication true table, False → True and False → False both result in True. This issue is tricky for me to figure out. I have changed pred according to your suggestion. It worked!!